Modal Translation of Substructural Logics
Takis Hartonas
TL;DR
This paper extends modal translation techniques to all substructural logics, including non-distributive systems, enabling classical interpretations and transfer of key logical properties.
Contribution
It demonstrates that every substructural logic can be embedded into a sorted, residuated modal logic, generalizing previous translations and covering non-distributive cases.
Findings
Every non-distributive logic is a fragment of a sorted, residuated modal logic.
The translation provides a classical interpretation of non-distributive propositional calculi.
Results like compactness and decidability transfer seamlessly via the translation.
Abstract
In an article dating back in 1992, Kosta Do\v{s}en initiated a project of modal translations in substructural logics, aiming at generalizing the well-known G\"{o}del-McKinsey-Tarski translation of intuitionistic logic into {\bf S4}. Do\v{s}en's translation worked well for (variants of) {\bf BCI} and stronger systems ({\bf BCW}, {\bf BCK}), but not for systems below {\bf BCI}. Dropping structural rules results in logic systems without distribution. In this article, we show, via translation, that every substructural (indeed, every non-distributive) logic is a fragment of a corresponding sorted, residuated (multi) modal logic. At the conceptual and philosophical level, the translation provides a classical interpretation of the meaning of the logical operators of various non-distributive propositional calculi. Technically, it allows for an effortless transfer of results, such as…
| iff | ||
| iff | ||
| iff | ||
| iff | and | |
| iff | and | |
| iff | ||
| iff | ||
| iff |
| iff | ||
| iff | ||
| iff | ||
| iff | ||
| iff |
| = | = | ||||
| = | = | ||||
| = | = | ||||
| = | = | ||||
| = | = | ||||
| = | = | ||||
| = | = | ||||
| = | = |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = | |
| ST | = |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Modal Translation
of Substructural Logics
Chrysafis Hartonas
Department of Computer Science and Engineering,
University of Applied Sciences of Thessaly (TEI of Thessaly), Greece
Abstract
In an article dating back in 1992, Kosta Došen initiated a project of modal translations in substructural logics, aiming at generalizing the well-known Gödel-McKinsey-Tarski translation of intuitionistic logic into S4. Došen’s translation worked well for (variants of) BCI and stronger systems (BCW, BCK), but not for systems below BCI. Dropping structural rules results in logic systems without distribution. In this article, we show, via translation, that every substructural (indeed, every non-distributive) logic is a fragment of a corresponding sorted, residuated (multi) modal logic. At the conceptual and philosophical level, the translation provides a classical interpretation of the meaning of the logical operators of various non-distributive propositional calculi. Technically, it allows for an effortless transfer of results, such as compactness, Löwenheim-Skolem property and decidability.
Keywords: Gödel translation, Substructural Logics, Resource Conscious Logics, Non-Distributive Logics, Representation of Lattice Expansions, Sorted Modal Logic
1 Introduction
In 1933, Kurt Gödel published a paper [28] he had presented the year before in the Mathematics Colloqium in Vienna, chaired by his former teacher, Karl Menger. In his presentation and paper Gödel proposed his well-known interpretation of Intuitionistic Logic (IL) into a certain modal extension of Classical Propositional Logic (CPL), now widely known as Lewis’s system S4. Gödel proposed to translate every IL formula to an S4-formula by prefixing a to every subformula of . He proved that if IL, then S4 and he advanced the conjecture, later proven by McKinsey and Tarski [51], that the converse also holds. Grigori Mints [52] complemented the result by providing a characterization of modal formulas equivalent in S4 to GMT-translations of intuitionistic formulas. Grzegorczyk [32] showed that adding to S4 the axiom (G) \Box(\Box(p\mbox{\rightarrow}\Box p)\mbox{\rightarrow}p)\mbox{\rightarrow}p, the (now known as) Grzegorczyk system Grz = S4+G is strictly stronger than S4, it is not contained in S5 and the same result about the GMT-translation of IL into Grz is provable. This was also shown to be true for McKinsey’s system S4.1 = S4+(). This quickly led to the investigation of logics, variably called super-intuitionistic, or intermediate logics between IL and CPL and their modal companions, i.e. modal logics containing S4, cf. [47, 48, 12, 21, 5], in some cases logics between S4 and S5 [16], which culminated in the Blok-Esakia theorem, independently proven by Blok [8] and Esakia [21]. The topological interpretation of S4 [49, 50, 51], interpreting the box operator as an interior operator, provided furthermore the background for investigating dualities between modal companions of superintuitionistic logics and topological spaces [5]. In all of the above cases distribution is assumed and topological dualities investigated are based on the Priestley [59] duality for distributive lattices, or on the Esakia [21, 20, 22] duality for Heyting algebras.
For logics without distribution, Goldblatt [29] provided a translation of Orthologic O into the B system of modal logic. This quickly led to modal approaches to quantum logic [58, 4], as an immediate application. Goldblatt’s result is specific to Orthologic and it was Kosta Došen [15] who embarked in a project of extending the GMT translation to the case of substructural logics. Došen’s main result is an embedding of BCI (to which he refers as BC), BCK, BCW with intuitionistic negation into S4-type modal extensions of versions of BCI, BCK, BCW, respectively, all equipped with a classical-type negation (satisfying double negation and De Morgan laws). The result is established by proof-theoretic means, but the approach does not apply uniformly to substructural logics at large. Indeed, Došen points out that difficulties arise when dealing with weak systems such as the non-commutative and/or non-associative full Lambek Calculus (N)FL (see [15], Introduction, as well as end of Section 4).
A parallel investigation into subintuitionistic logics has also developed, initiated by Corsi [14] in 1987 and then by Restall [60] in 1994, followed up by Celani and Jansana [11] and others. Unlike substructural logics which are proof-theoretically specified, subintuitionistic logics are typically specified in a model-theoretic way, as the logics of Kripke frames for intuitionistic logic with some frame conditions weakened, or dropped. Proof-theoretically, this is reflected as a weakening of the axiomatization of intuitionistic logic. In all cases, however, and as it is typical in mainstream relevance logic [1, 2], distribution is explicitly forced in the axiomatization and we therefore leave these outside the scope of our investigation. Our focus, instead, is with modal translations of non-distributive logics, arising as the logics of normal lattice expansions.
Normality for a lattice operator means that it is an additive operator [42, 43] (distributing over binary joins in each argument place), where for each , and designates the opposite lattice of (usually designated by ). The tuple will be referred to as its distribution type. For example, boxes and diamonds are normal operators , . Implication is a normal operator with distribution type , in other words it is an additive operator \mbox{\rightarrow}:\mathcal{L}\times\mathcal{L}^{\partial}\longrightarrow\mathcal{L}^{\partial}.
In this article, we restrict attention to the hierarchy of substructural logic systems displayed in Figure 1
and we present a uniform translation of the logics, proven here to be full and faithful. The target system of the translation is a corresponding sorted, residuated (multi) modal logic. Though we do not treat here Grishin’s dual operators [31], it will be obvious that our approach is easily extendible to the Full Lambek-Grishin (FLG) system.
The main structure of the argument is the following. We insist that a substructural logic SUB and its modal companion logic sub.ML2 are interpreted over the same class of frames . For modal definability (of the frames for substructural logics) reasons, we remove restrictions typically assumed to hold, such as frames being separated and reduced (RS-frames [26]). Models , are defined for SUB and sub.ML2, respectively, and a translation and co-translation of sentences of the language of SUB into the sorted language of sub.ML2 are defined. We then prove that in SUB iff iff in sub.ML2. To transfer the result on the provability relation, completeness theorems for each of SUB and sub.ML2 need to be proven, hence obtaining that in the proof system for SUB iff iff \psi^{\circ}\mbox{\medvert!!!!\sim}\hskip 1.5pt\varphi^{\circ} in the sorted proof system for sub.ML2, thereby establishing that the translation is full and faithful.
Lacking distribution, substructural logics are interpreted [63, 26, 13] in sorted frames with additional structure (to account for the residuated operators). As we detail in Section 2.1, the dual complex algebra of the frame can be taken to be either the formal concept lattice of the frame (equivalently, its complete lattice of Galois-stable sets), or the sorted, residuated modal algebra \largediamond:\powerset(X)\leftrightarrows\powerset(Y):\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt associated to the frame, where the residuated operators are generated by the complement of the Galois relation of the frame. Additional frame relations generate operators both on powerset algebras and on sets of Galois stable sets where, roughly, the latter are the Galois closures of the former (see [39, 36, 37]) and exploiting this connection leads to the possibility for a modal translation of substructural (non-distributive, more generally) logics.
Logically, the sorted, residuated modal logics we consider in this article arise as a synthesis in the sense of [10] of classical propositional logic and the logic of residuated Boolean algebras, combined together by means of a logical adjunction (a pair of sorted, residuated operators).
From an algebraic point of view, we consider the logics of sorted, residuated modal algebras , iff , where both are Boolean algebras and where is moreover a residuated Boolean algebra [44] with operators , i.e. iff iff . If the full Lambek-Grishin calculus is to be considered, then both are residuated Boolean algebras. These structures serve as algebraic models to the sorted, residuated modal logics we consider in this article. Note that the set is a meet sub-semilattice of which has a full lattice structure (non-distributive, in general) when defining joins in by setting . Similarly for the set and they are dually isomorphic . In the case of interest in this article, the closure operator carries over the residuation structure of to . More precisely, our representation results [39, 37] have established the following:
Theorem 1.1** ([39, 37]).**
Every residuated lattice \mathcal{L}=(L,\wedge,\vee,0,1,\mbox{\leftarrow},\circ,\mbox{\rightarrow}) is a sublattice of the lattice of a sorted, residuated modal algebra where, moreover, is a residuated Boolean algebra and where the lattice operator is the closure of the restriction of on , while its residuals \mbox{\leftarrow},\mbox{\rightarrow} are simply the restrictions of the residuals of on .
The target system of the translation can be therefore taken to be a corresponding sorted, residuated (multi) modal logic. Options exist as to the specification of the signature of the target companion modal logic and, in accordance with the previous discussion, we opt for the following sorted modal language
[TABLE]
for the full Lambek-Grishin (FLG) calculus, where are residuated binary diamonds, with residuals and , respectively. However, for the purposes of this article, focusing on the systems of Figure 1, we restrict to the sublanguage without the logical operators.
As an application for the usefulness of the result, we extend the standard translation of modal logic into first-order logic to the two-sorted case. Using established results [19, 53, 30, 9] for sorted first-order logic and for its two-variable fragment we obtain compactness, finite model property and decidability, as well as the Löwenheim-Skolem property for just about any substructural logic. A complexity bound for the satisfiability problem of the two-variable fragment of first-order logic is also known [9], which can be probably improved for the particular fragments at hand.
The structure of this article is as follows.
Section 2 briefly goes through some necessary preliminaries, presenting the basics of sorted frames, running through a quick presentation of substructural logics and reminding the reader of the basics on canonical extensions of lattice expansions.
Section 3 studies sorted frames with relations and their associated complex algebra (in fact, algebras (plural), as both a sorted algebra and an algebra of Galois stable sets are of significance) and it draws on recent work by this author on representation and duality for normal lattice expansions [39, 41, 36, 37].
Section 4 specifies the proposed modal translation and the argument that the translation is full and faithful is detailed. The main structure of the argument is that given a substructural logic SUB and its sorted modal companion logic sub.ML2 a translation of SUB-sentences is defined and it is shown that in some sub.ML2-model iff in an associated SUB-model (produced by just tampering with the interpretation function of and allowing only Galois stable sets to be in its range). To conclude from this that the sequent is provable in SUB iff its translation is provable in the companion logic sub.ML2, we establish soundness and completeness theorems of both SUB and sub.ML2 over the same class of frames.
Some consequences regarding properties of the logics we consider are then presented in Sections 5 and 6. Pointers for generalization of the results to just about any non-distributive logic are suggested in the Conclusions section 7.
2 Review and Technical Preliminaries
2.1 Sorted Frames
Single-sorted modal systems cannot express a fact such as that the set of worlds (states, points) is partitioned in a number of subsets, which is typical of domains populated by distinct types of individuals. Sorted modal logic arises precisely when taking into consideration the typing of the domain of the frame. Many-sorted modal logic has so far received little attention. Yde Venema’s [64], preceded by Balbiani’s modal multi-logic of geometry [3], employs a two-sorted system whose intended application domain is the projective plane, the two sorts being points and lines. Steven Kuhn’s PhD dissertation [46], supervised by Kit Fine, is perhaps the only source where a comprehensive study of many-sorted modal logics is carried out, dating back in 1976 and with a lot having changed in the meantime, as far as the theory of modal logic is concerned. Venema and Balbiani’s work is developed in the context of spatial logics, where individuals of distinct sorts populate the application domain of interest. Two-sorted frames have been the focus of attention in other contexts, as well, such as Wille’s formal concept analysis (FCA) [65] and Hardegree’s logic of natural kinds [33], but they were not accompanied by an interest in the two-sorted modal logic of the frames, though the approach seems to suit the needs of FCA extensions such as temporal FCA [66], or rough FCA [45]. Explicitly related to modal logics are also the sorted frames of [6, 7], called step-frames, which are structures where and , with a sorted diamond operator , used in defining approximations of free algebras of modal logics.
The class of two-sorted frames we consider consists of triples , where are non-empty sets and is a binary relation (to be called the Galois relation of the frame). Two-sorted frames may be concretely regarded as information systems, or object-attribute systems, where is the set of formal objects, is the set of formal attributes of objects and is the attribute assignment map. In general, a frame will have additional relations , of various sorting (contained in some product with factors , ).
Sorted frames generalize plain Kripke frames. Indeed, if and is the non-identity relation , then both maps of the Galois connection (1) are the set-complementation operator {}\mbox{{}^{\upVdash}}U=-U=U\mbox{{}^{\upVdash}}.
The Galois relation of the frame generates a Galois connection (hence its naming)
[TABLE]
and, by composition of the Galois maps, a closure operator on each of and . The relation iff \{x\}\mbox{{}^{\upVdash}}\subseteq\{z\}\mbox{{}^{\upVdash}} iff is easily seen to be a preorder on . Similarly for . A frame is separated (clarified) [25] if the preorder is a partial order. Separation turns out to be necessary in order to prove discrete, or Stone dualities for various classes of lattices with operators [36, 37], but it will not be assumed for frames in this article. The reason for this is that our argument is mostly semantically based in that it requires that we interpret both the substructural and the sorted modal logic systems over the same class of frames and we wish to ensure modal definability of the frames (by the modal companion logics of the substructural systems we examine).
The closure operators can be equivalently regarded as obtained by composition of the residuated pair of maps generated by the complement of the attribute assignment map , i.e. {}\mbox{{}^{\upVdash}}(U\mbox{{}^{\upVdash}})=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond U and ({}\mbox{{}^{\upVdash}}V)\mbox{{}^{\upVdash}}=\largesquare\raisebox{-3.5pt}{\mbox{\Huge{\filleddiamond}}}V, where {}\mbox{{}^{\upVdash}}V=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt(-V),U\mbox{{}^{\upVdash}}=\largesquare(-U) and \largesquare=-\largediamond-,\;\raisebox{-3.5pt}{\mbox{\Huge{\filleddiamond}}}=-\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt-,
[TABLE]
Where is the complement of , the following conditions are assumed.
[TABLE]
The frame conditions (3) correspond to the inclusions \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0ptB\subseteq\raisebox{-3.5pt}{\mbox{\Huge{\filleddiamond}}}B and . This implies that \largesquare\emptyset=\largesquare(-X)=X\mbox{{}^{\upVdash}}=\emptyset and, similarly, \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\emptyset=\emptyset.
A subset of is Galois stable, or just stable, if {}\mbox{{}^{\upVdash}}(A\mbox{{}^{\upVdash}})=A (equivalently, if A=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond A). Dually, a subset of is co-stable if ({}\mbox{{}^{\upVdash}}B)\mbox{{}^{\upVdash}}=B (equivalently, B=\largesquare\raisebox{-3.5pt}{\mbox{\Huge{\filleddiamond}}}B). Stable and co-stable sets are -increasing. Indeed, if and , i.e. \{x\}\mbox{{}^{\upVdash}}\subseteq\{z\}\mbox{{}^{\upVdash}}, then from we obtain A\mbox{{}^{\upVdash}}\subseteq\{x\}\mbox{{}^{\upVdash}}\subseteq\{z\}\mbox{{}^{\upVdash}}, hence z\in{}\mbox{{}^{\upVdash}}(\{z\}\mbox{{}^{\upVdash}})\subseteq A, by stability of . Similarly for co-stable sets.
A formal concept [25] is a pair consisting of a stable and a co-stable set such that B=A\mbox{{}^{\upVdash}} (and then also A={}\mbox{{}^{\upVdash}}B). The formal concept lattice of the frame is the complete lattice of formal concepts, with operations defined by
[TABLE]
where meets and joins on the right hand side of the equations are taken in the complete lattice of (co)stable sets, where meets are set intersections and joins are closures of unions. Clearly, the formal concept lattice is isomorphic to the lattice of concept extents (the complete lattice of Galois stable subsets of ) and dually isomorphic to the lattice of concept intents (the complete lattice of the co-stable subsets of ).
For a frame , let be its formal concept lattice and be its associated sorted, residuated modal algebra. It is evidently only a matter of focus which algebraic structure we decide to consider as the complex algebra of the frame . The two algebraic structures are not unrelated and, in fact, is isomorphic to and it therefore sits inside as a meet sub-semilattice of .
Remark 2.1** (Notational Conventions).**
For a sorted frame , perhaps with additional structure, always designates the Galois relation. (\;)\mbox{{}^{\upVdash}},{}\mbox{{}^{\upVdash}}(\;) designate the maps of the induced Galois connection (1). The complement of will be consistently designated by and it generates a pair of residuated set-operators \largediamond:\powerset(X)\leftrightarrows\powerset(Y):\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt.
is the preorder on each of defined by \{x\}\mbox{{}^{\upVdash}}\subseteq\{z\}\mbox{{}^{\upVdash}}, for and, similarly, iff {}\mbox{{}^{\upVdash}}\{v\}\subseteq{}\mbox{{}^{\upVdash}}\{y\}, for .
We typically and consistently use to range over and to range over .
For in , or in , we let be the -upset, . Without separation in the frame, only implies that , without forcing that .
Given a (two-sorted) frame , a sorted frame relation is any relation , where for each , . To keep track of the various relations and their sorting we make the convention to indicate the sorting by an upper index, a string of ’s and ’s, with 1 pointing to and pointing to . Thus, for example, is a relation contained in the cartesian product . An -ary relation will be always written in the form .
The sets obtained by not filling one argument place will be written in the form . For a two place relation we write and , rather than and , respectively. Similarly, for a 3-place relation we write , rather than and , respectively, but we use when the second argument place is not filled.
2.2 A Substructural Review
Substructural logics arise from the Gentzen system LJ for intuitionistic logic by dropping a combination of the structural rules of exchange, contraction and weakening and expanding the logical signature of the language to include the operator symbols (fusion, cotenability), (reverse implication) and, often, a constant .
We let NFL be the system with all structural rules dropped (including the association rule), which is precisely the non-associative Full Lambek calculus. We write FL for the associative Lambek calculus. For we designate by the system resulting by adding to (N)FL the structural rules in (where abbreviates ‘contraction’, abbreviates ‘exchange’ and similarly for and ‘weakening’). With the exception of , which is precisely LJ, distribution of conjunctions over disjunctions and conversely does not hold, unless explicitly added to the axiomatization (an option typically taken by mainstream relevance logicians [1, 2]).
The algebraic semantics of these systems has been investigated by Hiroakira Ono, Nick Galatos [23, 57, 54, 55, 56] and several others.
An FL-algebra is a structure \langle L,\leq,\wedge,\vee,0,1,\mbox{\leftarrow},\circ,\mbox{\rightarrow},\mathfrak{t}\rangle where
is a bounded lattice 2. 2.
is a partially-ordered monoid ( is monotone and associative and is a two-sided identity element ) 3. 3.
\mbox{\leftarrow},\circ,\mbox{\rightarrow} are residuated, i.e. iff b\leq a\mbox{\rightarrow}c iff a\leq c\mbox{\leftarrow}b 4. 4.
for any ,
An FL-algebra is commonly referred to as a residuated lattice [24]. FL-algebras (residuated lattices) are precisely the algebraic models of the associative full Lambek calculus. By residuation, the distribution types of the operators are \delta(\circ)=(1,1;1),\delta(\mbox{\rightarrow})=(1,\partial;\partial) and \delta(\mbox{\leftarrow})=(\partial,1;\partial).
An FLe-algebra adds to the axiomatization the exchange (commutativity) axiom for the cotenability operator (in which case and coincide). It corresponds to the system BCI studied by Došen [15].
An FLew-algebra adds the weakening axiom , as well, in which case combining with commutativity follows. In addition, by , the identity holds in FLew-algebras. FLew-algebras are also referred to in the literature as full BCK-algebras, corresponding to full BCK-logic, resulting from BCK whose purely implicational signature is expanded to include conjunction and disjunction connectives, alongside the cotenability logical operator and the constants . Algebraically, they constitute the class of commutative integral residuated lattices [24].
Similarly, an FLec-algebra, adds the contraction axiom (a distinguished case of which is square increasingness ). FLec-algebras are also known as BCW-algebras.
The language of the Lambek Calculus (associative, or not) that we consider is displayed below,
[TABLE]
where we omit the constant , avoiding matters of secondary interest. The use of the names BCI, BCW and BCK is more widespread than the use of the names FLe, FLec, FLew due to their connection with type theory and the Curry-Howard isomorphism, where BCI, BCK, BCW designate restricted families of -terms and the combinators B,C,I,K,W correspond to the following Hilbert-style axiomatization of their pure implicational fragment.
[TABLE]
Proof systems for substructural logics can be found in the literature and we do not take the space to restate them here. The reader may wish to consult [63], for a Gentzen System, or [15] for a Hilbert-style axiomatization. In fact, for the purposes of this article we will be content with a proof system as a symmetric consequence system, with sequents of the form , directly encoding the corresponding algebraic specification.
Fragments of these systems are also of independent interest, corresponding for example to the logics of implicative (L,\leq,0,1,\wedge,\vee,\mbox{\rightarrow}), or bi-implicative lattices (L,\leq,0,1,\wedge,\vee,\mbox{\leftarrow},\mbox{\rightarrow}). Going in the other direction, extensions of these systems for example by various negation and/or modal operators are also of interest, but we shall not treat such extensions in the present article.
Contrasting to relational semantics, algebraic semantics and soundness and completeness for the systems are well established results in the substructural logics community, see for example [56, 24].
Lacking distribution, substructural logics are interpreted in sorted frames , where is a ternary relation with the indicated sorting type and is the Galois relation of the frame. Fusion and implication have been modeled in sorted frames by Gehrke [26] and then also by Dunn, Gehrke and Palmigiano [17], using RS-frames (separated (clarified) and reduced frames, in Wille’s sense [25]). For our argument of a full and faithful modal translation to go through we need to ensure that the class of frames we use is modally definable, since both the substructural systems and their companion modal logics are to be interpreted in the same class of frames, with respect to which completeness theorems should be derivable. For this reason we drop both restrictions of being separated and being reduced for frames.
Given a frame a model for the interpretation of the language of a substructural logic is equipped with a map , assigning a stable set (a concept extent) to propositional variables. An interpretation of sentences as formal concepts \overline{V}(\varphi)=(\mbox{[![\varphi]!]},\mbox{(!|\varphi|!)}) with extent and intent \mbox{(!|\varphi|!)}=\mbox{[![\varphi]!]}\mbox{{}^{\upVdash}} is then recursively defined. The satisfaction and co-satisfaction relations are defined by setting, for and , iff x\in\mbox{[![\varphi]!]} and iff y\in\mbox{(!|\varphi|!)}. The recursive definition of the interpretation is specified by the appropriate clauses for and , shown in Table 1. The relation involved in the semantic clauses is defined by setting R^{\partial 11}zz^{\prime}=(R^{111}zz^{\prime})\mbox{{}^{\upVdash}}.
For a sentence it suffices to specify either a satisfaction, or a co-satisfaction clause, since in the interpretation \overline{V}(\varphi)=(\mbox{[![\varphi]!]},\mbox{(!|\varphi|!)}) we have \mbox{[![\varphi]!]}={}\mbox{{}^{\upVdash}}\mbox{(!|\varphi|!)} and \mbox{(!|\varphi|!)}=\mbox{[![\varphi]!]}\mbox{{}^{\upVdash}}. Hence both iff , as well as iff always obtain.
Table 2 displays relational constraints on frames, to be considered in the sequel.
The reader familiar with the literature on relevance logic will recognize them as the standard frame conditions relevance logicians consider on frames [1, 2, 18] and some of our related proof obligations come across the same type of difficulties as encountered in proving completeness theorems for relevance logic in relational semantics. An exception is the relational constraint (C3), corresponding to Weakening being assumed. In a Boolean setting (for the logics of residuated Boolean algebras) (C3) can be replaced by the condition , but this is too strong a requirement for the semantics of substructural logics.
Definition 2.2**.**
Taking the frame constraints of Table 2 in consideration, we distinguish the frame classes by the obvious criteria, detailed below:
- ) Unrestricted class of frames
- ) Frames where the constraint (C1) holds
- ) Frames where the constraints (C1) and (C2) hold
- ) Frames where the constraints (C1), (C2) and (C3) hold
- ) Frames where the constraints (C1), (C2) and (C4) hold
2.3 Canonical Extensions
Canonical extensions for bounded lattices were introduced by Gehrke and Harding [27], extending to the non-distributive case the notion of a canonical extension of Jónsson and Tarski [42, 43]. A canonical lattice extension is defined as a pair where is a complete lattice and is an embedding of a lattice into such that the following density and compactness requirements are satisfied
(density) is dense in , where the latter means that every element of can be expressed both as a meet of joins and as a join of meets of elements in
(compactness) for any set of closed elements and any set of open elements of , iff there exist finite subcollections such that
where the closed elements of are defined in [27] as the elements in the meet-closure of the representation map and the open elements of are defined dually as the join-closure of the image of . Existence of canonical extensions for bounded lattices is proven in [27] by demonstrating that the compactness and density requirements are satisfied in the representation due to Hartonas and Dunn [40] (though it is to be noted that the lattice representation argument of [40] is merely reproduced in [27], without attributing it to [40]).
The canonical extension construction is functorial. Indeed, recall from [27] that if is a canonical extension of a bounded lattice , and are its sets of closed and open elements, the and -extensions (where, following the notation of [27], designates the canonical extension of ) of a unary monotone map are defined in [27], taking also into consideration Lemma 4.3 of [27], by setting, for , and
[TABLE]
where in these definitions is identified with its isomorphic image in and is then identified with its representation image. Working concretely with the canonical extension of [40], the extension of a monotone map as in equation (4) and the dual -extension (not used in [27]) are defined by instantiating equation (4) in the concrete canonical extension of [40] considered here by setting, for and and where is a principal filter, a principal ideal and the closed elements are precisely the principal upper sets (for each of , ).
[TABLE]
From [34] recall that if is an -ary normal operator of distribution type , where (in other words is an additive operator), then we defined filter/ideal operators which, in the unary case are precisely the maps and (for a filter and ideal ). It can be then immediately observed that , if distributes over joins, and that if it distributes over meets (the cases of co-distribution being reducible to these two by considering as a map from to its opposite lattice , or the other way around). The -extension is obtained from the dual extension , by composition with the Galois maps, f_{\pi}({}\mbox{{}^{\upVdash}}\{y\})={}\mbox{{}^{\upVdash}}(f^{\partial}_{\sigma}({}\mbox{{}^{\upVdash}}\{y\})\mbox{{}^{\upVdash}})={}\mbox{{}^{\upVdash}}(f^{\partial}_{\sigma}(\Gamma y)), where the set \{{}\mbox{{}^{\upVdash}}\{y\}\;|\;y\in Y\} is the set of open elements of and {}\mbox{{}^{\upVdash}}(\;),(\;)\mbox{{}^{\upVdash}} designates the Galois connection generated by .
Besides serving as a means to construct the -extension of maps, as shown in [39, 41], point operators are used in [34] and in each of [39, 41] to construct relational structures dual to lattice expansions. Roughly, for each normal lattice operator , where , a canonical relation is defined by setting iff and a dual relation is then appropriately derived. The relations are then used to define operators on stable sets and on co-stable sets that are shown in [39, 41] to be the canonical (dual) extension of .
We conclude this section with considering the case where the represented lattice (expansion) is distributive, or a Boolean algebra. For the approach based on and extending the Hartonas-Dunn lattice duality [40], the canonical frames for distributive and Boolean algebras are the obvious subframes of the canonical lattice frame. Indeed, let be a lattice and assume it is a Boolean algebra. Let be the set of Galois-stable subsets of the Hartonas-Dunn dual canonical frame (the canonical extension of ) and let be its set of ultrafilters. It is not hard to see that the map defined by is an isomorphism of canonical extensions. Indeed, by uniqueness of canonical extensions [27], there is an isomorphism , commuting with the embeddings , , i.e. , for all . Given that by join density of principal filters any filter is , where we let designate a principal filter and that, letting , and since preserves both meets and joins, being an isomorphism, we obtain
[TABLE]
where in ‘’ designates filter inclusion. Given also join-density of the set of closed elements of (see Lemma 3.1, [36]) we obtain that for any stable set ,
[TABLE]
Stable sets are increasing, i.e. implies (see Lemma 3.1, [36]), hence .
The following lemma will be useful in the sequel.
Lemma 2.3**.**
Let be a Boolean algebra with a unary monotone operator . Let also be the Hartonas-Dunn canonical extension of considered merely as a lattice and let be the standard construction of the canonical (ultrafilter) extension of the Boolean algebra , after Stone [62]. Designate the canonical extension (-extension) of the map respectively by and . Then, the isomorphism is a homomorphism of lattice expansions, i.e. it commutes with the -extensions of , .
Proof.
For the purposes of this proof, let , , , for a filter and where designates filter inclusion, and and recall that it was argued above that . Letting and be the canonical embeddings of it is not hard to see that the intersection closure of is the collection of , with and, similarly, the intersection closure of is the collection of the sets , with . In other words, the sets of the form are the closed (filter) elements of and , respectively. By , the isomorphism of canonical extensions preserves closed elements (and similarly for open elements). Given the definition of the -extension of a monotone map in we obtain
[TABLE]
Similarly, considering the -extension of in we obtain by definition
[TABLE]
where iff iff iff . Hence we obtain that , as claimed. ∎
Using the fact pointed out in [27] that and , Lemma 2.3 extends readily to -ary maps that are either monotone, or antitone in their argument places.
3 Sorted Frames with Relations and their Logics
The extensions of ML2 that we consider arise as the logics of sorted frames with additional relations. Cases of interest include temporal formal contexts , where is a relation of temporal succession of (instances of) formal objects, of use in Temporal FCA [66], or contexts with an indiscernibility relation on formal objects, , arising in Rough FCA [45]. Frames of this type correspond to extensions of substructural logics with unary modal operators, which we do not discuss in this article.
We focus here on structures , where has the sorting type indicated by the superscript (with pointing to and to ), i.e. . With a spatial intuition, as in [64], can be understood, for example, as a colinearity relation for points in , iff , where is the incidence relation of the frame. We make no further assumptions about the accessibility relation , such as the ‘compatibility’ assumption made in [26, 13], because we wish to ensure modal definability of our frame classes. It is for the same reason that we do not assume that frames are separated and/or reduced.
3.1 Sorted, Residuated Modal Logics
Given a frame , the relation generates a classical binary additive operator on , defined in the standard way by
[TABLE]
It follows from the definition that distributes over arbitrary unions in each argument place and we let be its residuals in the algebra of subsets of , i.e. iff iff . Hence is a residuated Boolean algebra.
Lemma 3.1**.**
The residuals are defined by
- •
- •
Proof.
The proof is by the following calculation
[TABLE]
and since iff the claim for is true. Similarly, iff , then just change bound variables. ∎
Properties of the operator correspond to the relational constraints of Table 2.
Lemma 3.2**.**
The following hold
(C1) holds iff is associative 2. 2.
(C2) holds iff is commutative (in which case coincides with ) 3. 3.
If (C3) holds then is thinning on the family of -increasing sets, i.e. the inclusion holds for any -increasing 4. 4.
(C4) holds iff is contractive, i.e. the inclusion holds for any 5. 5.
If both (C2) and (C3) hold, then for any 6. 6.
If (C2)-(C4) all hold, then (C1) also holds since is trivialized to the set intersection operation
Proof.
Assuming (C1), let , and so that and , so that holds. By (C1), let be such that and , so that and , hence . The other direction of the inclusion is obtained similarly, going from (2) to (1). Conversely, if is associative, then from the identity the equivalence of conditions (1) and (2) is obtained in a straightforward manner, as it is merely a restatement of the special case of association , for any .
The case of (C2) and commutativity is immediate.
Assuming (C3), let , where are -increasing. Let so that . By (C3), and since , we obtain by -increasingness of .
If and (C4) holds, then by it follows . Conversely, if is contractive, choose to get from which follows. ∎
The sorted modal language of a frame , where we let be the complement of , is the language
[TABLE]
The language contains a copy of the language of CPL (in the second sort), a copy of the language of residuated Boolean algebras (in the first sort), synthesized by the sorted modalities on which a residuation axiom will be imposed.
The language is interpreted in models , where , and the interpretation is extended to all sentences by adding to the clauses for CPL (for each sort) satisfaction clauses for the additional constructs, as shown in Table 3.
It follows directly from definitions that \mbox{[![\alpha\odot\alpha^{\prime}]!]}=\{x\in X\;|\;x\models\alpha\circ\alpha^{\prime}\}=\mbox{[![\alpha]!]}\bigodot\mbox{[![\alpha^{\prime}]!]} and similarly \mbox{[![\alpha\rightfilledspoon\alpha^{\prime}]!]}=\mbox{[![\alpha]!]}\tilde{\Rightarrow}\mbox{[![\alpha^{\prime}]!]}, \mbox{[![\alpha^{\prime}\leftfilledspoon\alpha]!]}=\mbox{[![\alpha^{\prime}]!]}\tilde{\Leftarrow}\mbox{[![\alpha]!]}.
The two-sorted logic of a class of frames is a pair of sets of sentences such that for every and any model over any frame in the frame class , \mbox{[![\alpha]!]}_{\imath}=X and similarly for , \mbox{(!|\beta|!)}_{\imath}=Y. The hierarchy of the corresponding sorted, residuated modal logics is displayed in Figure 2, where the modal companion logic of a substructural logic SUB is designated by sub.ML2.
Note that for the systems including and above bci.ML2, the signature of the language may be restricted by dropping the (superfluous) .
Sorted Modal Logic: The Basic System ML2
The language of the minimal two-sorted, residuated modal logic (ML2) is generated by the following scheme
[TABLE]
Further logical connectives and constants are defined as usual in classical normal modal logic, i.e. , , , \alpha\mbox{\rightarrow}\alpha^{\prime}=\neg\alpha\vee\alpha^{\prime} and similarly for sentences of the second sort. In addition, diamond operators are defined by and \raisebox{-3.5pt}{\mbox{\Huge{\filleddiamond}}}\beta=\neg\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\neg\beta, where the two occurrences of negation are of different sort. Note that there are distinct constants (and similarly for ), corresponding to each sort. We avoid subscripts by letting and .
Models for ML2 on two-sorted frames (always assumed to satisfy condition (3)) are defined as detailed for the general case of sub.ML2.
Let ML designate the set of sentences of the first sort of the form \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta, for some sentence of the second sort. Similarly, let ML designate the set of sentences of second sort of the form , for some sentence of the first sort. If is an ML sentence and is an ML one, then clearly, \mbox{[![A]!]}=\mbox{[![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond A]!]}=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond\mbox{[![A]!]} and \mbox{(!|B|!)}=\mbox{(!|\largesquare\raisebox{-3.5pt}{\mbox{\Huge{}}}B|!)}=\largesquare\raisebox{-3.5pt}{\mbox{\Huge{\filleddiamond}}}\mbox{(!|B|!)}.
In accordance with our decision for the substructural logics proof systems we adopt a symmetric consequence system, directly encoding the algebraic specification of the logic. Thus, sequents for the logic ML2 are of the form , where are sentences of the first sort, as well as of the form \beta\mbox{\medvert!!!!\sim}\beta^{\prime}, where are sentences of the second sort. The proof system consists of axioms and rules for sequents of the first type and of the second type, which are copies of the rules for classical propositional logic and can be found in any standard reference. Furthermore, bridge rules are included, shown in Table 4, to relate the two subsystems.
For semantic entailment we write and (we do not change notation between the two sorts), with a standard, classical understanding. As usual, we write stand for , as well as for and similarly for and . It is immediate that ML2 is sound in the class of two-sorted frames satisfying condition (3).
The Lindenbaum-Tarski algebra of the logic is naturally a two-sorted algebra where both are Boolean algebras, are normal modal operators satisfying the D-axiom \blacksquare b\leq\raisebox{-1.5pt}{\mbox{\LARGE{\filleddiamond}}}b and and, in addition, for any , iff and then also \raisebox{-1.5pt}{\mbox{\LARGE{\filleddiamond}}}b\leq a iff where boxes and diamonds are interdefinable using classical complementation, as usual.
Soundness is immediate and completeness of ML2 is proven along the lines of the completeness proof for normal modal logics, except that we consider both the set of ultrafilters of (consisting of equivalence classes of sentences of the first sort), as well as the set of ultrafilters of (consisting of equivalence classes of sentences of the second sort). The canonical relation is defined along the standard lines: iff for all , if , then . This can be shown to be equivalent to the definition \forall a\;(a\in u\;\longrightarrow\;\raisebox{-1.5pt}{\mbox{\LARGE{\filleddiamond}}}a\in v), as usual. Furthermore, by residuation, the defining condition for the accessibility relation can be stated analogously and equivalently using (or ). We state the completeness result below; details are left to the interested reader.
Proposition 3.3**.**
ML2 is sound and complete in two-sorted frames satisfying conditions (3).
The proof systems of the modal companion logics sub.ML2, extending ML2, are specified as follows.
nfl.ML2
Monotonicity and residuation axioms for are added
[TABLE]
fl.ML2 = nfl.ML2 + Associativity axioms
and
bci.ML2 = fl.ML2 + Commutativity axiom
bcw.ML2 = bci.ML2 + Contraction axiom
bck.ML2 = bci.ML2 + Controlled weakening axiom
\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta\odot\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta^{\prime}\vdash\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta^{\prime}
It follows from the axiomatization that the Lindenbaum algebra of nfl.ML2 is a sorted, residuated modal algebra , where in addition is a residuated Boolean algebra. Adding associativity, commutativity and contraction axioms, the operator of the algebra is associative, commutative, contractive, respectively, and, with commutativity, . Note that contractiveness of can be assumed, yielding bcw.ML2, but not weakening, which can only be introduced in a controlled way (reminiscent of Linear Logic’s ! operator). Recall that satisfaction clauses (on top of the usual clauses for CPL, for each sort of sentences) have been specified in Table 3.
Theorem 3.4** (sub.ML2 Soundness).**
sub.ML2 is sound in -frames.
Proof.
The proof was essentially given in Lemma 3.2. For soundness of the bck.ML2 axiom \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta\odot\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta^{\prime}\vdash\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta^{\prime} it only needs to be observed that, given a frame , for any subset , the set \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0ptV\subseteq X is -increasing, since it is a Galois stable set \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0ptV=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0ptV (by residuation). ∎
3.2 Formal Concept Lattice Logics
Let be a frame and let be the closure of the restriction of on the set of Galois stable subsets of , i.e. A\bigovert C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(A\bigodot C). The Galois dual operator is defined on co-stable sets B=A\mbox{{}^{\upVdash}},D=C\mbox{{}^{\upVdash}} by
[TABLE]
where we let be defined by R^{\partial 11}uu^{\prime}=(R^{111}uu^{\prime})\mbox{{}^{\upVdash}}, i.e. for any it holds that iff . Hence we have and it then follows that distributes over arbitrary intersections of co-stable sets in each argument place. Therefore, by duality, distributes over arbitrary joins of Galois stable sets and hence it is residuated in , with residuals , i.e. iff iff .
Lemma 3.5**.**
The residuals of are the restrictions of the residuals of on stable sets. They are equivalently defined by
[TABLE]
Proof.
Note that for a stable set A=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond A and any set the inclusion \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond U\subseteq A obtains iff the inclusion does. In particular, iff , from which the first claim of the corollary follows. For the second claim we do only the case for (repeating the computation from [37]).
[TABLE]
The case for can be obtained from the above by appropriately modifying the last few lines, then changing bound variables to obtain the definition of as stated in the lemma. ∎
Lemma 3.6**.**
If is associative, commutative, thinning, or contractive, then so is . Consequently, the obvious correlation obtains between the frame constraints of Table 2 and properties of the operator on the complete lattice of Galois stable subsets of (which is isomorphic to the formal concept lattice of the frame).
Proof.
We first verify that associativity of implies associativity of . Recall first that if is a stable set, then \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond U\subseteq A iff , for any set . This implies in particular that (iff ) iff , for stable sets . We then obtain
[TABLE]
Hence, given associativity of and given that we have, by monotonicity, and, similarly, , it follows that is associative. By duality, B\bigovert^{\!\partial}D=({}\mbox{{}^{\upVdash}}B\bigovert{}\mbox{{}^{\upVdash}}D)\mbox{{}^{\upVdash}} and A\bigovert C={}\mbox{{}^{\upVdash}}(A\mbox{{}^{\upVdash}}\bigovert^{\!\partial}C\mbox{{}^{\upVdash}}), this implies associativity of . For the reader’s reassurance we display the calculation, given formal concepts (i.e. B=A\mbox{{}^{\upVdash}},D=C\mbox{{}^{\upVdash}},F=E\mbox{{}^{\upVdash}}).
[TABLE]
It is clear that is commutative iff is.
For the thinning property, assuming is thinning on -increasing sets then in particular for stable sets we have , hence \raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(A\bigodot C)\subseteq C, given stability of , which means by definition that .
For contractiveness, assume for any sets . In particular for stable sets and, taking closure, . ∎
Language and semantics for formal concept logics are those for substructural logics, presented in Section 2.2. As noted in Section 2.2, it is sufficient for the purposes of this article to consider proof systems as symmetric consequence systems , directly encoding the algebraic specification of the logic. The relational semantics of the substructural systems has been specified in Table 1. Algebraic soundness and completeness are well-established in the literature on substructural logics and, thereby, completeness in relational semantics can be established by a representation argument. For soundness, we verify that the algebra of stable subsets of the set of a frame is in the equational class of the Lindenbaum-Tarski algebra of the logic.
Theorem 3.7** (Soundness for SUB).**
Every substructural system SUB of Figure 1 is sound in the corresponding frame class , as defined in Definition 2.2.
Proof.
Let be a frame and its complete lattice of stable sets. In Sections 3.1 and 3.2 we have shown that is equipped with an operator , residuated with implication operators . This suffices for soundness of NFL in the class .
For the associative Lambek Calculus FL, the corresponding frame class assumes the constraint (C1) of Table 2. In Lemma 3.2 it was shown that (C1) is equivalent to associativity of and in Lemma 3.6 we verified that associativity of implies associativity of , which was defined on stable sets by setting A\bigovert C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(A\bigodot C). Furthermore, it was shown in Section 3.2 that is residuated in (and we in fact verified in Lemma 3.5 that its residuals are the respective restrictions of the residuals of in the algebra of all subsets of ). This establishes soundness of FL in its homonym frame class .
For BCI, Lemma 3.2 verified the equivalence between the constraint (C2) and commutativity of , from which commutativity of immediately follows, as observed in Lemma 3.6. Therefore, BCI is sound in its corresponding frame class .
For BCW, assuming contraction, it was verified in Lemma 3.2 that the relational constraint (C4) in the frame class is equivalent to contractiveness of , which immediately implies contractiveness of , as observed in Lemma 3.6, i.e. the inequation holds in . In other words, BCW is sound in the class .
For BCK, assuming weakening, it was verified in Lemma 3.2 that if the relational constraint (C3) (i.e. ) holds, then the inclusion holds for -increasing sets, and since every stable set is -increasing it follows that , from which we obtain A\bigovert C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(A\bigodot C)\subseteq C, given that we assume to be stable. Therefore, BCK is sound in the frame class and this concludes the proof. ∎
4 Modal Translation of Substructural Logics
In [38] we proved, via translation, that PLL (Positive Lattice Logic) is a fragment of ML2. We defined a translation and a co-translation of a sentence of the language of PLL into the two-sorted modal language ML2, by recursion, and we proved that the translation is full and faithful. This section extends the result to any substructural logic.
In Table 5, the translation of PLL into ML2 defined in [38] is extended to include the case of substructural logics.
Theorem 4.1**.**
Let be a -frame and a sub.ML2-model. Define a SUB-model on by setting V(p_{i})=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond\imath(P_{i}). Then for any SUB-sentences
\mbox{[![\varphi]!]}_{\mathfrak{N}}=\mbox{[![\varphi^{\bullet}]!]}_{\mathfrak{M}}=\mbox{[![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\neg\varphi^{\circ}]!]}_{\mathfrak{M}}=\mbox{[![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond\varphi^{\bullet}]!]}_{\mathfrak{M}} 2. 2.
\mbox{(!|\varphi|!)}_{\mathfrak{N}}=\mbox{(!|\varphi^{\circ}|!)}_{\mathfrak{M}}=\mbox{(!|\largesquare\neg\varphi^{\bullet}|!)}_{\mathfrak{M}}=\mbox{(!|\largesquare\raisebox{-3.5pt}{\mbox{\Huge{}}}\varphi^{\circ}|!)}_{\mathfrak{M}} 3. 3.
iff iff
Proof.
Claim 3) is an immediate consequence of the first two, which we prove simultaneously by structural induction. Note that, for 2), the identities \mbox{(!|\varphi|!)}_{\mathfrak{N}}=\mbox{(!|\largesquare\neg\varphi^{\bullet}|!)}_{\mathfrak{M}}=\mbox{(!|\largesquare\raisebox{-3.5pt}{\mbox{\Huge{}}}\varphi^{\circ}|!)}_{\mathfrak{M}} are easily seen to hold for any , given the proof of claim 1), since
[TABLE]
[TABLE]
For the induction proof, the cases for PLL have been covered in [38], Proposition 4.1, to which we refer the reader for details.
- (Case )
The following calculation proves the claim.
[TABLE]
The other two identities for claim 1) are straightforward, given definitions. For 2), observe that \mbox{(!|\varphi\circ\psi|!)}_{\mathfrak{N}}=\mbox{(!|\varphi|!)}_{\mathfrak{N}}\bigovert^{\!\partial}\mbox{(!|\psi|!)}_{\mathfrak{N}}=\mbox{[![\varphi]!]}_{\mathfrak{N}}^{\upVdash}\bigovert^{\!\partial}\mbox{[![\psi]!]}_{\mathfrak{N}}^{\upVdash} =(\mbox{[![\varphi]!]}_{\mathfrak{N}}\bigovert\mbox{[![\psi]!]}_{\mathfrak{N}})^{\upVdash}=\largesquare(-\mbox{[![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(\varphi^{\bullet}\bigodot\psi^{\bullet})]!]}_{\mathfrak{M}})=\mbox{(!|\largesquare\neg(\varphi^{\bullet}\bigodot\psi^{\bullet})|!)}_{\mathfrak{M}} but the latter is precisely \mbox{(!|(\varphi\circ\psi)^{\circ}|!)}_{\mathfrak{M}}. 2. (Case )
By definition of semantics and by the fact that is the restriction of on stable sets, see Lemma 3.5, we obtain
[TABLE] 3. (Case )
Similar to the case for .
Hence for any we obtained that \mbox{[![\varphi]!]}_{\mathfrak{N}}=\mbox{[![\varphi^{\bullet}]!]}_{\mathfrak{M}} and the identities \mbox{[![\varphi^{\bullet}]!]}_{\mathfrak{M}}=\mbox{[![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\neg\varphi^{\circ}]!]}_{\mathfrak{M}}=\mbox{[![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond\varphi^{\bullet}]!]}_{\mathfrak{M}} have been verified for the PLL fragment in [38] and are immediate for \circ,\mbox{\leftarrow},\mbox{\rightarrow} by the way the co-translation was defined. ∎
To transfer the result to the provability relation, completeness results need to be established, for each system SUB and its companion modal logic sub.ML2.
Theorem 4.2** (Completeness for SUB).**
Every substructural system SUB of Figure 1 is (sound, by Theorem 3.7, and) complete in the corresponding frame class , as defined in Definition 2.2.
Proof.
For completeness, let be the Lindenbaum-Tarski algebra of the logic and let be the canonical lattice frame [40], where is the complete lattice of (proper) lattice-filters, is the complete lattice of (proper) lattice-ideals and iff . Note that the canonical frame is separated i.e. the pre-order induced by setting iff \{x\}\mbox{{}^{\upVdash}}\subseteq\{z\}\mbox{{}^{\upVdash}} is a partial order on and similarly for . This is because if \{x\}\mbox{{}^{\upVdash}}\subseteq\{z\}\mbox{{}^{\upVdash}}, then for any , , hence which implies that . Furthermore, it follows from the definition of that it is increasing in each argument place.
Following [34] and as detailed in [39, 37], define the canonical relation by first defining a point operator on filters, where and designates a principal filter and then letting , where designates filter inclusion. Note that for any we easily obtain from the definition that
[TABLE]
It remains to show (a) that the canonical frame for a substructural logic SUB is a -frame and that (b) the canonical (co)interpretation, defined by \mbox{[![\varphi]!]}=\{x\in\mbox{\rm Filt}(\mathcal{L})\;|\;[\varphi]\in x\} and \mbox{(!|\varphi|!)}=\{y\in\mbox{\rm Idl}(\mathcal{L})\;|\;[\varphi]\in y\} respects the recursive satisfaction conditions of Table 1. We do this next in two lemmas, the canonical frame and canonical interpretation lemmas. ∎
Lemma 4.3** (Canonical SUB-Frame Lemma).**
The canonical frame for a substructural logic SUB is a -frame.
Proof.
There is nothing to prove for NFL. We argue separately each case of a logic above NFL (see Figure 1).
FL
To show that for all points , statements (1) and (2) below are equivalent in the canonical frame
(1) (2)
note first that equivalence of (1), (2) is an immediate consequence of associativity of the point operator . Indeed, assuming (1) holds, i.e. for some both and hold, then and we may take . Similarly for the converse.
To prove associativity of the point operator note that it follows from [34] (Theorem 6.6) where point operators were first introduced that distributes over arbitrary joins in each argument place, given that the lattice operator distributes over binary joins and that ([34], Lemma 6.7) it preserves principal filters, i.e. . It is then obtained that
[TABLE]
and this establishes associativity of . This implies, incidentally, that the associativity equation is canonical. Indeed, recall that the operator , defined on stable sets by A\bigovert C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(A\bigodot C), was shown in [39, 37] to be the -extension of the lattice cotenability operator . From [27], recall that is first defined on closed elements of (sets of the form ) by setting
[TABLE]
then extended to all stable sets using join-density of closed elements by setting . As pointed out in [39, 35, 37, 36], this delivers the same map on stable sets as the map defined on closed elements by setting , then again extending to all stable sets by using join-density of closed elements. This is immediate since , where by the definition of point operators in [34] we have . Thereby, the identity obtains on stable sets iff the identity on closed elements holds. Given the fact pointed out above that , associativity of the filter operator implies canonicity of the associativity equation since \Gamma u\mbox{\bigovert}(\Gamma v\mbox{\bigovert}\Gamma w)=(\Gamma u\mbox{\bigovert}\Gamma v)\mbox{\bigovert}\Gamma w\mbox{ iff }\Gamma(u\widehat{\circ}(v\widehat{\circ}w))=\Gamma((u\widehat{\circ}v)\widehat{\circ}w), which is equivalent to the identity , given that the canonical lattice frame is separated.
BCI
The case is straightforward, since by definition of , if is commutative, then so is the operator : . Hence holds iff holds, i.e. the constraint (C2) holds in the canonical frame.
BCK
Given , we obtain for any . Hence
[TABLE]
Therefore, if , i.e. , it follows that and thereby the constraint (C3) holds in the canonical frame.
BCW
We now have , i.e. . Then
[TABLE]
In particular, , i.e. holds. Hence the constraint (C4) holds in the canonical frame of BCW. ∎
Lemma 4.4** (Canonical SUB-Interpretation Lemma).**
The canonical interpretation, assigning to a sentence the formal concept (\mbox{[![\varphi]!]},\mbox{(!|\varphi|!)}) with extent \mbox{[![\varphi]!]}=\{x\in X\;|\;[\varphi]\in x\} and intent \mbox{(!|\varphi|!)}=\{y\in Y\;|\;[\varphi]\in y\}, where is the equivalence class of under provability, satisfies the recursive conditions of Table 1.
Proof.
The proof is by induction, the cases for are straightforward and we turn to the cases for the residuated operators.
The canonical accessibility relation has been defined by setting, for filters , iff (where we consistently use for filter inclusion). Hence is a Galois stable set, in fact a closed element of . The canonical Galois relation is increasing in each argument place from which it follows that iff . It needs to be verified, given the co-satisfaction clause for , that y\in\mbox{(!|\varphi\circ\psi|!)} iff for any , if u\in\mbox{[![\varphi]!]} and v\in\mbox{[![\psi]!]}, then . By definition of the canonical interpretation we have y\in\mbox{(!|\varphi\circ\psi|!)} iff iff . For lattice elements , given monotonicity of and increasingness of we obtain
[TABLE]
In particular, for the above yields precisely the co-satisfaction clause for cotenability: .
For the satisfaction clause for implication, it suffices to show that a\mbox{\rightarrow}b\in z iff .
Define first a point operator as in [34], given a filter and an ideal , to be the ideal generated by all implications a\mbox{\rightarrow}b with , i.e. x\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y=\bigvee\{y_{a\mbox{\rightarrow}b}\;|\;a\in x,b\in y\}.
Note that, it follows from the results of [39] that for the particular case of the normal lattice operator , of distribution type , the operator on defined by is its -extension and that A\bigovert C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(A\bigodot C).
In [39] and more specifically in [35] we have also constructed the -extension \Rightarrow_{1}=\mbox{\rightarrow}^{\sigma} of the lattice implication operator in our canonical lattice frame. This was done by first defining by . This is a monotone operator, completely distributing over arbitrary joins of closed elements in each argument place, hence it is extended to all of by setting . Then was defined in [35] by setting A\Rightarrow_{1}C={}\mbox{{}^{\upVdash}}(A\Rightarrow_{0}C\mbox{{}^{\upVdash}}). In particular, \Gamma x\Rightarrow_{1}{}\mbox{{}^{\upVdash}}\{y\}={}\mbox{{}^{\upVdash}}(\Gamma x\Rightarrow_{0}\Gamma y)={}\mbox{{}^{\upVdash}}\{x\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y\}.
By results of [27], Proposition 6.6, it follows that residuation is preserved by canonical extensions, hence for stable sets it holds that iff . In particular then, \Gamma x\bigovert\Gamma z\subseteq{}\mbox{{}^{\upVdash}}\{y\} iff \Gamma z\subseteq\Gamma x\Rightarrow_{1}{}\mbox{{}^{\upVdash}}\{y\}. This is equivalent, given the definitions of the stable set operators, to iff . Given the definition of , we obtain
[TABLE]
Furthermore, using the above we obtain
[TABLE]
By a completely symmetric argument and with defined as the join we similarly obtain that iff , from which it follows by the same argument as above that b\mbox{\leftarrow}a\in x iff and this completes the proof of the canonical interpretation lemma. ∎
We may then conclude.
Theorem 4.5** (SUB Soundness and Completeness).**
Each substructural logic SUB of Figure 1 is sound and complete in the respective frame-class.
For completeness of the modal companion logics, recall that to show that if (resp. ) is logically valid, i.e. (resp. ), then is a theorem, i.e. (resp. \mbox{\medvert!!!!\sim}\beta), one proceeds contrapositively arguing that for every non-theorem (resp. ) a model can be found such that (resp. ) is not valid in that model. The well established completeness argument proceeds by demonstrating that there is in fact a single model that invalidates all non-theorems of the logic, the so-called canonical model \mathfrak{M}_{c}=(\mathfrak{F}_{c},\mbox{[![;]!]}_{c}) of the logic, where is the canonical (sorted, in our case) frame and \mbox{[![\zeta]!]}_{c}=\{w\in W\;|\;[\zeta]\in w\}, while \mbox{(!|\eta|!)}=\largesquare(W\setminus\mbox{[![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\neg\eta]!]}_{c}) and where is the equivalence class, under provability, of .
Algebraically, the canonical frame construction is a realization of a canonical extension of the Lindenbaum-Tarski algebra of the logic. The standard (ultrafilter) canonical frame of a modal companion logic sub.ML2 is constructed from ultrafilters, as detailed for ML2. The canonical accessibility relation is defined on utrafilters by the condition iff for all and we have . We will however have use, for proof purposes, of an alternative canonical extension which regards the Boolean algebra merely as a lattice. By the results of Section 2.3 the two canonical extension constructions are isomorphic, a fact that we use in the proofs of the canonical frame and interpretation lemmas.
Lemma 4.6** (Canonical sub.ML2-Frame Lemma).**
The canonical frame of sub.ML2 is a -frame.
Proof.
There is nothing to prove for the system nfl.ML2 (the canonical relation generates residuated operators as detailed in Section 3.1) and we discuss each other system separately.
fl.ML2
This case (associativity relational constraint) has been identified as a non-elementary case and resolved by logicians working on Relevance Logic [1, 2] and we could simply refer to the related results (see, for example, a detailed proof in [18]). However, a simple solution can be now given using the notion of a canonical extension and related results and we report it below. Note first that, algebraically, the canonical frame is a realization of the construction of a canonical extension of the Lindenbaum-Tarski algebra of the logic (a residuated Boolean algebra, considering only the first sort, where the associative operation is defined). For distributive lattices the extension is based on the set of prime filters (as is the case for relevance logic) and for the Boolean case ultrafilters are considered, as it is well known. For arbitrary lattices all filters are used [40]. We already mentioned (and proved) in Section 4.2 that the associativity equation is canonical (it is preserved by canonical extensions). Furthermore, the set operator (on sets of ultrafilters) defined by
[TABLE]
is the -extension of (by the results of Jónsson and Tarski on Boolean algebras with operators [42, 43]), hence associative, where the canonical accessibility relation is defined (as for relevance logic) by
[TABLE]
It is furthermore elementary to see that the associativity relational constraint (C1) is equivalent to the identity , for any . Hence (C1) holds in the canonical fl.ML2 frame.
bci.ML2
Straightforward, since assuming , if , then , hence since commutativity is assumed in this case we also get from which follows, by definition of the relation.
bck.ML2
Let be ultrafilters such that holds. Fix , arbitrary. For any , and since holds in the Lindenbaum-Traksi algebra of the logic and is a filter, we obtain that . It follows that , which implies that , since they are both maximal filters. Since is a preorder, hence reflexive, it follows from that . Hence the relational constraint (C3) holds in the canonical frame.
bcw.ML2
The case is straightforward since, given any ultrafilter , for any lattice elements , if both , then and since contraction is assumed in bcw.ML2 we get from . Hence (C4) holds in the canonical frame. ∎
Lemma 4.7** (Canonical sub.ML2-Interpretation Lemma).**
The canonical interpretation of sub.ML2 satisfies the recursive clauses of Table 3.
Proof.
For each sort of sentences, the canonical interpretation \mbox{[![;]!]}_{c},\mbox{(!|;|!)}_{c} assigns to a sentence the set of respective ultrafilters containing its equivalence class, as usual. The proof is by induction and we skip the familiar cases corresponding to the Boolean operators (for each sort). For the needs of the proof we let , primed or with subscripts, and , again possibly with subscripts or primed.
Case \largesquare\alpha,\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta
Both cases are immediate by the way the canonical frame relation is defined.
Case
The current proof obligation is known in the relevance logic literature and it has been handled by Routley and Meyer [61] (see also [2, 18]) with a maximalization argument using Zorn’s lemma (delivering prime filters, which are maximal filters in our Boolean algebra case) and we could simply direct the reader to that proof argument. Instead, we provide a proof that makes use of the uniqueness, up to isomorphism, of canonical extensions of lattice expansions, see Lemma 2.3.
Recall from the results of Jónsson and Tarski [42, 43] that the additive, binary operator on the Boolean algebra is represented (in the ultrafilter canonical extension) relationally as the operator
[TABLE]
where is defined by
[TABLE]
Furthermore, is the -extension (in the terminology of [27]) of the cotenability operator and it is a completely additive operator, i.e. . Note also that iff .
Now regard the Boolean algebra merely as a lattice and take its canonical extension as the complete lattice of Galois stable sets , where . Let . As shown in Section 2.3, the isomorphism (by uniqueness of canonical extensions of lattices) between and sends a stable set to . The cotenability operator is now represented as an operator on Galois stable sets as in the proof of Lemma 4.3, by first defining a point operator (on filters), setting , then defining by iff , which is equivalent to the definition iff . Note that the restriction on the set of ultrafilters is precisely the canonical accessibility relation in the standard canonical (ultrafilter) extension of the Boolean algebra with an additive operator . By the analysis in Section 2.3, which is precisely the set . By Lemma 2.3, , using the notation introduced in the above mentioned lemma. By complete additivity of the latter is the union . Hence we have obtained that, for an ultrafilter and any filters ,
[TABLE]
In particular, given elements of the Boolean algebra,
[TABLE]
Now let be the respective equivalence classes of . The canonical interpretation \mbox{[![\alpha\odot\alpha^{\prime}]!]}_{c} is the representation of the equivalence class , i.e. \mbox{[![\alpha\odot\alpha^{\prime}]!]}_{c}=h(a\circ a^{\prime}), where is the Stone representation map . Assume for an ultrafilter that u\in\mbox{[![\alpha\odot\alpha^{\prime}]!]}_{c}, so that . It needs to be shown that there exist ultrfilters such that and . But and if , then , i.e. holds. This is equivalent, by (11), to the assertion that ultrafilters exist with and where . This shows that for an ultrafilter ,
[TABLE]
hence the canonical interpretation conforms to the relevant clause in the definition of the satisfaction relation of Table 3.
Case ,
The cases of follow from the case for , given Lemma 3.1 and hence the proof is complete. ∎
Hence we may conclude
Theorem 4.8** (Completeness for sub.ML2).**
Each modal companion logic sub.ML2 is (sound, by Theorem 3.4) and complete in the respective frame-class.
By Theorem 4.1 and by the soundness and completeness results proven above for each substructural logic SUB and its companion modal logic sub.ML2, we obtain that
Corollary 4.9**.**
in SUB iff iff \psi^{\circ}\mbox{\medvert!!!!\sim}\varphi^{\circ} in sub.ML2.
5 Translation into Sorted First-Order Logic
Assume are countable, non-empty and disjoint sets and let
[TABLE]
be the two-sorted, first-order language with equality whose sorted variables are in (ranged over by etc), (ranged over by etc) and it includes sorted quantifiers , a binary predicate Ixy, unary predicates P, Q (where sorting is indicated by the superscript) corresponding to the propositional variables of sub.ML2 and a three-place predicate . Superscripts indicating sorting type will be dropped in the sequel, for simplicity of notation. A two-sorted first-order structure for is a structure where are disjoint sets and , , , for each , and , while are the identity relations for each sort.
The standard translation of sub.ML2 into FOL (First-Order Logic) is exactly as in the single-sorted case, except for the relativization to two sorts, displayed in Table 6.
Note that a sub.ML2-model is also an -structure, setting , so that the following is immediate.
Proposition 5.1**.**
For any sub.ML2 formulae (of sort 1, 2, respectively), sub.ML2-model and , iff \mathfrak{M}\models\mbox{ST{}{z}(\alpha)}[z:=x] and iff \mathfrak{M}\models\mbox{ST{}{v}(\beta)}[v:=y].
Composing with the translation and co-translation of SUB into sub.ML2, respective translations of SUB into are obtained, displayed in Table 7.
Corollary 5.2**.**
For any SUB-sentences , any sub.ML2-model (-structure) and corresponding SUB-model , any ,
iff iff \mathfrak{M}\models\mbox{ST{}^{\bullet}_{z}(\varphi)}[z:=x] 2. 2.
iff iff for any , if \mathfrak{M}\models\mbox{ST{}^{\bullet}{z}(\varphi)}[z:=x], then \mathfrak{M}\models\mbox{ST{}^{\bullet}{z}(\psi)}[z:=x] 3. 3.
iff iff \mathfrak{M}\models\forall x\;\mbox{ST{}^{\bullet}_{x}(\varphi)} 4. 4.
\mathfrak{M}\models\mbox{ST{}^{\bullet}_{z}(\varphi)}[z:=x] iff
\wedge\;\mbox{ST{}^{\bullet}_{z^{\prime}}(\varphi)})[z:=x]
and similarly for ST.
Compactness and the Löwenheim-Skolem properties for any substructural logic SUB follow immediately from the reduction presented in this article.
Theorem 5.3**.**
The following hold.
(Compactness) A set of SUB-sentences has a model iff every finite subset of it has a model 2. 2.
(Upward Löwenheim-Skolem) If a set of SUB-sentences has a countable model, then it has a model of cardinality , for any 3. 3.
(Downward Löwenheim-Skolem) If a set of SUB-sentences has an infinite model, then it has a model of cardinality
Proof.
If is a set of SUB-sentences and is a SUB-model of , then clearly every finite subset of has a model, to wit . For the converse, if every finite subset of a set of SUB-sentences has a model , then every finite subset of thereby has a model (the same model ), hence has a model by compactness of sorted FOL (cf [19]) and then , on the same frame and with interpretation defined by V(p_{i})=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond\imath(P_{i}), is a model of .
The Löwenheim-Skolem properties follow by the same back and forth argument from SUB-models to first-order structures, using Corollary 5.2 and the Löwenheim-Skolem theorem for sorted first-order logic. ∎
6 Sort Reduction and Decidability
Decidability can be deduced from the finite model property (FMP) of the two-variable fragment of FOL, yet to the best of this author’s knowledge the FMP property has only been proven for unsorted FOL, hence sort-reduction needs to be performed (cf Enderton [19]), extending with two unary predicates , redefining first-order structures for so that and relativising the translation of Table 6
[TABLE]
with the obvious clauses for negation and conjunction. For a two-sorted first-order model , let be its corresponding single-sorted model, whose universe is the union of the universes of each sort of . The translation by sort reduction is known to be full and faithful (cf Enderton [19]).
Theorem 6.1** (Decidability and Complexity).**
A substructural logic SUB has the finite model property and its satisfiability problem is decidable in nondeterministic exponential time.
Proof.
Decidability of the satisfiability problem for SUB follows from the finite model property of the two-variable fragment of first-order logic (assuming here sort-reduction for the standard translation of SUB), proven in [53, 30, 9].
Complexity bounds based on the FMP property are typically exponential. Indeed, Mortimer [53] proved the finite model property of the two-variable fragment with a doubly exponential bound on the model size. The result was improved in [30] by Grädel, Kolaitis and Vardi to a single-exponential bound. Checking for satisfiability of a sentence in the two-variable fragment of FOL, with models of at most exponential size, can be then performed in nondeterministic exponential time, as argued by Börger, Grädel and Gurevich in [9]. ∎
7 Conclusions
This article, a follow-up to [38] and based on the representation results of [39, 37], initiated a project of modal translation of non-distributive logics, focusing on a class of familiar non-distributive systems collectively referred to as substructural logics. The modal translation problem for substructural logics has been also addressed by Došen [15], who embarked in a project of extending the GMT translation. Došen’s main result is an embedding of BCI, BCK and BCW with intuitionistic negation into S4-type modal extensions of versions of BCI, BCK, BCW, respectively, all equipped with a classical-type negation. The approach, however, does not apply uniformly to substructural logics at large, as pointed out by Došen in [15].
In this article, the target modal system is a sorted, residuated modal logic which arises as the logical adjunction of classical propositional logic with the logic of residuated Boolean algebras [44]. The result is extendible to the full Lambek-Grishin calculus and to just any non-distributive logic, based on the representation results of [39, 36].
The approach and results in the present article have implications for the correspondence theory of substructural (non-distributive, more generally) logics, which can be addressed by considering the intermediate translation into the companion modal logic. Axioms in the substructural systems correspond to axioms in the modal companion systems, as shown, and frame conditions can be thereby calculated by employing the techniques of automated Shalqvist correspondence for modal logic.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Alan Ross Anderson and Nuel D. Belnap. Entailment: The Logic of Relevance and Necessity , volume I. Princeton University Press, 1975.
- 2[2] Alan Ross Anderson, Nuel D. Belnap, and J. Michael Dunn. Entailment: The Logic of Relevance and Necessity , volume II. Princeton University Press, 1992.
- 3[3] Philippe Balbiani. The modal multilogic of geometry. Journal of Applied Non-Classical Logics , 8(3):259–281, 1998.
- 4[4] Alexandru Baltag and Sonja Smets. Quantum logic as a dynamic logic. Synthese , 179(2):285–306, Mar 2011.
- 5[5] Guram Bezhanishvili. The universal modality, the center of a Heyting algebra, and the Blok-Esakia theorem. Annals of Pure and Applied Logic , 161(3):253 – 267, 2009. Papers presented at the Symposium on Logical Foundations of Computer Science 2007.
- 6[6] Nick Bezhanishvili and Silvio Ghilardi. The bounded proof property via step algebras and step frames. Annals of Pure and Applied Logic , 165(12):1832 – 1863, 2014.
- 7[7] Nick Bezhanishvili, Silvio Ghilardi, and Mamuka Jibladze. Free modal algebras revisited: the step-by-step method. In Leo Esakia on Duality in Modal and Intuitionistic Logics , pages 43–62. Springer, 2014.
- 8[8] Willem J. Blok. Varieties of Interior Algebras . University of Amsterdam, Department of Mathematics, 1976.