1 Introduction

Substructural logics originated. In the work of Gentzen [40] (see also [84]), namely,. In the formalization of intuitionistic logic as the sequent calculus LJ. The classical sequent calculus LK yields LJ with the restriction that there be at most one formula. In the succedent. This restriction also renders two of the right structural rules superfluous. In the late 1950s, Lambek. Introduced a calculus, which omitted all the structural rules from LK, and then,. In [56], he treated the comma as a binary operation with no special properties assumed.

Of course, various changes to LK may change the properties of the logical connectives that can be. Introduced, plus previously. Interchangeable rules may turn out not to be equipotent. Substructural logics,. In a limited sense, could mean the. Investigation of logical systems that are obtained from LK via the. Introduction of some structural restrictions. However, we adopt a more encompassing view here, which. Includes. Into the area of substructural logics all those logics that have a sequent calculus-style formalization that is not merely an extension of LK with new axioms or rules. [29] is a representative collection of papers that was published after the first conference on substructural logics. In 1990.

I will emphasize two main themes that. Intertwine. In the. Investigations of substructural logics,. In the last 40 years or even longer. One of these is the connection between combinatory logic and sequent calculi. The other is the goal of defining semantics (preferably, set-theoretic semantics) for a wide range of logics. In a systematic way — rather than crafting somewhat ad hoc. Interpretations each time.

Substructural logics have produced a lot of. Interesting results. In the last couple of decades, and there remain. Interesting unsolved, and yet undiscovered problems. In a short overview, there is no space to provide complete proofs or even proof sketches. Also, the list of references cannot be exhaustive; however, it is. Intended to provide some pointers —. Including for topics that are not touched upon. In any detail. In the text.

2 New Substructural Logics

The major relevance logics (R, E and T) had been formulated. In the 1950s and 1960s. However, the so-called minimal relevance logic, B was not. Introduced until 1972. In [63] (and reshaped. In [80]). What the logic B and its fragments lack. In complexity, they make up. In. Interesting connections to type assignment systems and to structurally free logics.

A logic that attracted much attention. In the 1990s is linear logic, LL, that was. Introduced. In [42]. It was advertised as the constructivization of logic carried all the way through. However, the main. Influences of this logic were a surge of. Interest. In logics (and their set-theoretical semantics) that cannot prove the distributivity of conjunction (∧) and disjunction (∨) and an. Interest. In exploring structural rules that are applicable only to formulas of a particular shape. The first paper on LL used a peculiar notation, and its terminology is often quite original. More standard presentations,. Including axiomatic, natural deduction and two-sided sequent calculi may be found. In [4] and [86].

Linear logic may be viewed as a combination of logics: its multiplicative part (minus the zero-ary constants) is BCI logic, which was singled out already. In [57]; the algebra of the additive part is a non-distributive lattice, and the exponentials are modalities. The idea of combining modal logics is well-known — this is how Prior created the first tense logics, for. Instance. There had been a sustained. Interest. In adding necessity to R — with the idea of giving an alternative presentation for E, the logic of entailment (or at least for some of its fragments). Indeed, E and LL have a strong similarity. In that they both restrict the types of arguments for certain combinators. The restrictions. In E are expressible by improper combinators, which require certain arguments to have functional types; LL, on the other hand, requires the addition of new sorts of combinators, because the modalities cannot be captured as functional types.

Additions of modalities to the basic relevance logic are studied. In [81]. Further combinations of certain relevance logics and. Intuitionistic negation and. Intuitionistic implication are. Investigated, respectively,. In [75] and [43], for example.

Fragments are, perhaps, neither new logics, nor separate logics (in some sense). Nonetheless, sometimes they are isolated,. Investigated and extended later than the original logics are — as illustrated by [24], which deals with (extensions of) fragments of R-mingle.

3 Sequent and Display Calculi

Given that substructural logics originated from modifications of LK, it may be surprising at first that not all substructural logics had sequent calculus formulations. In the early 1960s.

The implicational fragments of E and R had been formulated as sequent calculi long ago, and Kripke’s decision procedure for them. In [52] relied on those sequent calculi. The addition of negation was straightforward as. In [7], however, the addition of ∧ and ∨ turned out to be challenging.

The difficulty, to put it quickly, is that the proof of the distributivity of ∧ over ∨ (e.g.,. In LK) requires not only permutation and contraction, but also thinning, which is not an acceptable structural rule from the point of view of the motivations of relevance logics — see [33] for more details. The left thinning rule. In LK yields (1), the so called “negative paradox of material implication” (⊃), and with a left permutation step added, it gives (2), the “positive paradox” too.

$${} (1)\,\,\, \varphi\supset\psi\supset\psi \qquad\qquad\qquad\qquad\qquad(2)\,\,\, \varphi\supset\psi\supset\varphi $$

The difficulties arising. In a sequent calculus formulation of a logic that contains distributive conjunction and disjunction, may be compared to the easy sequent calculus presentation of linear logic and of some variations on the associative Lambek calculus, where the distributivity of ∧ and ∨ is not provable. The latter logics have been studied. In [68] as well as. In [74] and. In [70] among others.

The core. Insight that is necessary to obtain a sequent calculus presentation of positive relevance logics, is the split of the structural connective of a sequent calculus along the lines where the families of operations are divided. Classical propositional logic. In its common presentations is highly redundant. In the light of functional completeness results, but. In R, for. Instance, the addition of ∧ and ∨ (using usual notation) is not superfluous when → (implication) and ∼ (negation) are the only connectives. Of course, it should also be ensured that the structural connectives (or the structures that they generate from formulas and structures). Interact appropriately.

Dunn. In [30] defined L R + and. Introduced a new structural connective, denoted by ; , which may be thought to correspond to ∘ (intensional conjunction). In a similar way as , corresponds to ∧ (extensional conjunction). The two kinds of structural connectives generate. Intensional and extensional structures, respectively. To ensure the appropriate. Interaction of the two kinds of structures, the empty. Intensional structure has to be handled carefully, especially,. In applications of the cut rule. This is facilitated by the. Inclusion of t (intensional truth). Into the logic.

LK — unlike LJ — is a calculus with multiple right-hand sides. Several formulas on the right-hand side of the turnstile are used. In handling negation as well as. In a proof of the classical theorem ((φ⊃ψ)⊃φ)⊃φ (which is often used as an axiom). The analogue of this formula is not a theorem of R →, and. In the absence of negation, the calculus may be formulated so that every sequence contains exactly one formula on the right.

R allows the permutation as well as the regrouping of the premises. In other words, ∘ is a commutative and associative operation. In R. Neither E nor T contains a similar semi-group operation. In this respect, these logics are somewhat similar to the non-associative Lambek calculus,. In which the only structural connective is a binary operation that is not assumed to be either associative or commutative. The need for t. In the sequent calculi for the positive fragments of B, T and E used to cause a difficulty. The cut theorem, following Gentzen, is usually proved by double. Induction for a single or a multiple cut. (For relevance logics, the latter cannot go as far as mix does, because there is no way to reinstate missing occurrences of a formula by applications of the thinning rule.) Unfortunately, the double. Inductive argument is not sufficient to prove the cut theorem when the constant t is. Included.

Connections between structural rules. In sequent calculi and combinators were noticed by Curry (mentioned. In [28]), who also. Invented the theory of functionality. The connection was made precise. In [38], where structurally free logics, the LC systems were. Introduced. Function application is neither associative nor commutative; accordingly, LC contains a binary structural connective ; . Additionally, LC moves beyond type-assignment systems. In that it treats combinators as formulas, and they appear not simply as labels on rules, which may as well be omitted from a proof. Combinators can be. Introduced. In two ways, either by the identity axiom or by rules that are reminiscent of structural rules, but. Insert the appropriate combinator. Into the lower sequent. That is, combinatory rules are like structural rules, but their application leaves an. Indelible mark. In the sequent itself. To give an example, the rule for the combinator C (the three-place regular permutator) and for Y (the fixed point combinator) are as follows.

$$\frac{\Gamma[{\Delta}_{1};{\Delta}_{2};{\Delta}_{3}]\vdash\varphi}{\Gamma[\mathsf{C};{\Delta}_{1}; {\Delta}_{3};{\Delta}_{2}]\vdash \varphi}\,\,(\mathsf{C}\vdash) \qquad\qquad \frac{\Gamma[{\Delta};(\mathsf{Y};{\Delta})]\vdash\varphi}{\Gamma[\mathsf{Y};{\Delta}]\vdash \varphi}\,\,(\mathsf{Y}\vdash) $$

The axioms for these combinators are \(\mathsf {C} xyz\vartriangleright xzy\) and \(\mathsf {Y} x\vartriangleright x(\mathsf {Y} x)\). The latter combinator is obviously not proper, but it is definable from a combinatorially complete basis — even if that comprises proper combinators only. Y was not. Included. In the original LC systems. In [38], where the admissibility of cut was proved. If (Y⊩) is. Included, then the usual double. Inductive proof for multiple cut cannot be carried out. Nonetheless, it is possible to prove by. Induction, as. In [10], that applications of the cut rule,. In which the cut formula is Y, are directly eliminable. t with respect to its effect is more like the identity combinator I (perhaps, collapsed with the dual identity combinator). However, from a proof-theoretic point of view, the behavior of t is quite similar to that of Y.

Structurally free logics are. Interesting. In their own right, but they also. Inspired some of the new sequent calculi for the implicational and for the positive fragments of B, T and E. These are presented. In [16, Ch. 2], [11] and [12], respectively. The implicational fragment of ticket entailment with. Intensional truth, \(T_{\rightarrow }^{\boldsymbol {t}}\) may be formalized as a sequent calculus by the identity axiom φ⊩φ and the multiplicative implication. Introduction rules

$$\frac{\Gamma\vdash\varphi\quad{\Delta}[\psi]\vdash\chi}{\Delta[\varphi\rightarrow \psi;{\Gamma}]\vdash\chi}\,\,(\rightarrow\vdash) \qquad\qquad \frac{\Gamma;\varphi\vdash\psi}{\Gamma\vdash\varphi\rightarrow\psi}\,\,(\vdash\,\rightarrow) $$

together with structural rules, three of which are similar to rules for the combinators B, B ′ and W,

$$\frac{\Gamma[{\Delta}_{1};({\Delta}_{2};{\Delta}_{3})]\vdash\varphi}{\Gamma[{\Delta}_{1}; {\Delta}_{2};{\Delta}_{3}]\vdash\varphi}(\mathsf{B}\vdash) \qquad \frac{\Gamma[{\Delta}_{2};({\Delta}_{1};{\Delta}_{3})]\vdash\varphi}{\Gamma[{\Delta}_{1}; {\Delta}_{2};{\Delta}_{3}]\vdash\varphi}\,\,(\mathsf{B}^{\prime}\vdash) \qquad \frac{\Gamma[{\Delta}_{1};{\Delta}_{2};{\Delta}_{2}]\vdash\varphi}{\Gamma[{\Delta}_{1}; {\Delta}_{2}]\vdash\varphi}\,\,(\mathsf{W}\vdash) $$

and two of which are specific to t

$$\frac{\Gamma[{\Delta}]\vdash\varphi}{\Gamma[\,\boldsymbol{t};{\Delta}]\vdash \varphi}\,\,(\mathsf{K}\mathsf{I}_{\boldsymbol{t}}\vdash) \qquad\qquad \frac{\Gamma[\,\boldsymbol{t};\boldsymbol{t}\,]\vdash\varphi}{\Gamma[\,\boldsymbol{t}\,]\vdash\varphi}\,\,(\mathsf{M}_{\boldsymbol{t}}\vdash). $$

A remarkable feature of this as well as of the aforementioned sequent calculi is that they all admit the cut rule, and the cut theorem has been proved rigorously, utilizing multiple. Inductions.

The sequent calculi \(LT_{\rightarrow }^{\boldsymbol {t}}\) and \(LE_{\rightarrow }^{\boldsymbol {t}}\) treat the structural connective ; as a groupoid operation, which leads to the idea that a proof of a theorem of T → or E →. In these sequent calculi must allow the extraction of a combinatory. Inhabitant for the theorem. Combinatory type-assignment systems are usually formulated. In natural deduction-style, which are quite close to axiomatic proof systems with a strict notion of proofs (see, e.g., the traversing proofs. In [11]). Sequent calculi retain the context at each step. In a proof, thereby, allowing freedom as to which formulas to reason with. The constant presence of context makes the. Inhabitant extraction more challenging than that from a traversing proof. Extraction algorithms are defined for classes of proofs. In \(LT_{\rightarrow }^{\boldsymbol {t}}\) and \(LE_{\rightarrow }^{\boldsymbol {t}}\). In [21] and [14, Ch. 9], respectively.

Display logic was. Introduced. In [5] and applied to LL. In [6]. Display calculi are rich. In structural connectives — typically containing more than one family of them — and they place an emphasis on the relationships between these connectives. The name of these systems alludes to the possibility of displaying formulas on one or the other side of the turnstile without any surrounding formulas or structures. This facilitates the proof of the admissibility of the display cut rule.

Residuation, a concept that originated. In lattice theory, is a conspicuous relationship between certain operations that is suitable for “moving things around.”. In LK, ⊃ is a residual of ∧. If a new structural connective would be added to LK, let us say, denoted by \(\rightsquigarrow \), then Γ,φ⊩Δ could perhaps be treated as equivalent to \({\Gamma }\vdash \varphi \rightsquigarrow {\Delta }\), which would allow moving formulas to the right. Similarly, the ⊅ connective is a residual of ∨, that is, of , on the right-hand side of ⊩ . Adding a structural connective emulating ⊅ would enable moving formulas to the left. The display logic framework has been applied to other logics, for. Instance,. In [73] and [45].

The structural connectives on the two sides of the turnstile may have the same shape (like ,. In LK), but they are distinct structural connectives. The cut rule. In LK can be used as follows.

figure a

This is a very simple (classical) example of the phenomenon that was called hemidistributivity. In [37]. Obviously, in LK where , is associated to ∧ or to ∨, respectively, and all structural rules are available, this cut is as eliminable as any other. The general case, however, is more subtle as shown. In [18], where a new method is. Introduced for the proof of the cut theorem. In symmetric generalized Galois logics. The semantical analysis of the same logics using set-theoretical representations (and expanding previous results. In gaggle theory,. Including those. In [16]) are. In [17].

4 Semantics for Substructural Logics

The first set-theoretical semantics for a substructural logic was. Introduced. In the 1960s by Kripke. In [54]. Intuitionistic logic has well-known connections to the normal modal logic S4, and their semantics utilize a pre-order (or a partial order) on a set of situations and on a set of possible worlds. From the more general viewpoint provided by gaggle theory, that was. Introduced by Dunn. In [34], it is a coincidence that the. Intuitionistic implication connective can be modeled from a binary accessibility relation (as shown. In [36]).

Relevance logics are philosophically well-motivated. Notwithstanding, the meta-theory of these logics posed new and often mathematically more difficult problems than those encountered. In the meta-theory of classical logic. The set-theoretical semantics of classical logic along the lines of [82] and [47] can be viewed to be continued. In the representation theory for Boolean algebras with operators. In [48] and [49], as well as. In the standard semantics for normal modal logics. In [53] and [55].

A set-theoretical semantics was defined for the semi-relevant logic R-mingle (RM). In [31] and [32]. R-mingle is atypical within the relevant family, because Sugihara matrices, which are linearly ordered, are models of propositional RM. Once again, it is a coincidence that the accessibility relation that enters. Into the modeling of the implicational connective can be chosen to be an order relation.

The major relevance logics, E, R and T have less similarity to classical logic than RM has. The positive fragments of these logics were given a semantics. In [78], which was accompanied by two other papers, [77] and [79]. R, E and T may be thought of as logics obtained by successively excluding certain axioms from a suitably chosen axiomatization of classical logic. (Of course, this means that we overlook that all these are different logics with their own languages.)

The semantics for the modal logics K, T, B, S4 and S5 showed that some axioms necessitate that the accessibility relation possesses certain properties. For. Instance, \(\square \varphi \supset \varphi \) requires the accessibility relation to be reflexive; on the other hand, the axiom permits the canonical accessibility relation to be proved reflexive. (In the modal logic literature, the. Investigations. Into how modal axioms and conditions on the accessibility relation are related has become to be known as correspondence theory.) Correspondences between axioms. In relevance logics and conditions on the ternary accessibility relation were considered. In [63]. Furthermore, it was realized that some of those conditions have a strong resemblance to combinatory reduction axioms. Mares and Meyer. In [60] also emphasize such connections between relevance and combinatory logics —. In view of later developments of connections between relevance logics and extended theories of type assignment.

It had been known for a long time that R’s implicational fragment, R →, which was. Introduced by Church. In [26] (with another label), comprises the principal type schemas for the combinators B, W, C and I. Similarly, T → corresponds to B, B ′, W and I (or B, B ′, S ′ and I, if contraction is replaced by a form of the distributivity of → over →). E → is more complicated, because the restricted axioms (such as restricted permutation, restricted conditioned modus ponens and restricted assertion) require that an argument of a combinator is typed with a non-atomic simple type. As a result the combinators that have these axioms as their types, which figure. Into formalizations of E →, turn out not to be proper. For example, restricted assertion, (φ→ψ)→((φ→ψ)→χ)→χ corresponds to a combinator, denoted by 1. In [11], the axiom of which, for example, can be described by \(\mathsf {1}xy\vartriangleright y(\mathsf {B}^{\prime }\mathsf {I} x)\).

Operators on Boolean algebras, as defined. In [48], are everywhere monotone operations, which is not a serious limitation on the operations that can be considered, because of the. Interplay between negation and the other operations. Roughly speaking, an operation that is anti-tone. In some argument places can be equivalently replaced by an everywhere monotone one. Ultrafilters of Boolean algebras are prime, but. In the semantics for R, or for the other major relevance logics, the points are prime filters, which are,. In general, not absolutely maximal. At the same time, the (original) De Morgan negation of relevance logics does not support similar definability results. Thus, finding a suitable modeling of → from a ternary accessibility relation was important,. In particular, because relevance logics focus on relevant implication and entailments.

Some substructural logics differ from the major relevance logics. In that ∧ and ∨ do not distribute over each other. Examples. Include the non-distributive version of R, LR, which was. Introduced. In the process of. Investigations. Into the decidability of R, and linear logic, LL.

Two generalizations of Stone’s representation for Boolean algebras to distributive lattices are given. In [83] and. In [72], the latter of which has been more. Influential and applicable. In the semantics of substructural logics. A reason for this might be that the addition of a partial order to a topology is unproblematic when the canonical frame comprises theories, which can be ordered straightforwardly by the subset relation.

The representation theory for (general) lattices, that is, for lattices that are not required to be distributive or even modular, is more “chaotic.” Of course, each proposed representation supports the respective theorems, however, it is less clear which of them (if any) should be the favored one, when additions of further operations, relative simplicity and other similar aspects are taken. Into account too.

An easy way to generalize prime theories (or prime filters) is to drop primeness. (Filters and theories as well as ideals and co-theories may be used. Interchangeably, because they are “essentially the same”. In a mathematical sense, though the algebraic objects are a type-level higher.) Primeness is very useful. In the modeling of ∨, however,. In a lattice that is not distributive there may be too few prime filters for them to be useful. To put it. Informally, even if ∧ and ∨ do not distribute over each other, they are still connectives. In the logic; therefore, they need to be modeled somehow.

Urquhart. In [87]. Introduced a doubly ordered topological space. A pair of Galois functions, l and r are defined from the two pre-orders, \(\sqsubset _{1}\) and \(\sqsubset _{2}\), as. In (1) and (2).

  1. (1)

    \(l(X)=\{\,y\colon \forall x\,(y\sqsubset _{1}x\Rightarrow x\notin X)\,\}\)

  2. (2)

    \(r(X)=\{\,y\colon \forall x\,(y\sqsubset _{2}x\Rightarrow x\notin X)\,\}\)

The sets that carry the model are the Galois-closed sets. The topological space is compact and disconnected with respect to both pre-orders, which means that it is totally order disconnected with respect to both pre-orders where the separating set is Galois-closed, and both that set and its l image are closed. In the topology. These doubly ordered topological spaces have to satisfy two further conditions, one of which is connected to the. Intricacies of modeling ∨ on Galois-closed sets.

The usual operations that stand. In for ∧ and ∨. In a model comprising sets are. Intersection and union (or vice versa). The choice of prime theories ensures that unions of sets of prime theories, that are propositions, represent disjunctions of propositions, because non-prime theories do not need to be added. In — they are all excluded from the set of situations by definition. On the other hand, if a representation contains only one sort of objects, then no matter what those are, the two set-theoretical operations, ∩ and ∪ cannot be used at once to represent ∧ and ∨, because they distribute over each other.

An idea that goes back at least to [23] is to use a pair of Galois functions, let us say f and g. Then the lattice operation meet can be mapped. Into. Intersection, whereas the other operation, join is mapped. Into the closure of union. A bit more formally and more generally, let us take a pair of ordered sets 〈X,≤ X 〉 and 〈Y,≤ Y 〉, that are linked by a pair of order. Inverting functions g:X→Y and f:Y→X, where (G) holds.

(G):

x≤ X f(y) iff y≤ Y g(x)

Taking the set of Galois-closed elements. In X, the closure of Z, where Z⊆X is the set of closed elements that are closures of elements that belong to Z. Then, a lattice of the closed subsets of X can be constructed by taking intersection for meet, and f(g Z 1∩g Z 2) for join. The latter operation turns out to be the closure of the union of Z 1 and Z 2. Other topological representations of lattices, which utilize Galois-closed sets. In some way can be found. In [46] (Stone spaces),. In [16, Ch. 9] (inclusion spaces and centered spaces).

The appropriate doubly ordered topological space of a lattice. In [87] is built out of certain pairs of filters and ideals, namely, of maximally disjoint filter–ideal pairs. That is, the filter is maximal (in the ⊆ ordering on filters) with respect to not. Intersecting the ideal, and the other way around for the ideal. It is not difficult to prove that the elements of these pairs are join-irreducible filters and meet-irreducible ideals.

Philosophically speaking, such a pair can be thought to contain both positive and negative. Information about a situation — without the. Information being contradictory. Moreover, there is no similar pair that could contain more. Information, either from the point of view of the theory or from the point of view of the co-theory.

Given this characterization of the situations, a natural question to ask is whether the maximality is a necessary condition. It is not difficult to prove that maximally disjoint filter–ideal pairs do not need to “exhaust” the lattice, that is, there can be elements. In a lattice of which no. Information is available, and because of the maximality, it is clear that the pairs cannot be “improved”. In this respect. Maximality,. Indeed, may be omitted without the loss of the representation result. It is also worth pointing out that if the lattice is distributive, then the maximally disjoint filter–ideal pairs provide complete. Information about a situation; more technically speaking, all join-irreducible filters are prime filters and all meet-irreducible ideals are prime ideals. The converse. Inclusions are always true, which means that the pairs are embellished versions of prime filters, when the lattice is distributive.

Join-irreducible filters are usually defined by saying that they are not. Intersections of two other filters. Of course, this is a perfectly good definition, however, it appeals to objects (i.e., other filters), that are not given or determined by the join-irreducible filter itself. Prime filters, on the other hand, can be defined without appealing to anything outside of the filter. This distinction may be philosophically. Interesting, and it may explain why filters without qualifiers appear to be an easier generalization of the notion of prime filters.

Dunn. In [34]. Introduced gaggle theory, which provides a framework for semantics for a wide range of logics — as shown. In [35, 36] and [16]. Gaggles (i.e., generalized Galois logics or ggl’s) are generalizations of Boolean algebras with operators. \(\lozenge \) —. In the standard semantics of normal modal logics — is modeled using the existential image of a binary accessibility relation, whereas ∘ —. In the standard semantics of relevance logics — is the existential image of a ternary accessibility relation, as. In (3). Then, the. Interpretation of →, which is a residual of ∘, is defined. In a model by a universally quantified formula, as. In (4).

  1. (3)

    A∘B={ z:∃x ∃y (R 1 x y z∧x∈A∧y∈B) }

  2. (4)

    A→B={ x:∀y ∀z ((R 2 x y z∧y∈A)⇒z∈B) }

The properties of the connectives can be seen to determine their modeling. In the framework provided by gaggle theory. It is well-known that \(\lozenge \) and \(\square \). In normal modal logics can be modeled by one accessibility relation, which should not be surprising, given the. Interdefinability of these connectives. An important. Insight of gaggle theory is that certain connectives can be modeled by the same accessibility relation even if one cannot be expressed. In terms of the others. That is,. Interdefinability is not a necessary condition for a shared accessibility relation. For example, ∘ and →,. In the positive fragments of relevance logics, can be modeled from one ternary accessibility relation (together with ←. In B + and T +). Indeed, R 1 and R 2. In (3) and (4) above are the same relation. A key concept is abstract residuation — or yet more generally, colligation — between operations. These relationships join operations. Into families, and yield further properties for the operations such as their distribution and tonicity types, depending on context.

The concrete modeling of a (general) lattice impacts how ∘, → and other. Intensional operations can be modeled. If the model is based on Galois-closed sets, then it is natural to define each operation by a universal formula, because g Z 1∩g Z 2 is the. Intersection of certain sets. This is how a semantics for LL, and for several other logics is defined. In [1]. Despite appearances, this semantics generalizes the semantics for relevance logics, because. In a distributive lattice the union of upward closed sets of prime filters could be replaced equivalently by the. Intersection of downward closed sets of prime ideals. It is fortunate that either prime theories or prime co-theories suffice, and traditionally, the former are. In the center of attention. It has been pointed out. In [1] that maximality could be omitted from maximally disjoint filter–ideal pairs. A concrete example of a semantics based on disjoint filter–ideal pairs for punctual logic (which was. Introduced. In [6]) may be found. In [16, Ch. 3].

Galois-closed sets can be created from a polarity,. In the sense of [23], on a single partially ordered set. The. Interest. In this idea is that the set of filters is partially ordered by ⊆ and the Galois-closed sets can be. Independently characterized as the upward closed sets that have their. Intersection as their element. A semantics for the minimal substructural logic LS was defined based on this idea. In [15]. Further applications of this idea may be found. In [16, Ch. 3 and Ch. 9].

The original LC calculus. In [38] did not contain ∧ or ∨, which makes the definition of a semantics simpler. In the sense that there are plenty of theories (i.e., cones) available. At the same time, these theories do not have some desirable properties. Filters, which exist if there is conjunction. In the language, can be generalized to cones (i.e.,. Increasing sets), however, an. Intermediate step is to consider downward directed upward closed sets. Directed sets are also important. In theories of computation, hence, it is perhaps, not surprising that they turned out to be the suitable situations for the semantics of structurally free logics, where combinators are essential. A complete combinatory basis has to contain a combinator which produces at least two copies of at least one of its arguments. S (with axiom \(\mathsf {S} xyz\vartriangleright xz (yz)\)) and W (with axiom \(\mathsf {W} xy\vartriangleright xyy\)) are, perhaps, the best known duplicators; and the already mentioned S ′ (with axiom \(\mathsf {S}^{\prime }xyz\vartriangleright yz (xz)\)) is another example. A semantics for LC was given. In [38] using downward directed cones.

Combinators are constants, and this likens them to t and its cousins, T, f and F. By and large, it is clear that these distinguished elements have to be modeled by subsets of situations. However, the specific properties of these constants are revealed by their. Interaction with each other or with the (non-zero-ary) connectives. For example, if a logic is not prime (when ∨ is its connective), then there can be no single situation that generates the modeling of t; or if F is. In the language of LC, then ∘ cannot be a normal operation provided that cancellators are not excluded. Gaggle theory provides the conceptual framework to deal with such and other questions too, some of which are. Investigated. In detail. In [16].

5 Decidability and Complexity

Views concerning the desirability of a logic being decidable vary. One could, perhaps, say that classical propositional logic is so easy to learn, because it is decidable. However, even. In that case, the best decision procedure is thought to be unfeasible, because it is a co-NP-complete problem. On the other hand, it may be reasonable to claim that a sufficiently refined logic is likely to be (or outright must be) undecidable already at the propositional level — unlike. In classical logic, where undecidability shows up only at the first-order level.

The decidability of E → and R → was resolved. In [52] soon after those logics were singled out. The decidability results for the negation–implication fragments followed quickly. This might have generated a certain expectation as to the decidability of R and E (and perhaps, of T too) to be solved easily. Alas, the problem turned out to be difficult: many experts. In relevance logics tried to solve it, and the only proof of the undecidability that exists so far (see [88] and [91]) is far more difficult to follow than a proof of the undecidability of classical first-order logic. We only mention here that the word problem of a semigroup is reduced to provability. In an R theory. Then after further considerations, the undecidability follows for E and T too. Urquhart. In [88] (see also [3, §65]) shows that the deducibility problem all the way from T W + “upward” (to the logic determined by the models constructed. In the proof) is undecidable.

The logic of ticket entailment occasionally gets less attention that E and R do. T is a well-motivated logic,. In which the idea about the distinction between laws and facts, and their respective roles. In reasoning are captured. This is emphasized. In the Fitch-style natural deduction formulation of T →, where laws must precede facts. Despite the elegance of T →, its decidability turned out to be one of the last decidability problems. In the area of relevance logics among those that were conceived at about the same time when R → and E → were shown to be decidable. The decidability problem of T → was open for over 50 years.

Bimbó and Dunn in [19] and [20] present a solution that utilizes Kripke’s decidability proof for R → together with the sequent calculus , which is an extension of \(LT_{\rightarrow }^{\boldsymbol {t}}\) from [11]. The two new rules are “purely combinatorial,”. In the sense that they do not. Introduce a new connective, though one of them. Introduces t, for which there is already an. Introduction rule. In \(LT_{\rightarrow }^{\boldsymbol {t}}\).

$$\frac{\Gamma[{\Delta}]\vdash\varphi}{\Gamma[{\Delta};\boldsymbol{t}\,]\vdash \varphi}\,\,(\mathsf{K}_{\boldsymbol{t}}\vdash) \qquad \frac{\Gamma[{\Delta};\boldsymbol{t}\,]\vdash\varphi}{\Gamma[\,\boldsymbol{t};{\Delta}]\vdash \varphi}\,\,(\mathsf{T}_{\boldsymbol{t}}\vdash) $$

T is definable as C I. In the labels for the rules, the combinators are subscripted with t to. Indicate that the rules are not applicable to arbitrary structures; rather one of them,. In a specific place, must be the. Intensional truth constant. This calculus also has the cut property — despite the latter two rules imposing limitations on the shape of structures to which they are applicable.

The rule (K t ⊩). Introduces t as if it were a dual identity combinator. Of course, if there is a left and a right identity element for a binary connective, then the “two” identities are the same. Looking at the addition of the two rules algebraically, they make t. Into a left-right lower-upper identity, and this turns the logic of ticket entailment. Into the logic of relevant implication. That is, the calculus captures \(R_{\rightarrow }^{\boldsymbol {t}}\), which makes this calculus suitable to re-create cut-free irredundant proofs of \(R_{\rightarrow }^{\boldsymbol {t}}\) and \(T_{\rightarrow }^{\boldsymbol {t}}\) theorems.

The multiplicative–additive fragment of linear logic (or MALL) had been known to be decidable for a long time, because its decidability is a consequence of the decidability of lattice-R (LR), which was proved. In [61]. Linear logic’s unique feature is the modalization of thinning and contraction. Perhaps, because of the. Interaction between the exponentials and the structural rules, the decidability of MELL, the multiplicative–exponential fragment remained unresolved for nearly 30 years. This logic was proved decidable. In [8] using a suitable modification of the Curry–Kripke proof technique (which was used to prove R → and E → decidable). The latter is based on the. Insight that the possibility of contraction is created by applications of rules; hence, the contraction rule may be forfeited, if a limited amount of contraction is part of the operational rules. The decidability of full propositional linear logic has been proved. In [22]. Lambek calculus with contraction is also decidable, and it has been proved. In [14, Ch. 9].

Complexity theory concerns computational problems. In general, however, a seminal result about NP-completeness (in [27]) concerns the satisfiability problem of a logic, namely, of classical propositional logic. The simplicity of classical logic that I stated earlier is vindicated by several results about the complexity of substructural logics (that are decidable) compared to the complexity of classical propositional logic.

Urquhart. In [89] and [90] proved upper and lower bounds for some decidable relevance logics. Kripke’s decision procedure for R → is elegant, but its space complexity is staggering: it requires an exponential amount of space. In the length of. Inputs. [89] also proved that the size of the search tree resulting from an application of the R → decision procedure is primitive recursive. In the Ackermann function. The search tree comprises “backward proof” attempts. In the sequent calculus for R →. In which the contraction rule is omitted. In favor of a left-introduction rule for → that builds. In a sufficient amount of contraction. (Detailed presentations of versions of this calculus may be found. In [33] and [19].) The same lower bound applies to the conjunction–implication fragments of R, and of logics between T →∧ and R →∧.

A decision procedure for LR was implemented as the program Kripke as described. In [85]. Urquhart [90] showed that there is no primitive recursive decision procedure for L R +, the positive fragment of LR. The same bound applies to LR, and to the implication–conjunction fragments of logics between T and R. The upper bound of the complexity of the decision procedure for LR is proved to be primitive recursive. In the Ackermann function.

6 Some Other Topics

Sequent calculi are preeminently useful to prove conservative extension results — provided that the calculus is well-behaved, that is, the cut theorem has been proved. The sequent calculus formalizations of various fragments of relevance logics that we already mentioned show that those logics are put together. In a reasonable way, and with suitable translations. Into axiomatic and natural deduction systems, prove similar results for the latter kinds of calculi.

Booelan algebras are extremely well-studied and well-understood structures nowadays. Although the main relevance logics have ∧ and ∨ distributing over each other, De Morgan negation is not a complementation, and the major relevance logics do not algebraize. Into a Boolean algebra with operations. The addition of a “classical” negation to relevance logics, especially to R, was thought to be an exciting philosophical question.

The papers [64] and [65] show that a “classical” negation, denoted by ¬, can be added to R + without the resulting logic becoming a notational variant of classical logic. Furthermore, the original negation of R (∼) can be defined if a unary connective ∗ is added to the language, that is, ∼φ is ¬∗ φ. The notation for the new connective is similar to the unary operation. In the set-theoretical semantics of relevance logics (which enters. Into the. Interpretation of formulas of the form ∼φ), and the. Interpretation of ∗ φ. In the situation x goes via the. Interpretation of φ at the situation x ∗. Similar conservativity results were obtained for some other relevance logics. Including B. In [62].

Mares. In [59] proved that the addition of ¬ to E is not conservative. The extension CE is obtained by adding formulas of the form φ→ψ to E, where ¬φ∨ψ is an. Instance of a classical tautology. \(\square \) is defined as usual. In E, and then it is proved that the modal K axiom,. In the form \(\sim \square (\sim p\lor q)\lor \sim \square p\lor \square q\) (for some propositional variables p and q). In not an E theorem, whereas \(\sim \square (\sim \varphi \lor \psi )\lor \sim \square \varphi \lor \square \psi \) is a theorem of CE, because the normal modal logic S4 can be embedded. Into CE.

Lastly, I mention that there seems to be a renewed. Interest. In the Lambek calculi and related systems. Both the associative and the non-associative Lambek calculi are decidable leading to the question of their complexity, as. In [71]. Linguists, for. Instance. In [67],. Introduced some new extensions of the basic calculi to deal with a range of natural language phenomena such as VP ellipsis, pied-piping and gapping. [66] dualizes the Lambek calculus, and. Includes certain distribution like structural rules, which allows the modeling of limited permutations. In natural languages without having the full power of a permutation rule. In the calculus.Footnote 1