A Fundamental Non-Classical Logic — TEI-tagged view

Wesley H. HollidaypersName (2023date). “A Fundamental Non-Classical Logic.” Logicstitle·j.

Object of study — a base propositional (and first-order) logic in the signature of conjunction, disjunction, negation and the quantifiers whose only rules are the introduction and elimination rulesterm for the connectives

Research question — whether there is a logic more fundamental than intuitionistic, ortho, and classical logicterm - one justified purely by the introduction and elimination meaning of the connectives - and how to characterise it proof-theoretically and semantically

Contribution — 'fundamental logicterm': a proof- and semantically-characterised base logic from which intuitionistic logicterm (by adding Reiterationterm), orthologicterm (by adding Reductio), and classical logicterm (by adding both) are recovered, together with an algebraic and relational semanticsterm

Full text — tagged

The reference list is not part of the text we hold for this paper. Our copy was extracted from the publisher's page and the bibliography did not survive that extraction, so the article below ends before its references. Nothing has been removed by us.

A Fundamental Non-Classical Logic Abstract Abstract We give a proof-theoretic as well as a semantic characterization of a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that we suggest has a certain fundamental status. We present a Fitch-style natural deductionterm system for the logic that contains only the introduction and elimination rulesterm for the logical constants. From this starting point, if one adds the rule that Fitch called Reiterationterm, one obtains a proof system for intuitionistic logicterm in the given signature; if instead of adding Reiterationterm, one adds the rule of Reductio ad Absurdumterm, one obtains a proof system for orthologicterm; by adding both Reiterationterm and Reductio, one obtains a proof system for classical logicterm. Arguably neither Reiterationterm nor Reductio is as intimately related to the meaning of the connectives as the introduction and elimination rulesterm are, so the base logic we identify serves as a more fundamental starting point and common ground between proponents of intuitionistic logicterm, orthologicterm, and classical logicterm. The algebraic semantics for the logic we motivate proof-theoretically is based on bounded latticesterm equipped with what has been called a weak pseudocomplementationterm. We show that such lattice expansions are representable using a set together with a reflexive binary relation satisfying a simple first-order condition, which yields an elegant relational semanticsterm for the logic. This builds on our previous study of representations of lattices with negations, which we extend and specialize for several types of negation in addition to weak pseudocomplementationterm. Finally, we discuss ways of extending these representations to lattices with a conditional or implication operation. Keywords: natural deduction; introduction and elimination rulesterm; lattices with negation; lattices with implication; representation of lattices; intuitionistic logicterm; orthologicterm MSC: 03B20; 03G10; 06B15; 06B23; 06C15; 06D15; 06D20 1. Introduction According to an influential strand of proof theory and philosophy of language, the meaning of the logical connectives is given by their introduction and elimination rulesterm (or just by the introduction rules, from which the elimination rules are thought to follow; see, e.g., [1] (Section 5.13), [2] (Section 4), [3] (Chapters 11–13), [4]). Prior [5] explains a version of the view as follows: If we are asked what is the meaning of the word ’and’, at least in the purely conjunctive sense (as opposed to, e.g., its colloquial use to mean ’and then’), the answer is said to be completely given by saying that (i) from any pair of statements P and Q, we can infer the statement formed by joining P to Q with ’and’ (which statement we hereafter describe as ’the statement P-and-Q’), that (ii) for any conjunctive statement P-and-Q we can infer P, and (iii) from P-and-Q we can always infer Q. Anyone who has learnt to perform these inferences knows the meaning of ’and’, for there is simply nothing more to knowing the meaning of ’and’ than being able to perform these inferences. (p. 38) Without going nearly so far as to claim that the ability to follow the introduction and elimination rulesterm is all there is to grasping the meaning of ’and’, one can still appreciate that the validity of the introduction and elimination rulesterm is a central semantic fact about ’and’.

Logicians motivated by proof-theoretic accounts of the meaning of the connectives have tended to favor intuitionistic logicterm over classical logicterm on the grounds that the classical rule of Reductio ad Absurdumterm (if the assumption of ¬ 𝜑 leads to a contradiction, conclude 𝜑 ) allegedly cannot be justified on the basis of the meaning of negation in the way that the introduction and elimination rulesterm for negation can be (see [1] (Section 5.3), [3] (pp. 291–300), [6] (Section 1.2)). In fact, one can go further and argue that even intuitionistic logicterm goes beyond what can be justified on the basis of the meaning of the connectives. For example, in recent work in the formal semantics of natural language [7,8], it has been argued that the distributive lawterm of classical and intuitionsitic logic, according to which 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) entails ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) , is invalid for fragments of language that include the epistemic modalsterm ’might’ (⋄) and ’must’ (□). First, there is extensive evidence that sentences of the form (1) It’s raining but it might not be raining ( 𝑝 ∧ ⋄ ¬ 𝑝 ) are contradictory (see, e.g., [7,8,9,10,11]), not merely pragmatically infelicitous to assert.1 As discussed in [8], if we accepted the distributive lawterm, then from the banal expression of ignorance that (2) either it’s raining or it’s not, and it might be raining and it might not be raining ( ( 𝑝 ∨ ¬ 𝑝 ) ∧ ⋄ 𝑝 ∧ ⋄ ¬ 𝑝 ) we could draw the absurd conclusion that (3) it’s raining and it might not be, or it’s not raining and it might be ( ( 𝑝 ∧ ⋄ ¬ 𝑝 ) ∨ ( ¬ 𝑝 ∧ ⋄ 𝑝 ) ), which is a disjunction of two contradictions and therefore a contradiction.

One might think that the distributive lawterm can be justified using the introduction and elimination rulesterm for conjunction and disjunction, but this depends on the precise formulation of those rules. In particular, one must be careful to distinguish between what could be called Proof by Casesterm, the principle that if 𝜑 ⊢ 𝜒 and 𝜓 ⊢ 𝜒 , then 𝜑 ∨ 𝜓 ⊢ 𝜒 , and what could be called Proof by Casesterm with Side Assumptions, the principle that if 𝛼 ∧ 𝜑 ⊢ 𝜒 and 𝛼 ∧ 𝜓 ⊢ 𝜒 , then 𝛼 ∧ ( 𝜑 ∨ 𝜓 ) ⊢ 𝜒 , or if 𝛼 , 𝜑 ⊢ 𝜒 and 𝛼 , 𝜓 ⊢ 𝜒 , then 𝛼 , ( 𝜑 ∨ 𝜓 ) ⊢ 𝜒 .

If one takes the elimination rule for disjunction to be Proof by Casesterm with Side Assumptions, then the distributive lawterm is derivable using the introduction and elimination rulesterm for the connectives. But if one takes the elimination rule for disjunction to be Proof by Casesterm, it is not.2 The point can be made in an illuminating way in a Fitch-style natural deductionterm system [13,14]. Figure 1 shows a Fitch-style natural deductionterm of the absurd (3) above from the banal (2). The “mistake” in the proof lies in the Reiterationterm steps on lines 7 and 11: we should not be allowed to reiterate the assumption that might ¬ 𝑝 into a subproof where we have just assumed p or reiterate the assumption that might p into a subproof where we have just assumed ¬ 𝑝 ! From this perspective, the problematic principle of a Fitch-style natural deductionterm system when the language contains ’might’ is the rule of Reiterationterm, not the rule of ∨ elimination. Reiterationterm also leads to the pseudocomplementationterm principle that if 𝜑 ∧ 𝜓 ⊢ ⊥ , then 𝜓 ⊢ ¬ 𝜑 . But this principle is unacceptable for a language containing ’might’, since 𝑝 ∧ ⋄ ¬ 𝑝 is contradictory and yet ⋄ ¬ 𝑝 (’it might not be raining’) plainly does not entail ¬ 𝑝 (’it’s not raining’) [11]. For a battery of further arguments against distributivity, pseudocomplementationterm, and other laws to which Reiterationterm leads, in the context of a language with epistemic modalsterm, see [8].

For the purposes of the present paper, it is enough for the reader to find the project of going to a weaker logic without distributivity or pseudocomplementationterm to be an interesting one. Denying these principles is familiar from quantum logic [15], but the orthomodularity principle of quantum logic also appears to be invalid for fragments of natural language containing ’might’ and ’must’ [8]. Thus, we are interested in the weaker system of orthologicterm [16], though we weaken it even further by following the intuitionists in dropping Reductio ad Absurdumterm. In addition to the criticisms of Reductio for enabling nonconstructive proofs [17], there are arguments to the effect that Reductio and the principle of excluded middle to which it leads should be rejected for a language with vague predicates [18,19,20]. In any case, here we drop Reductio not on ideological grounds but rather to find a neutral base logic. Figure 1. An illustration of the problem with Reiterationterm in a language with epistemic modalsterm.

In this paper, we begin in Section 2 with a Fitch-style natural deductionterm system for a propositional logic in the signature with conjunction, disjunction, and negation that contains only the introduction and elimination rulesterm for the connectives. We defer the addition of the universal and existential quantifiers with their introduction and elimination rulesterm to Section 5. Starting from the system we define, if one adds Fitch’s rule of Reiterationterm, one obtains a proof system for intuitionistic logicterm in the given signature, defined in Appendix A; if instead of adding Reiterationterm, one adds the rule of Reductio ad Absurdumterm, one obtains a proof system for orthologicterm; by adding both Reiterationterm and Reductio, one obtains a proof system for classical logicterm. Arguably neither Reiterationterm nor Reductio is as intimately related to the meaning of the connectives as the introduction and elimination rulesterm are, so the base logic we identify serves as a more fundamental starting point and common ground between proponents of intuitionistic logicterm, orthologicterm, and classical logicterm. In Section 3, we turn to the algebraic semantics for the logic, which is based on bounded latticesterm equipped with what has been called a weak pseudocomplementationterm. In Section 4, we show that such lattice expansions are representable using a set together with a reflexive binary relation satisfying a simple first-order condition, which yields an elegant relational semanticsterm for the logic. This builds on our previous study of representations of lattices with negations in [21], which we extend and specialize for several types of negation in addition to weak pseudocomplementationterm. In Section 5, we use one of our representation theorems to prove completeness with respect to relational semanticsterm of the extension of the logic from Section 2 with quantifiers. In Section 6 and Appendix B, we discuss ways of extending our representational approach to lattices with a conditional or implication operation. Finally, in Section 7, we conclude with a brief summary and look ahead.

Several Jupyter notebooks with code to check proofs and to construct algebras from relational frames and relational representations of algebras are available at https://github.com/wesholliday/fundamental-logic (Accessed on: 29 October 2022).

Though our argument against distributivity involved modals, we do not include modals in our language in this paper. A modal version of the fundamental logicterm defined in Section 2 can be studied using ideas from [8,21], but we will not do so here. As a result, our formal system will not reflect an important point: setting aside issues from quantum mechanics, as far as we can tell from natural language, distributivity is valid for sentences not including modals (or indicative conditionals). However, in this paper, we take atomic sentences 𝑝 , 𝑞 , 𝑟 , ⋯ to be genuine propositional variables, standing in for arbitrary propositions (cf. [22] (pp. 147–148)); thus, the failure of distributivity for modal propositions implies that we cannot accept 𝑝 ∧ ( 𝑞 ∨ 𝑟 ) ⊢ ( 𝑝 ∧ 𝑞 ) ∨ ( 𝑝 ∧ 𝑟 ) as a schematically valid principle. By enriching the language, one can define a system in which Reiterationterm and hence distributivity hold for special non-modal propositions but not for modal propositions [8]. But in this paper, the rules of the fundamental logicterm are supposed to be schematically valid principles holding for all propositions.

The relational semanticsterm in Section 4 covers logics much weaker than the fundamental logicterm of Section 2, including paraconsistent logics in the spirit of Battilotti and Sambin’s [23] basic logic, which (in a fragment of its language) is a sublogic of fundamental logicterm without 𝜑 ∧ ¬ 𝜑 ⊢ 𝜓 , 𝜑 ⊢ ¬ ( 𝜓 ∧ ¬ 𝜓 ) , or ⊥ ⊢ 𝜓 (though we do not have a primitive ⊥ in our language). In fact, we can cover logics as weak as the logic of lattices with an antitone unary operation ¬ (Theorem 4.29). Note that “fundamental” is not supposed to indicate that the logic of Section 2 is as weak as possible but rather that it has a special status based on introduction and elimination rulesterm insofar as the only gap between this logic and intuitionistic logicterm (resp. orthologicterm) in the relevant signature is Reiterationterm (resp. Reductio). Of course, Kolmogorov [24] and others have questioned the explosion principleterm 𝜑 ∧ ¬ 𝜑 ⊢ 𝜓 of intuitionistic logicterm. However, for inference in natural language, 𝜓 ∨ ( 𝜑 ∧ ¬ 𝜑 ) ⊢ 𝜓 appears acceptable, and this is equivalent to explosion given the rules for ∨. In any case, readers interested in weaker logics can focus on our semantics for those logics.

2. Fitch-Style Natural Deductionterm Given a nonempty set Prop of propositional variables, our propositional language 𝐿 is given by the grammar 𝜑 : : = 𝑝 ∣ ¬ 𝜑 ∣ ( 𝜑 ∧ 𝜑 ) ∣ ( 𝜑 ∨ 𝜑 ) where 𝑝 ∈ Prop . As abbreviations, we define ⊥ : = ( 𝑝 ∧ ¬ 𝑝 ) and ⊤ : = ¬ ⊥ .

We will define when a formula 𝜓 is provable from a formula 𝜑 , denoted 𝜑 ⊢ 𝐹 𝜓 , using a Fitch-style natural deductionterm system [13,14] (based on Jaskowski’s approach in [25]). We chose ’ 𝐹 ’ for fundamental logicterm or rather fundamental propositional logic, as we introduce a first-order extension in Section 5. To represent an argument with multiple assumptions, conjoin the assumptions with ∧ into a single formula 𝜑 . We chose Fitch-style natural deductionterm in part because we agree that it “corresponds more closely to proofs in ordinary mathematical practice” [26] (p. 134) and “is more faithful to the phenomenology of reasoning” [27] (p. 1110) than Gentzen-style natural deductionterm. Although the idea that the meaning of the connectives is given by introduction and elimination rulesterm is usually formulated in proof theory in terms of Gentzen rules, the view described by Prior in the quotation in Section 1 can certainly be formulated in terms of Fitch rules; indeed, referring to the introduction and elimination rulesterm for negation as in [14], Hazen and Pelletier [27] write that “they have as good a claim as any Gentzen-ish pair to specify uniquely the meaning of the connective they govern” (p. 1114).

We depart from Fitch in dropping his rules of Reiterationterm and double negation elimination [14]. A proof will be a sequence of formulas and possibly other proofs, defined inductively below. Every proof begins with one formula, considered its assumption (even if this is just ⊤). When diagramming proofs as in Figure 1, we adopt Fitch’s convention of drawing a horizontal line under the assumption of a proof. We regard a one formula proof 〈 𝜑 〉 as having 𝜑 as both its assumption and its conclusion, diagrammed as follows: We allow proofs that do not end with a conclusion formula (which could be called “partial proofs”) but we define the provability relation ⊢ 𝐹 as follows: 𝜑 ⊢ 𝐹 𝜓 if there exists a proof beginning with 𝜑 and ending with 𝜓 . For those familiar with Fitch-style natural deductionterm, the rules of our system are shown in Figure 2.

A rigorous inductive definition is as follows.3 The set of proofs is the smallest set containing for each formula 𝜑 the sequence 〈 𝜑 〉 and satisfying the following closure conditions for 1 ≤ 𝑖 , 𝑗 ≤ 𝑛 : If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof and 𝜏 is a proof, then 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜏 〉 is a proof. If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof and 𝜎 𝑖 , 𝜎 𝑗 are formulas, then 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜎 𝑖 ∧ 𝜎 𝑗 〉 is a proof (∧I). If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof and 𝜎 𝑖 is a formula of the form 𝜑 ∧ 𝜓 , then 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜑 〉 and 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜓 〉 are proofs (∧E). If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof and 𝜎 𝑖 is a formula, then for any formula 𝜑 , both 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜎 𝑖 ∨ 𝜑 〉 and 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜑 ∨ 𝜎 𝑖 〉 are proofs (∨I). If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof, 𝜎 𝑖 is a formula of the form 𝜑 ∨ 𝜓 , 𝜎 𝑛 − 1 is a sequence beginning with 𝜑 and ending with 𝜒 , and 𝜎 𝑛 is a sequence beginning with 𝜓 and ending with 𝜒 , then 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜒 〉 is a proof (∨E). If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof, 𝜎 𝑖 is a formula 𝜓 , and 𝜎 𝑛 is a sequence beginning with 𝜑 and ending with ¬ 𝜓 , then 〈 𝜎 1 , … , 𝜎 𝑛 , ¬ 𝜑 〉 is a proof (¬I). If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof and 𝜎 𝑖 and 𝜎 𝑗 are formulas of the form 𝜑 and ¬ 𝜑 , respectively, then for any formula 𝜓 , 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜓 〉 is a proof (¬E).

Note that for any proof 〈 𝜎 1 , … , 𝜎 𝑛 〉 , 𝜎 1 is a formula and all later 𝜎 𝑖 are either formulas or proofs. Also note that when diagramming proofs, we follow Fitch and include line numbers that justify a given rule application, but these data are not needed as official parts of a proof, just as they are not needed in Hilbert-style proofs. Whether a sequence is a proof is clearly decidable by an algorithm.

Our introduction and elimination rulesterm for ∧ and ∨ and our elimination rule for ¬ match those of Fitch [14]. However, our introduction rule for ¬ is not exactly the same as his. Our ¬ introduction rule says that if from the assumption of φ, you derive the negation of another formula derived just before the assumption, then conclude ¬ 𝜑 . This formulation of ¬ introduction is admissible in Fitch’s system, thanks to his Reiterationterm rule; but Fitch [14] states his ¬ introduction rule in a way that requires a pair of contradictory formulas to appear in the subproof that starts with 𝜑 .4 To accomplish what we accomplish with ¬I, Fitch would reiterate 𝜓 into the subproof beginning with 𝜑 to obtain a contradiction between 𝜓 and ¬ 𝜓 within the subproof. But we can disassociate Reiterationterm, which we do not allow (recall the cautionary Figure 1), from ¬ introduction. The idea of Reiterationterm is that if 𝜓 was derived just before a subproof beginning with 𝜑 , then ψ still holds under the assumption of φ. By contrast, when applying our ¬I rule, we prove that the negation of 𝜓 holds under the assumption of φ, and then since we know that ψ holds prior to the assumption of φ, we deduce ¬ 𝜑 .5 Let us relate our Fitch-style proof system to a binary logic in the sense of Goldblatt [16]. The following definition differs from Goldblatt’s definition of an orthologicterm only in dropping ¬ ¬ 𝜑 ⊢ 𝜑 and adding rules for ∨, which for us is not definable in terms of ∧ and ¬. Similarly, a sequent calculus presentation can be obtained from Cutland and Gibbins’ [28] (Section 3) sequent calculus for orthologicterm by dropping their rule ¬ ¬ → .

An intro-elim logicterm is a binary relation ⊢ ⊆ 𝐿 × 𝐿 such that for all 𝜑 , 𝜓 , 𝜒 ∈ 𝐿 : 1. 𝜑 ⊢ 𝜑 8. if 𝜑 ⊢ 𝜓 and 𝜓 ⊢ 𝜒 , then 𝜑 ⊢ 𝜒 2. 𝜑 ∧ 𝜓 ⊢ 𝜑 3. 𝜑 ∧ 𝜓 ⊢ 𝜓 9. if 𝜑 ⊢ 𝜓 and 𝜑 ⊢ 𝜒 , then 𝜑 ⊢ 𝜓 ∧ 𝜒 4. 𝜑 ⊢ 𝜑 ∨ 𝜓 5. 𝜑 ⊢ 𝜓 ∨ 𝜑 10. if 𝜑 ⊢ 𝜒 and 𝜓 ⊢ 𝜒 , then 𝜑 ∨ 𝜓 ⊢ 𝜒 6. 𝜑 ⊢ ¬ ¬ 𝜑 7. 𝜑 ∧ ¬ 𝜑 ⊢ 𝜓 11. if 𝜑 ⊢ 𝜓 , then ¬ 𝜓 ⊢ ¬ 𝜑 .

The following is easy to check.

⊢ 𝐹 is an intro-elim logicterm.

In fact, we will see that ⊢ 𝐹 is the smallest intro-elim logicterm (Proposition 3.8), which justifies the name of such logics: they all have at least the power of the introduction and elimination rulesterm for the connectives from ⊢ 𝐹 . Let us highlight the most important, even if obvious, cases of the proof of Proposition 2.2 for our purposes. First is 𝜑 ⊢ 𝐹 ¬ ¬ 𝜑 , which is shown as follows: Next is the property that if 𝜑 ⊢ 𝐹 𝜓 , then ¬ 𝜓 ⊢ 𝐹 ¬ 𝜑 . Assuming we have a proof from 𝜑 to 𝜓 , we construct a proof from ¬ 𝜓 to ¬ 𝜑 as follows: Proving 8–10 of Definition 2.1 for ⊢ 𝐹 also involves gluing together proofs. For 8, given proofs 〈 𝜑 , 𝜎 1 , … , 𝜎 𝑛 , 𝜓 〉 and 〈 𝜓 , 𝜏 1 , … , 𝜏 𝑚 , 𝜒 〉 , it is easy to see that 〈 𝜑 , 𝜎 1 , ⋯ 𝜎 𝑛 , 𝜓 , 𝜏 1 , … , 𝜏 𝑚 , 𝜒 〉 is also a proof. For 9, given proofs 〈 𝜑 , 𝜎 1 , … , 𝜎 𝑛 , 𝜓 〉 and 〈 𝜑 , 𝜏 1 , … , 𝜏 𝑚 , 𝜒 〉 , the sequence 〈 𝜑 , 𝜎 1 , … , 𝜎 𝑛 , 𝜓 , 𝜏 1 , … , 𝜏 𝑚 , 𝜒 , 𝜓 ∧ 𝜒 〉 is a proof. For 10, given proofs 𝜎 = 〈 𝜑 , 𝜎 1 , … , 𝜎 𝑛 , 𝜒 〉 and 𝜏 = 〈 𝜓 , 𝜏 1 , … , 𝜏 𝑚 , 𝜒 〉 , the sequence 〈 𝜑 ∨ 𝜓 , 𝜎 , 𝜏 , 𝜒 〉 is a proof.

Let us mention the three most salient extensions of our logic. First, adding Reductio ad Absurdumterm as in Figure 3 produces a Fitch-style proof system for orthologicterm, also laid out in [8]. Equivalently, let ⊢ 𝑂 be the smallest intro-elim logicterm containing ¬ ¬ 𝜑 ⊢ 𝜑 for all 𝜑 ∈ 𝐿 . As in the negative translation of classical logicterm into intuitionistic logicterm [29,30], the translation g given by 𝑔 ( 𝑝 ) = ¬ ¬ 𝑝 , 𝑔 ( ¬ 𝜑 ) = ¬ 𝑔 ( 𝜑 ) , 𝑔 ( 𝜑 ∧ 𝜓 ) = ( 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) ) , and 𝑔 ( 𝜑 ∨ 𝜓 ) = 𝑔 ( ¬ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) is a full and faithful embedding of orthologicterm into ⊢ 𝐹 .6 For all 𝜑 , 𝜓 ∈ 𝐿 , we have 𝜑 ⊢ 𝑂 𝜓 iff 𝑔 ( 𝜑 ) ⊢ 𝐹 𝑔 ( 𝜓 ) .

First, an easy induction shows that for all 𝜑 ∈ 𝐿 , 𝜑 ⊢ 𝑂 𝑔 ( 𝜑 ) and 𝑔 ( 𝜑 ) ⊢ 𝑂 𝜑 . Hence if 𝜑 ⊬ 𝑂 𝜓 , then 𝑔 ( 𝜑 ) ⊬ 𝑂 𝑔 ( 𝜓 ) and so 𝑔 ( 𝜑 ) ⊬ 𝐹 𝑔 ( 𝜓 ) , using that ⊢ 𝐹 is the smallest intro-elim logicterm. For the other direction, we claim that the relation ⊢ 𝑔 defined by 𝜑 ⊢ 𝑔 𝜓 iff 𝑔 ( 𝜑 ) ⊢ 𝐹 𝑔 ( 𝜓 ) is an intro-elim logicterm such that ¬ ¬ 𝜑 ⊢ 𝑔 𝜑 for all 𝜑 ∈ 𝐿 . Then since ⊢ 𝑂 is the smallest such logic, 𝜑 ⊢ 𝑂 𝜓 implies 𝑔 ( 𝜑 ) ⊢ 𝐹 𝑔 ( 𝜓 ) .

First, we prove by induction on 𝜑 ∈ 𝐿 that ¬ ¬ 𝜑 ⊢ 𝑔 𝜑 . For the base case of ¬ ¬ 𝑝 ⊢ 𝑔 𝑝 , we need that ¬ ¬ ¬ ¬ 𝑝 ⊢ 𝐹 ¬ ¬ 𝑝 , which follows from ¬ 𝑝 ⊢ 𝐹 ¬ ¬ ¬ 𝑝 . For the ¬ case of ¬ ¬ ¬ 𝜑 ⊢ 𝑔 ¬ 𝜑 , we need ¬ ¬ ¬ 𝑔 ( 𝜑 ) ⊢ 𝐹 ¬ 𝑔 ( 𝜑 ) , which follows from 𝑔 ( 𝜑 ) ⊢ 𝐹 ¬ ¬ 𝑔 ( 𝜑 ) . For the ∧ case of ¬ ¬ ( 𝜑 ∧ 𝜓 ) ⊢ 𝑔 𝜑 ∧ 𝜓 , we need ¬ ¬ ( 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) ) ⊢ 𝐹 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) . From 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) ⊢ 𝐹 𝑔 ( 𝜑 ) , we have ¬ 𝑔 ( 𝜑 ) ⊢ 𝐹 ¬ ( 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) ) and hence ¬ ¬ ( 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) ) ⊢ 𝐹 ¬ ¬ 𝑔 ( 𝜑 ) , so ¬ ¬ ( 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) ) ⊢ 𝐹 𝑔 ( 𝜑 ) by the inductive hypothesis. By similar reasoning, ¬ ¬ ( 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) ) ⊢ 𝐹 𝑔 ( 𝜓 ) , so we obtain ¬ ¬ ( 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) ) ⊢ 𝐹 𝑔 ( 𝜑 ) ∧ 𝑔 ( 𝜓 ) . Finally, for the ∨ case of ¬ ¬ ( 𝜑 ∨ 𝜓 ) ⊢ 𝑔 𝜑 ∨ 𝜓 , we need ¬ ¬ ¬ ( ¬ 𝑔 ( 𝜑 ) ∧ ¬ 𝑔 ( 𝜓 ) ) ⊢ 𝐹 ¬ ( ¬ 𝑔 ( 𝜑 ) ∧ ¬ 𝑔 ( 𝜓 ) ) , which follows from ¬ 𝑔 ( 𝜑 ) ∧ ¬ 𝑔 ( 𝜓 ) ⊢ 𝐹 ¬ ¬ ( ¬ 𝑔 ( 𝜑 ) ∧ ¬ 𝑔 ( 𝜓 ) ) .

Now it is easy to verify that ⊢ 𝑔 is an intro-elim logicterm. For condition 10 of Definition 2.1, given 𝜑 ⊢ 𝑔 𝜒 and 𝜓 ⊢ 𝑔 𝜒 , so 𝑔 ( 𝜑 ) ⊢ 𝐹 𝑔 ( 𝜒 ) and 𝑔 ( 𝜓 ) ⊢ 𝐹 𝑔 ( 𝜒 ) , we have ¬ 𝑔 ( 𝜒 ) ⊢ 𝐹 ¬ 𝑔 ( 𝜑 ) ∧ ¬ 𝑔 ( 𝜓 ) and hence ¬ ( ¬ 𝑔 ( 𝜑 ) ∧ ¬ 𝑔 ( 𝜓 ) ) ⊢ 𝐹 ¬ ¬ 𝑔 ( 𝜒 ) . It follows by the previous paragraph that ¬ ( ¬ 𝑔 ( 𝜑 ) ∧ ¬ 𝑔 ( 𝜓 ) ) ⊢ 𝐹 𝑔 ( 𝜒 ) , so 𝜑 ∨ 𝜓 ⊢ 𝑔 𝜒 . □ If instead of Reductio, we add Fitch’s rule of Reiterationterm to ⊢ 𝐹 , as in Appendix A, then we obtain a Fitch-style proof system for intuitionistic logicterm in the ∧ , ∨ , ¬ fragment. Intuitionistic logicterm in this fragment is the logic of pseudocomplemented distributive lattices [32], and using Reiterationterm we obtain both pseudocomplementationterm (see Figure 4) and distributivity (in the style of Figure 1). Finally, adding both Reductio and Reiterationterm yields a Fitch-style proof system for classical logicterm (see Appendix A).

We briefly note in Figure 5 how our points about Reiterationterm in Fitch-style natural deductionterm transfer to Gentzen-style natural deductionterm (see, e.g., [33] (Section 3.4)). The introduction and elimination rulesterm for conjunction, the introduction rule for disjunction, and the elimination rule for negation7 remain unchanged. We drop RAA from the Gentzen system just as we did from the Fitch system.

In response to a presentation of this paper at the Colloquium Logicum 2022, Aguilera and Bydžovský [34] observed that a sequent calculus LF for fundamental logicterm can be obtained from Gentzen’s sequent calculus LK for classical logicterm in the { ∧ , ∨ , ¬ } -signature by restricting to sequents Γ ⇒ Δ in which | Δ | ≤ 1 , as for intuitionistic logicterm, and | Γ | + | Δ | ≤ 2 , as for orthologicterm [35]. They verified that 𝜑 ⇒ LF 𝜓 iff 𝜑 ⊢ 𝐹 𝜓 , that LF admits cut-elimination, and that proof search in the cut-free calculus terminates in polynomial time, following a proof-search strategy of Egly and Tompits [36] (Section 4.3) for orthologicterm.

(Aguilera and Bydžovský) It is decidable in polynomial time whether 𝜑 ⊢ 𝐹 𝜓 .

In fact, Aguilera and Bydžovský obtained cut-elimination and decidability for the first-order version of fundamental logicterm in Section 5.

3. Algebras We now turn to algebraic semantics for the logic presented in Section 2. The relevant algebraic structures are bounded latticesterm equipped with an appropriate negation. We denote the lattice operations by ∧ and ∨ and the negation operation by ¬, trusting that no confusion will arise by using the same symbols as in 𝐿 .

We first define the operations corresponding to negation in intuitionistic logicterm, orthologicterm, and ⊢ 𝐹 , namely pseudocomplementationterm, orthocomplementation, and weak pseudocomplementationterm, respectively.

Let L be a bounded latticeterm and 𝑎 ∈ 𝐿 . An 𝑥 ∈ 𝐿 is the pseudocomplement of a if x is the maximum in L of { 𝑦 ∈ 𝐿 ∣ 𝑎 ∧ 𝑦 = 0 } , a complement of a if 𝑎 ∧ 𝑥 = 0 and 𝑎 ∨ 𝑥 = 1 , and a semicomplement of a if 𝑎 ∧ 𝑥 = 0 .

A pseudocomplementationterm (resp. complementation, semicomplementation) is a unary operation ¬ on L such that for all 𝑎 ∈ 𝐿 , ¬ 𝑎 is the pseudocomplement (resp. a complement, semicomplement) of a.

An orthocomplementation is a complementation that is antitone ( 𝑎 ≤ 𝑏 implies ¬ 𝑏 ≤ ¬ 𝑎 ) and involutive ( ¬ ¬ 𝑎 = 𝑎 ). An ortholattice is a bounded latticeterm equipped with an orthocomplementation.

A weak pseudocomplementationterm is an antitone semicomplementation satisfying double negation introduction: 𝑎 ≤ ¬ ¬ 𝑎 for all 𝑎 ∈ 𝐿 .

The negation operation in a Heyting algebra, defined by ¬ 𝑎 = 𝑎 → 0 , is the pseudocomplementationterm. Note that if a lattice admits a pseudocomplementationterm, then it is unique, in contrast to the other kinds of negations above. The term ’weak pseudocomplementationterm’ is taken from [37,38,39].8 The relational semanticsterm of Section 4 will handle other kinds of negations besides those for intuitionistic logicterm, orthologicterm, and ⊢ 𝐹 , so we define some weaker kinds below. For surveys of the large literature on different types of negation, we refer the reader to [41] and [42] (Chapter 8).

A precomplementation on a bounded latticeterm is an antitone unary operation ¬ such that ¬ 1 = 0 . A protocomplementation is an antitone semicomplementation ¬ such that ¬ 0 = 1 . An ultraweak pseudocomplementationterm is an antitone unary operation ¬ satisfying double negation introduction and ¬ 1 = 0 .

The term ’protocomplementation’ is from [21]. An “ultraweak” pseudocomplementationterm drops 𝑎 ∧ ¬ 𝑎 = 0 from the definition of weak pseudocomplementationterm in the spirit of paraconsistent logics [43].9 An example of an ultraweak but not weak pseudocomplementationterm is the negation operation on the three-element chain with ¬ 1 = 0 , ¬ 0 = 1 , and ¬ 1 2 = 1 2 used for Kleene’s [45] three-valued logic.

Properties of and the logical relations between six types of negation are shown in Table 1 and Figure 6. For example, to see that any weak pseudocomplementationterm is a protocomplementation, we show that 1 ≤ ¬ 0 : given that 1 ≤ ¬ ¬ 1 , it suffices to show ¬ 1 = 0 ; indeed, ¬ 1 = 1 ∧ ¬ 1 = 0 for any semicomplementation ¬. A number of other types of negation could be added to the diagram in Figure 6 (cf. the “kites of negations” in [44]). Each may appear to be based on a rather arbitrary choice of some properties but not others; but what makes weak pseudocomplementationsterm stand out in our view is the connection with the introduction and elimination rulesterm of ⊢ 𝐹 established below.

The weakest notion of negation defined above is that of a precomplementation. Yet restricting to precomplementations already forecloses some types of negation studied in the literature. For example, negation in Johansson’s [46] minimal logic (cf. [24]) is antitone and satisfies double negation introduction and the principle of non-contradiction in the form ¬ ( 𝑎 ∧ ¬ 𝑎 ) = 1 but not the semicomplementation axiom 𝑎 ∧ ¬ 𝑎 = 0 ; yet any ultraweak pseudocomplementationterm satisfying non-contradiction is a semicomplementation (and hence a weak pseudocomplementationterm). To give semantics for negation in minimal logic, we must drop the axiom ¬ 1 = 0 of precomplementations. The same applies to the basic logic of Battilotti and Sambin [23], whose negation (which is quasi-minimal in the terminology of [44]) satisfies none of 𝑎 ∧ ¬ 𝑎 = 0 , ¬ ( 𝑎 ∧ ¬ 𝑎 ) = 1 , or ¬ 1 = 0 . Although it is not our focus in this paper, we will explain how to handle negations that do not satisfy ¬ 1 = 0 in Remark 4.8 below.

For later use we note the following facts.

Let ¬ be a unary operation on a bounded latticeterm L.

1. If ¬ is a semicomplementation, then ¬ is anti-inflationary: 𝑎 ≰ ¬ 𝑎 for all nonzero 𝑎 ∈ 𝐿 . If ¬ is antitone and anti-inflationary, then ¬ is a semicomplementation. 2. ¬ satisfies antitonicity and double negation introduction iff for all 𝑎 , 𝑏 ∈ 𝐿 , 𝑎 ≤ ¬ 𝑏 implies 𝑏 ≤ ¬ 𝑎 . 3. ¬ is an orthocomplementation iff ¬ is a weak pseudocomplementationterm satisfying double negation elimination: ¬ ¬ 𝑎 ≤ 𝑎 for all 𝑎 ∈ 𝐿 .

For part 1, if for some nonzero 𝑎 ∈ 𝐿 , 𝑎 ≤ ¬ 𝑎 , then 𝑎 ∧ ¬ 𝑎 = 𝑎 ≠ 0 , so ¬ is not a semicomplementation. Now suppose ¬ is antitone and anti-inflationary. If 𝑎 ∧ ¬ 𝑎 ≠ 0 , then by anti-inflationarity, 𝑎 ∧ ¬ 𝑎 ≰ ¬ ( 𝑎 ∧ ¬ 𝑎 ) , but since 𝑎 ∧ ¬ 𝑎 ≤ 𝑎 , we have ¬ 𝑎 ≤ ¬ ( 𝑎 ∧ ¬ 𝑎 ) by antitonicity and hence 𝑎 ∧ ¬ 𝑎 ≤ ¬ ( 𝑎 ∧ ¬ 𝑎 ) .

For part 2, if ¬ satisfies antitonicity and double negation introduction, them 𝑎 ≤ ¬ 𝑏 implies ¬ ¬ 𝑏 ≤ ¬ 𝑎 and hence 𝑏 ≤ ¬ 𝑎 . Conversely, suppose ¬ satisfies the implication in part 2. Then starting with ¬ 𝑏 ≤ ¬ 𝑏 and 𝑎 = ¬ 𝑏 , we have 𝑏 ≤ ¬ ¬ 𝑏 . For antitonicity, if 𝑎 ≤ 𝑐 , then 𝑎 ≤ ¬ ¬ 𝑐 , so taking 𝑏 = ¬ 𝑐 , we have ¬ 𝑐 ≤ ¬ 𝑎 .

For part 3, we need only show 1 ≤ 𝑎 ∨ ¬ 𝑎 when ¬ is a weak pseudocomplementationterm satisfying double negation elimination. Since 𝑎 ≤ 𝑎 ∨ ¬ 𝑎 and ¬ 𝑎 ≤ 𝑎 ∨ ¬ 𝑎 , we have ¬ ( 𝑎 ∨ ¬ 𝑎 ) ≤ ¬ 𝑎 ∧ ¬ ¬ 𝑎 and hence ¬ ( 𝑎 ∨ ¬ 𝑎 ) ≤ ¬ 𝑎 ∧ 𝑎 , so ¬ ( ¬ 𝑎 ∧ 𝑎 ) ≤ ¬ ¬ ( 𝑎 ∨ ¬ 𝑎 ) ≤ 𝑎 ∨ ¬ 𝑎 . Then since a weak pseudocomplementationterm satisfies ¬ 𝑎 ∧ 𝑎 = 0 and ¬ 0 = 1 , we have 1 ≤ 𝑎 ∨ ¬ 𝑎 . □ Figure 7 shows the 𝑁 5 lattice equipped with a pseudocomplementationterm that is not an orthocomplementation (left), a weak pseudocomplementationterm that is neither a pseudocomplementationterm nor an orthocomplementation (middle), and a protocomplementation that is not a weak pseudocomplementationterm (right). Figure 8 shows the Benzene ring 𝑂 6 equipped with an orthocomplementation that is not a pseudocomplementationterm (left) and a pseudocomplementationterm that is not an orthocomplementation (right).

Note that any bounded latticeterm can be equipped with a weak pseudocomplementationterm by setting ¬ 0 = 1 and ¬ 𝑎 = 0 for all 𝑎 ≠ 0 ; and if there are nonzero 𝑎 , 𝑏 ∈ 𝐿 with 𝑎 ∧ 𝑏 = 0 , this ¬ is not a pseudocomplementationterm. Also note that any bounded latticeterm can be equipped with a precomplementation by setting ¬ 1 = 0 and ¬ 𝑎 = 1 for all 𝑎 ≠ 1 ; and if L has more than one nonzero element, this ¬ is not a protocomplementation.

It is noteworthy that all of the intuitionistically acceptable De Morgan inequalities that hold in bounded latticesterm with pseudocomplementationsterm also hold in bounded latticesterm with weak pseudocomplementationsterm: ¬ ( 𝑎 ∨ 𝑏 ) = ¬ 𝑎 ∧ ¬ 𝑏 and ¬ 𝑎 ∨ ¬ 𝑏 ≤ ¬ ( 𝑎 ∧ 𝑏 ) . However, there are inequalities that hold in all bounded latticesterm with pseudocomplementationsterm and all bounded latticesterm with orthcomplementations but do not hold in all bounded latticesterm with weak pseudocomplementationsterm. An example is ¬ ¬ 𝑎 ∧ ¬ ¬ 𝑏 ≤ ¬ ¬ ( 𝑎 ∧ 𝑏 ) . Consider the 4-element Boolean lattice equipped not with Boolean negation but with the weak pseudocomplementationterm with ¬ 0 = 1 and ¬ 𝑐 = 0 for 𝑐 ≠ 0 . Where a and b are the side elements of the lattice, we have ¬ ¬ 𝑎 ∧ ¬ ¬ 𝑏 = 1 ∧ 1 = 1 while ¬ ¬ ( 𝑎 ∧ 𝑏 ) = ¬ ¬ 0 = 0 .10 This suggests an interesting problem, not pursued here, of axiomatizing the intersection of orthologicterm and intuitionistic logicterm (or orthointuitionistic logic).

As usual, we can interpret the language 𝐿 in lattice expansions ( 𝐿 , ¬ ) as follows.

A valuation on a lattice expansion ( 𝐿 , ¬ ) is a function 𝜃 : Prop ⟶ 𝐿 that extends to 𝜃 ˜ : 𝐿 ⟶ 𝐿 by: 𝜃 ˜ ( 𝑝 ) = 𝜃 ( 𝑝 ) , 𝜃 ˜ ( ¬ 𝜑 ) = ¬ 𝜃 ˜ ( 𝜑 ) , 𝜃 ˜ ( 𝜑 ∧ 𝜓 ) = 𝜃 ˜ ( 𝜑 ) ∧ 𝜃 ˜ ( 𝜓 ) , and 𝜃 ˜ ( 𝜑 ∨ 𝜓 ) = 𝜃 ˜ ( 𝜑 ) ∨ 𝜃 ˜ ( 𝜓 ) .

Given a class 𝐶 of lattice expansions, we define 𝜑 ⊧ 𝐶 𝜓 if for every ( 𝐿 , ¬ ) ∈ 𝐶 and valuation 𝜃 on ( 𝐿 , ¬ ) , we have 𝜃 ˜ ( 𝜑 ) ≤ 𝜃 ˜ ( 𝜓 ) .

Let 𝑊 be the class of lattices expanded with a weak pseudocomplementationterm. Then we have the following soundness result for our Fitch-style proof system.

For any 𝜑 , 𝜓 ∈ 𝐿 , if 𝜑 ⊢ 𝐹 𝜓 , then 𝜑 ⊧ 𝑊 𝜓 .

We claim that for any Fitch-style proof 〈 𝜎 1 , … , 𝜎 𝑛 〉 , if 𝜎 𝑛 is a formula, then 𝜎 1 ⊧ 𝑊 𝜎 𝑛 . We proceed by induction on proofs, using the fact that if 〈 𝜎 1 , … , 𝜎 𝑘 〉 is a proof, so is 〈 𝜎 1 , … , 𝜎 ℓ 〉 for 1 ≤ ℓ ≤ 𝑘 . Suppose, for example, that 〈 𝜎 1 , … , 𝜎 𝑛 + 1 〉 is a proof in which 𝜎 𝑛 + 1 = ¬ 𝜑 is obtained by the ¬I rule: that is, 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof, there is a formula 𝜎 𝑖 of the form 𝜓 , and 𝜎 𝑛 is a proof beginning with 𝜑 and ending with ¬ 𝜓 . Then by the inductive hypothesis applied to the proof 〈 𝜎 1 , … , 𝜎 𝑖 〉 , we have 𝜎 1 ⊧ 𝑊 𝜓 ; and by the inductive hypothesis applied to the proof 𝜎 𝑛 , we have 𝜑 ⊧ 𝑊 ¬ 𝜓 , which implies 𝜓 ⊧ 𝑊 ¬ 𝜑 by Lemma 3.4.2. Putting the previous two steps together, we have 𝜎 1 ⊧ 𝑊 ¬ 𝜑 . The other cases of the proof are similar. □ As usual, the Lindenbaum-Tarski algebra of ⊢ 𝐹 has as its elements the equivalence classes [ 𝜑 ] of formulas of 𝐿 , where 𝜑 and 𝜓 are equivalent if 𝜑 ⊢ 𝐹 𝜓 and 𝜓 ⊢ 𝐹 𝜑 , and the operations are defined by ¬ [ 𝜑 ] = [ ¬ 𝜑 ] , [ 𝜑 ] ∧ [ 𝜓 ] = [ 𝜑 ∧ 𝜓 ] , and [ 𝜑 ] ∨ [ 𝜓 ] = [ 𝜑 ∨ 𝜓 ] . It is easy to show using Proposition 2.2 that this algebra is a bounded latticeterm equipped with a weak pseudocomplementationterm, ( 𝐿 , ¬ ) , whose lattice order we denote by ≤. Then the valuation 𝜃 : Prop ⟶ 𝐿 defined by 𝜃 ( 𝑝 ) = [ 𝑝 ] is such that for all 𝜑 ∈ 𝐿 , 𝜃 ˜ ( 𝜑 ) = [ 𝜑 ] . Hence if 𝜑 ⊬ 𝐹 𝜓 , so [ 𝜑 ] ≰ [ 𝜓 ] , then 𝜃 ˜ ( 𝜑 ) ≰ 𝜃 ˜ ( 𝜓 ) , so 𝜑 ⊭ 𝑊 𝜓 . This yields the following completeness result.

For any 𝜑 , 𝜓 ∈ 𝐿 , if 𝜑 ⊧ 𝑊 𝜓 , then 𝜑 ⊢ 𝐹 𝜓 .

By similar reasoning, we can show the soundness and completeness with respect to 𝑊 of the smallest intro-elim logicterm, so we obtain the following.

⊢ 𝐹 is the smallest intro-elim logicterm.

Thus, ⊢ 𝐹 is the logic of bounded latticesterm with weak pseudocomplementationsterm. Table 2 shows the numbers of algebras up to isomorphism of size up to 10, calculated using Mace4 [48], for ⊢ 𝐹 , intuitionistic logicterm (i.e., finite distributive lattices, each of which can be equipped with a unique pseudocomplementationterm), and orthologicterm. For comparison we also include the number of lattices and the number of pseudocomplemented lattices (i.e., lattices in which each element has a pseudocomplement).

Finally, we note that the observation above that any bounded latticeterm can be equipped with a weak pseudocomplementationterm implies a conservativity fact about ⊢ 𝐹 : if 𝜑 ⊢ 𝐹 𝜓 and 𝜑 , 𝜓 do not contain ¬, then 𝜓 is provable from 𝜑 in the Fitch-style proof system for the { ∧ , ∨ } -fragment of 𝐿 defined as for ⊢ 𝐹 but without the negation rules. That restricted proof system is easily shown to be sound and complete with respect to the class of all bounded latticesterm. Hence if 𝜓 is not provable from 𝜑 in the restricted system, then there is a bounded latticeterm witnessing that 𝜓 is not a semantic consequence of 𝜑 , which we then expand to a bounded latticeterm with a weak pseudocomplementationterm witnessing that 𝜓 is not a semantic consequence of 𝜑 , so 𝜑 ⊬ 𝐹 𝜓 .

4. Relational Representation and Semantics In this section, we give a relational semanticsterm for our logic via a relational representation of bounded latticesterm equipped with a weak pseudocomplementationterm. In Section 4.1 and Section 4.2, we build on the discrete representation of bounded latticesterm equipped with a protocomplementation from [21], extended and specialized for other kinds of negation from Section 3 (and further extended to bounded latticesterm with implications in Section 6 and Appendix B). In Section 4.3, we cover a topological representation of bounded latticesterm with negations. It would be natural to extend these representations to categorical dualities between categories of lattices with negations and categories of relational frames, but we will not pursue such a project here. Finally, in Section 4.4, we discuss translations of propositional logics into modal logics suggested by our relational semanticsterm.

4.1. From Relational Frames to Lattices with Negation In [49], a representation of bounded latticesterm is developed using a set together with a reflexive binary relation and a topology. For now we ignore topology (until Section 4.3) and use relational frames for a discrete representation of complete lattices with negations as in [21].

Relational representations of lattices with various negations have also been developed on the basis of Urquhart’s [50] doubly ordered sets in [37,38,51] and on the basis of Birkhoff’s [52] polarities in [39]. Here we use a single relation on a single set to realize both a lattice and its negation, in contrast to two relations to realize a lattice and a third to realize a negation [37,38] or a relation between two sets to realize a lattice and a second relation to realize a negation [39]. Using a single relation on a single set to realize a lattice and its negation goes back to Birkhoff and von Neumann ([52,53] (p. 25)), who applied this idea to ortholattices, leading to relational semanticsterm for orthologicterm [16,54]. Of course it also appears in relational semanticsterm for intuitionistic logicterm [55,56,57], which is a special case of the following approach (see Remark 4.9), though using a single relation in this case is not surprising since the relevant negation is uniquely determined by the lattice.

Inspired by the intuitionistic and orthological cases, Došen [58,59,60], Vakarelov [61], and Dunn [62,63,64] (also see [44]) study negation using triples ( 𝑋 , ⊲ , ⊑ ) where ( 𝑋 , ⊲ ) is a relational frame as below, ⊑ is a partial order on X, and an interaction condition holds between ⊲ and ⊑. Their definition of negation is the same as in [52] for orthocomplementation, namely that 𝑥 ∈ ¬ 𝐴 iff for all 𝑦 ⊲ 𝑥 , 𝑦 ∉ 𝐴 (or equivalently, for all 𝑦 ∈ 𝐴 , 𝑦 ⊲ 𝑥 , and possibly writing 𝑥 ⊳ 𝑦 instead of 𝑦 ⊲ 𝑥 ), which we will also use; the interaction condition between ⊲ and ⊑ then ensures that the negation operation sends upsets (or downsets, depending on one’s preference) to upsets (or downsets) of ⊑. Berto [65] (also see [66]) uses their setup to argue that ¬ should satisfy at least antitonicity and 𝑎 ≤ ¬ ¬ 𝑎 , a congenial conclusion given our interest in ⊢ 𝐹 . However, the cited authors do not generate the underlying lattice of propositions using the closure operator 𝑐 ⊲ as in Propositions 4.4.1 and 4.5.1 below (Došen and Vakarelov take the lattice of upsets/downsets, and Dunn sometimes takes the lattice of upsets/downsets and sometimes does not, e.g., when he wants to represent ortholattices), and their correspondences between conditions on ⊲ and axioms for negation are not the same as in our setting (see Remark 4.16).

The single relation approach has recently been applied to a sublogic of orthologicterm and intuitionistic logicterm in [67], which axiomatizes the logic of the reflexive frames below in the { ¬ , ∧ } -fragment of 𝐿 (see Theorem 4.27.2 below for the axiomatization in the full language with ∨). Zhong [67] takes inspiration from Dalla Chiara and Giuntini [15] (pp. 139–140), who observe that there is a closure operator definable from a reflexive relation—the same closure operator used in [49]—whose fixpoints are propositions for orthologicterm if the relation is symmetric or for intuitionistic logicterm if the relation is transitive.

Finally, the approach of representing a lattice using a binary relation on a set X contrasts with the approach of representing a lattice using a binary relation between X and ℘ ( 𝑋 ) , or equivalently, a function 𝑁 : 𝑋 → ℘ ( ℘ ( 𝑋 ) ) , as in neighborhood semantics for modal logic [68,69,70]. In the neighborhood approach, one imposes conditions on N such that the operation 𝑐 : ℘ ( 𝑋 ) ⟶ ℘ ( 𝑋 ) defined by 𝑐 ( 𝐴 ) = { 𝑥 ∈ 𝑋 ∣ 𝐴 ∈ 𝑁 ( 𝑥 ) } is a closure operator,11 whose fixpoints give us a complete lattice via Proposition 4.3 below. Conversely, any complete lattice is representable as the lattice of fixpoints of a closure operator on a powerset (see, e.g., [71] (Thm. 5.3)), and any closure operator c on ℘ ( 𝑋 ) is representable using a function N as above, defined by 𝑁 ( 𝑥 ) = { 𝐴 ⊆ 𝑋 ∣ 𝑥 ∈ 𝑐 ( 𝐴 ) } . By contrast, in the approach with a binary relation on X, matching relational semanticsterm for modal logic (see Section 4.4) instead of neighborhood semantics, the representability of complete lattices is less immediate. Versions of the neighborhood approach have been used by van Fraassen [72] (Section II), who applies it to Heyting algebras, ortholattices, and Boolean algebras, and Goldblatt [73], who applies it to Heyting algebras. Dragalin [74,75] also uses functions 𝑁 : 𝑋 → ℘ ( ℘ ( 𝑋 ) ) to represent Heyting algebras, but he defines his closure operator from N in a kind of dual way (also see [76]).

Our basic objects are simply the following frames.

A relational frame is a pair ( 𝑋 , ⊲ ) of a nonempty set X and a binary relation ⊲ on X. We say the frame is reflexive if ⊲ is reflexive.

We call elements of X states and read 𝑥 ⊲ 𝑦 as x is open to y in the sense of the following remark.12 When convenient, we write 𝑦 ⊳ 𝑥 for 𝑥 ⊲ 𝑦 .

For an intuitive picture to pair with the mathematical development to follow, start with the distinction between accepting a proposition and rejecting it. We want to allow for partial states that are completely noncommittal about a proposition, so non-acceptance of a proposition should not entail rejection of it. Moreover, we want to allow for states that reject a proposition without accepting the negation of it; for example, an intuitionist might reject a certain instance of the law of excluded middle, 𝐴 ∨ ¬ 𝐴 , but will certainly not accept its negation, which is an intuitionistic contradiction (cf. Field’s [19] separation of rejection, non-acceptance, and acceptance of the negation). These notions can be linked with our notion of openness as follows: x is open to y iff x does not reject any proposition that y accepts. If this is consistent with y rejecting some proposition that x accepts, then openness in our sense is not necessarily symmetric. Now if we start with ( 𝑋 , ⊲ ) and a proposition 𝐴 ⊆ 𝑋 , say that x accepts A if 𝑥 ∈ 𝐴 ; x rejects A if for all 𝑦 ⊳ 𝑥 , 𝑦 ∉ 𝐴 ; and x accepts ¬ 𝐴 if for all 𝑦 ⊲ 𝑥 , 𝑦 ∉ 𝐴 .13 Then we will indeed have that 𝑥 ⊲ 𝑦 iff x does not reject any proposition that y accepts.14 Finally, another result of the partiality of states is that accepting a disjunction does not require accepting either disjunct. Instead, x accepting 𝐴 ∨ 𝐵 will amount to the following: no state open to x rejects both disjuncts.

Rather than moving from a relational frame to an associated Boolean algebra with an operator, as in modal logic, here we move to an associated lattice equipped with a negation. See [77] for comparison with the realization of complete lattices using doubly ordered structures and polarities.

First recall that a unary operation on a lattice is a closure operator if c is inflationary ( 𝑎 ≤ 𝑐 ( 𝑎 ) ), idempotent ( 𝑐 ( 𝑐 ( 𝑎 ) ) = 𝑐 ( 𝑎 ) ), and monotone ( 𝑎 ≤ 𝑏 implies 𝑐 ( 𝑎 ) ≤ 𝑐 ( 𝑏 ) ). We will use the relation ⊲ to define a closure operator on ℘ ( 𝑋 ) , whose fixpoints give us a complete lattice as in the following classic result (see, e.g., [71] (Thm. 5.2)).

Let X be a nonempty set and c a closure operator on ℘ ( 𝑋 ) . Then the fixpoints of c, i.e., those 𝐴 ⊆ 𝑋 with 𝑐 ( 𝐴 ) = 𝐴 , ordered by ⊆ form a complete lattice with ⋀ 𝑖 ∈ 𝐼 𝐴 𝑖 = ⋂ 𝑖 ∈ 𝐼 𝐴 𝑖 and ⋁ 𝑖 ∈ 𝐼 𝐴 𝑖 = 𝑐 ⋃ 𝑖 ∈ 𝐼 𝐴 𝑖 .

In our case, the relevant closure operator is given in part 1 of the following, while the relevant negation operation on the fixpoints of the closure operator is given in part 2. The proof is straighforward.

For any relational frame ( 𝑋 , ⊲ ) : 1. the operation 𝑐 ⊲ : ℘ ( 𝑋 ) ⟶ ℘ ( 𝑋 ) defined by 𝑐 ⊲ ( 𝐴 ) = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑥 ′ ⊲ 𝑥 ∃ 𝑥 ″ ⊳ 𝑥 ′ : 𝑥 ″ ∈ 𝐴 } is a closure operator on ℘ ( 𝑋 ) ; 2. the operation ¬ ⊲ : ℘ ( 𝑋 ) ⟶ ℘ ( 𝑋 ) defined by ¬ ⊲ 𝐴 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ⊲ 𝑥 𝑦 ∉ 𝐴 } sends 𝑐 ⊲ -fixpoints to 𝑐 ⊲ -fixpoints.

Thus, x is in the closure of A iff every state open to x is open to some state in A;15 and x is in the negation of A iff no state open to x is in A. We call the fixpoints of the 𝑐 ⊲ operation, those A such that 𝑐 ⊲ ( 𝐴 ) = 𝐴 , the 𝑐 ⊲ -fixpoints, rather than closed sets, since later (Section 4.3) we will add a topology in which the 𝑐 ⊲ -fixpoints are open but not necessarily closed, so our terminology avoids any possible confusion. We will assume that propositions are 𝑐 ⊲ -fixpoints, which amounts to the following in the terms of Remark 4.2: A is a proposition ( 𝑐 ⊲ -fixpoint) iff whenever a state x does not accept A, then there is a state open to x that rejects A.

In Section 6 and Appendix B, we also define binary implication operations from the ⊲ relation, and from these implication operations, both 𝑐 ⊲ and ¬ ⊲ are in turn definable.

Proposition 4.3 together with Proposition 4.4.1 yields part 1 of the following, while Proposition 4.4.2 together with some easy additional reasoning yields parts 2 and 3.

For any relational frame ( 𝑋 , ⊲ ) : 1. the 𝑐 ⊲ -fixpoints ordered by ⊆ form a complete lattice 𝐿 ( 𝑋 , ⊲ ) with meet and join calculated as in Proposition 4.3; 2. ¬ ⊲ is a precomplementation on 𝐿 ( 𝑋 , ⊲ ) ; 3. if ⊲ is reflexive, then ¬ ⊲ is a protocomplementation on 𝐿 ( 𝑋 , ⊲ ) .

One subtlety is that the 0 of the lattice 𝐿 ( 𝑋 , ⊲ ) is 𝑐 ⊲ ( ⌀ ) , which is equal to ⌀ in reflexive frames but not in arbitrary relational frames, where the situation with 0 is as follows.

For a relational frame ( 𝑋 , ⊲ ) and 𝑥 ∈ 𝑋 , x is absurd if there is no y with 𝑦 ⊲ 𝑥 .

For any relational frame ( 𝑋 , ⊲ ) : 1. the 0 of 𝐿 ( 𝑋 , ⊲ ) is the set of absurd states, also equal to ¬ ⊲ 1 ; 2. ¬ ⊲ 0 = 1 iff there is no 𝑦 ∈ 𝑋 and absurd 𝑥 ∈ 𝑋 with 𝑥 ⊲ 𝑦 .

For part 1, an absurd state x belongs to every 𝑐 ⊲ -fixpoint, since it holds vacuously that ∀ 𝑥 ′ ⊲ 𝑥 ∃ 𝑥 ″ ⊳ 𝑥 ′ : 𝑥 ″ ∈ 𝐴 , so the set of absurd states is a subset of every 𝑐 ⊲ -fixpoint and hence equal to 0. Moreover, since 1 = 𝑋 , we have 𝑥 ∈ ¬ ⊲ 1 only if x is absurd, so ¬ ⊲ 1 = 0 . Part 2 follows immediately from part 1. □ A more general approach to negation, which would allow ¬ 1 ≠ 0 , uses triples ( 𝑋 , ⊲ , 𝐹 ) where ( 𝑋 , ⊲ ) is a relational frame and F is a distinguished 𝑐 ⊲ -fixpoint. Then we define the negation operation by ¬ ⊲ , 𝐹 𝐴 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑥 ′ ⊲ 𝑥 ( 𝑥 ′ ∈ 𝐴 ⇒ ∃ 𝑥 ″ ⊳ 𝑥 ′ : 𝑥 ″ ∈ 𝐹 ) } . Then ¬ ⊲ is the special case ¬ ⊲ , 0 . The ¬ ⊲ , 𝐹 operation can in turn be obtained from the implication operation → ⊲ studied in Appendix B, as ¬ ⊲ , 𝐹 𝐴 = 𝐴 → ⊲ 𝐹 . We will return to ¬ ⊲ , 𝐹 once more in Theorem 4.29.

It is easy to see that if ⊲ is a reflexive and transitive relation ≤, then the lattice of 𝑐 ⊲ -fixpoints is simply the complete Heyting algebra of all downsets of ( 𝑋 , ≤ ) , as observed in [15] (pp. 139–140) (cf. [78] (Prop. 4.1.1), [21] (Prop. 2.9(ii))). Note, however, that this construction can only realize special complete Heyting algebras, namely those in which every element is a join of completely join-prime elements [79] (Prop. 1.1). By contrast, the result in Theorem 4.13.1 below applies to all complete Heyting algebras (cf. [47], Section 4).

Figure 9 and Figure 10 show reflexive relational frames that give rise to the lattices with negations in Figure 7 and Figure 8, respectively. When drawing frames, an arrow with a triangle arrowhead from y to x indicates 𝑦 ⊳ 𝑥 . Thus, we draw the directed graph ( 𝑋 , ⊳ ) to represent the frame ( 𝑋 , ⊲ ) . Reflexive arrows are not shown but are assumed. The 𝑐 ⊲ -fixpoints, excluding ⌀ and X, are outlined. Looking at a diagram of a relational frame, one can check that A is a 𝑐 ⊲ -fixpoint by checking that the following holds: from any 𝑥 ∈ 𝑋 \ 𝐴 , you can step forward along an arrow to a state 𝑥 ′ that cannot step backward along an arrow into A.

Informally, “from x you can see a state that cannot be seen from A”. Figure 9. Reflexive frame representations of the lattice expansions in Figure 7. Figure 10. Reflexive frame representations of the lattice expansions in Figure 8.

For instance, in the reflexive frame on the left of Figure 9, { 𝑥 } is a 𝑐 ⊲ -fixpoint since obviously any state outside of { 𝑥 } can see a state that cannot be seen from { 𝑥 } ; the only close call is y, but y can see z, which cannot be seen from { 𝑥 } . By contrast, { 𝑦 } is not a 𝑐 ⊲ -fixpoint, because although 𝑥 ∉ { 𝑦 } , x cannot see a state that cannot be seen from { 𝑦 } . For a more interesting calculation, consider the reflexive frame on the right of Figure 10. Here { 𝑧 } is a 𝑐 ⊲ -fixpoint; the only close call is w, but w can see u, which cannot be seen from z (though u can see z, but that is irrelevant). By contrast, { 𝑤 } is not a 𝑐 ⊲ -fixpoint, because z cannot see a state that cannot be seen from w (note that the arrow between v and w is symmetric).

A more efficient procedure for calculating 𝑐 ⊲ -fixpoints, using Ganter’s [80] algorithm for calculating fixpoints of a closure operator, is implemented in one of the notebooks mentioned in Section 1.

From this starting point, algebras for intuitionistic logicterm, orthologicterm, and classical logicterm arise from natural constraints on the relation ⊲. It has long been known that reflexive frames in which ⊲ is symmetric give rise to ortholattices [52] (Sections 32–34), and all complete ortholattices can be so represented [81], which yields a relational semanticsterm for orthologicterm [16] (cf. [54]). To characterize the complete Heyting case, [21] uses the following concepts.16 Given a relational frame ( 𝑋 , ⊲ ) and 𝑥 , 𝑦 ∈ 𝑋 : 1. x pre-refines y if for all 𝑧 ∈ 𝑋 , 𝑧 ⊲ 𝑥 implies 𝑧 ⊲ 𝑦 ; 2. x post-refines y if for all 𝑧 ∈ 𝑋 , 𝑥 ⊲ 𝑧 implies 𝑦 ⊲ 𝑧 ; 3. x refines y if x pre-refines and post-refines y; 4. x is compossible with y if there is a non-absurd 𝑤 ∈ 𝑋 that refines x and pre-refines y.

We say that ⊲ is compossible if whenever 𝑥 ⊲ 𝑦 , then x is compossible with y.

Note that if ⊲ is symmetric, then pre-refinement and post-refinement are equivalent, and x is compossible with y just in case they have a common non-absurd refinement.

The following lemma will be useful below.

For any relational frame ( 𝑋 , ⊲ ) and 𝑥 , 𝑦 ∈ 𝑋 , if x pre-refines y, then for every 𝑐 ⊲ -fixpoint A, if 𝑦 ∈ 𝐴 , then 𝑥 ∈ 𝐴 .

If 𝑥 ′ ⊲ 𝑥 , then since x pre-refines y, 𝑥 ′ ⊲ 𝑦 . Then since 𝑦 ∈ 𝐴 , there is an 𝑥 ″ ⊳ 𝑥 ′ with 𝑥 ″ ∈ 𝐴 . Hence for any 𝑥 ′ ⊲ 𝑥 there is an 𝑥 ″ ⊳ 𝑥 ′ with 𝑥 ″ ∈ 𝐴 , which shows 𝑥 ∈ 𝐴 . □ Note that if x post-refines y, then for any A that y rejects in the sense of Remark 4.2, x rejects A too. Hence if x refines y, then x accepts every proposition that y does and rejects every proposition that y does.

Now we can characterize complete Heyting algebras, ortholattices, and Boolean algebras using relational frames as follows. For a proof, see [21] (Theorems 2.21 and 3.18). Part 1 also follows from our results concerning lattices with implications in Appendix B.

1. ( 𝐿 , ¬ ) is a complete Heyting algebra with pseudocomplementationterm ¬ iff ( 𝐿 , ¬ ) is isomorphic to ( 𝐿 ( 𝑋 , ⊲ ) , ¬ ⊲ ) for a relational frame ( 𝑋 , ⊲ ) in which ⊲ is reflexive and compossible. 2. ( 𝐿 , ¬ ) is a complete ortholattice with orthocomplementation ¬ iff ( 𝐿 , ¬ ) is isomorphic to ( 𝐿 ( 𝑋 , ⊲ ) , ¬ ⊲ ) for a relational frame ( 𝑋 , ⊲ ) in which ⊲ is reflexive and symmetric. 3. ( 𝐿 , ¬ ) is a complete Boolean algebra with Boolean negation ¬ iff ( 𝐿 , ¬ ) is isomorphic to ( 𝐿 ( 𝑋 , ⊲ ) , ¬ ⊲ ) for a relational frame ( 𝑋 , ⊲ ) in which ⊲ is reflexive, symmetric, and compossible.

Not every pseudocomplemented lattice ( 𝐿 , ¬ ) is a Heyting algebra, as Heyting algebras require a relative pseudocomplementationterm → such that for all 𝑎 , 𝑏 , 𝑐 ∈ 𝐿 , 𝑎 ∧ 𝑏 ≤ 𝑐 iff 𝑎 ≤ 𝑏 → 𝑐 , which implies that L is distributive. Thus, let us isolate a condition just for pseudocomplementationterm, which is the conjunction of two conditions: 𝑎 ∧ ¬ 𝑎 = 0 , and 𝑎 ∧ 𝑏 = 0 implies 𝑎 ≤ ¬ 𝑏 . Let us also isolate the condition for double negation introduction that we want for weak pseudocomplementationsterm, as well as the condition for double negation elimination that turns weak pseudocomplementationsterm into orthocomplementations (Lemma 3.4.3).

For any relational frame ( 𝑋 , ⊲ ) , in each of the following pairs, (a) and (b) are equivalent: (a) for all 𝑐 ⊲ -fixpoints A, we have 𝐴 ∩ ¬ ⊲ 𝐴 = 0 ; (b) for all non-absurd 𝑥 ∈ 𝑋 , there is a 𝑧 ⊲ 𝑥 that pre-refines x. (a) for all 𝑐 ⊲ -fixpoints A, we have 𝐴 ⊆ ¬ ⊲ ¬ ⊲ 𝐴 ; (b) pseudosymmetry: for all 𝑥 ∈ 𝑋 and 𝑦 ⊲ 𝑥 , there is a 𝑧 ⊲ 𝑦 that pre-refines x. (a) for all 𝑐 ⊲ -fixpoints 𝐴 , 𝐵 , if 𝐴 ∩ 𝐵 = 0 , then 𝐴 ⊆ ¬ ⊲ 𝐵 . (b) weak compossibility: for all 𝑥 ∈ 𝑋 and 𝑦 ⊲ 𝑥 , there is a non-absurd z that pre-refines y and x. (a) for all 𝑐 ⊲ -fixpoints A, we have ¬ ⊲ ¬ ⊲ 𝐴 ⊆ 𝐴 ; (b) for all 𝑥 ∈ 𝑋 and 𝑦 ⊲ 𝑥 , there is a 𝑦 ′ ⊲ 𝑥 such that for all 𝑧 ∈ 𝑋 , if 𝑧 ⊲ 𝑦 ′ then 𝑦 ⊲ 𝑧 .

For part 1, suppose (b) holds, 𝑥 ∈ 𝐴 , and 𝑥 ∉ 0 , so by Lemma 4.7.1, x is non-absurd. Then by (b) there is a 𝑧 ⊲ 𝑥 that pre-refines x, which with Lemma 4.12 implies 𝑧 ∈ 𝐴 and hence 𝑥 ∉ ¬ ⊲ 𝐴 . This proves 𝐴 ∩ ¬ ⊲ 𝐴 ⊆ 0 . Conversely, suppose (b) does not hold, so there is a non-absurd x that is not pre-refined by any state open to x. First, we claim 𝑥 ∈ ¬ ⊲ 𝑐 ⊲ ( { 𝑥 } ) . For suppose 𝑦 ⊲ 𝑥 . Since y does not pre-refine x, there is a 𝑧 ⊲ 𝑦 such that 𝑧 ⊲ 𝑥 . This shows 𝑦 ∉ 𝑐 ⊲ ( { 𝑥 } ) , so 𝑥 ∈ ¬ ⊲ 𝑐 ⊲ ( { 𝑥 } ) and hence 𝑥 ∈ 𝑐 ⊲ ( { 𝑥 } ) ∩ ¬ ⊲ 𝑐 ⊲ ( { 𝑥 } ) . Then since x is non-absurd, we have 𝑐 ⊲ ( { 𝑥 } ) ∩ ¬ ⊲ 𝑐 ⊲ ( { 𝑥 } ) ≠ 0 .

For part 2, suppose (b) holds, 𝑥 ∈ 𝐴 , and 𝑦 ⊲ 𝑥 . Then by pseudosymmetry, there is a 𝑧 ⊲ 𝑦 that pre-refines x. Since 𝑥 ∈ 𝐴 , it follows by Lemma 4.12 that 𝑧 ∈ 𝐴 , which with 𝑧 ⊲ 𝑦 implies 𝑦 ∉ ¬ ⊲ 𝐴 . Thus, we have 𝑥 ∈ ¬ ⊲ ¬ ⊲ 𝐴 , so 𝐴 ⊆ ¬ ⊲ ¬ ⊲ 𝐴 . Conversely, suppose (b) does not hold, so there are 𝑥 , 𝑦 ∈ 𝑋 with 𝑦 ⊲ 𝑥 such that for all 𝑧 ⊲ 𝑦 , there is some 𝑤 ⊲ 𝑧 with 𝑤 ⊲ 𝑥 , which implies 𝑧 ∉ 𝑐 ⊲ ( { 𝑥 } ) . Hence 𝑦 ∈ ¬ 𝑐 ⊲ ( { 𝑥 } ) , which with 𝑦 ⊲ 𝑥 implies 𝑥 ∉ ¬ ⊲ ¬ 𝑐 ⊲ ( { 𝑥 } ) . Yet 𝑥 ∈ 𝑐 ⊲ ( { 𝑥 } ) , so 𝑐 ⊲ ( { 𝑥 } ) ⊆ ¬ ⊲ ¬ 𝑐 ⊲ ( { 𝑥 } ) .

For part 3, suppose (b) holds, 𝐴 ∩ 𝐵 = 0 , 𝑥 ∈ 𝐴 , but 𝑥 ∉ ¬ ⊲ 𝐵 , so there is a 𝑦 ⊲ 𝑥 with 𝑦 ∈ 𝐵 . Then by weak compossibility, there is a non-absurd z that pre-refines y and x. Hence 𝑧 ∈ 𝐴 ∩ 𝐵 by Lemma 4.12. Since z is non-absurd, it follows that 𝐴 ∩ 𝐵 ≠ 0 by Lemma 4.7.1. Conversely, suppose (b) does not hold, so there are 𝑥 , 𝑦 ∈ 𝑋 with 𝑦 ⊲ 𝑥 but there is no non-absurd z that pre-refines y and x. It follows that 𝑐 ⊲ ( { 𝑦 } ) ∩ 𝑐 ⊲ ( { 𝑥 } ) = 0 . But since 𝑦 ⊲ 𝑥 , we have 𝑥 ∉ ¬ ⊲ 𝑐 ⊲ ( { 𝑦 } ) , so 𝑐 ⊲ ( { 𝑥 } ) ⊆ ¬ ⊲ 𝑐 ⊲ ( { 𝑦 } ) .

For part 4, suppose (b) holds and 𝑥 ∉ 𝐴 , so there is a 𝑦 ⊲ 𝑥 such that for all 𝑤 ⊳ 𝑦 , 𝑤 ∉ 𝐴 . By (b), there is a 𝑦 ′ ⊲ 𝑥 such that for all 𝑧 ∈ 𝑋 , 𝑧 ⊲ 𝑦 ′ implies 𝑦 ⊲ 𝑧 and hence 𝑧 ∉ 𝐴 by the previous sentence. Thus, 𝑦 ′ ∈ ¬ ⊲ 𝐴 , which with 𝑦 ′ ⊲ 𝑥 implies 𝑥 ∉ ¬ ⊲ ¬ ⊲ 𝐴 . Conversely, suppose (b) does not hold, so there is some 𝑦 ⊲ 𝑥 such that (i) for all 𝑦 ′ ⊲ 𝑥 , there is a 𝑧 ⊲ 𝑦 ′ such that 𝑦 ⊲ 𝑧 . Let 𝐴 = { 𝑤 ∈ 𝑋 ∣ 𝑦 ⊲ 𝑤 } . Then A is a 𝑐 ⊲ -fixpoint, for if 𝑣 ∉ 𝐴 , then 𝑦 ⊲ 𝑣 and for all 𝑢 ⊳ 𝑦 , 𝑢 ∉ 𝐴 . Moreover, 𝑥 ∈ ¬ ⊲ ¬ ⊲ 𝐴 by (i), but 𝑥 ∉ 𝐴 . □ Note the relation between the (b) conditions in parts 1 and 2 of Lemma 4.14: the first says that if 𝑦 ⊲ 𝑥 , then there is a pre-refinement of x that is open to x, while the second says that if 𝑦 ⊲ 𝑥 , then there is a pre-refinement of x that is open to y. In Appendix B, we consider a pair of analogous conditions for an implication → ⊲ in place of the negation ¬ ⊲ (Lemma B.1).

Concerning part 1 of Proposition 4.14, it turns out (Theorem 4.24.2) that for the purposes of representing protocomplementations, we can strengthen the condition in 1(b) to reflexivity without loss of generality. Concerning part 2, pseudosymmetry is a weakening of the symmetry property that yields ortholattices. Pseudosymmetry says that if y is open to x, then while x might not be open to y, some pre-refinement of x is open to y. In the terms of Remark 4.2, pseudosymmetry corresponds to the condition that for any proposition A and 𝑦 ∈ 𝑋 , if 𝑦 accepts ¬ 𝐴 , then 𝑦 rejects 𝐴 . For assume pseudosymmetry and that y does not reject A, so there is an 𝑥 ⊳ 𝑦 with 𝑥 ∈ 𝐴 ; then taking z as in the statement of pseudosymmetry, we have 𝑧 ∈ 𝐴 by Lemma 4.12, so 𝑧 ⊲ 𝑦 implies that y does not accept ¬ 𝐴 . Conversely, if pseudosymmetry fails, then y does not reject 𝑐 ⊲ ( { 𝑥 } ) but does accept ¬ ⊲ 𝑐 ⊲ ( { 𝑥 } ) .

In Dunn’s setting with triples ( 𝑋 , ⊲ , ≤ ) referenced in Section 4.1, 𝐴 ⊆ ¬ ¬ 𝐴 corresponds to the symmetry of ⊲ ([44] (Thm. 2.10), [83] (Thm. 11.41)), which in our setting overshoots and makes ¬ an orthocomplementation.

We will also consider the following strengthening of pseudosymmetry.

A relational frame ( 𝑋 , ⊲ ) is strongly pseudosymmetric if for all 𝑥 ∈ 𝑋 and 𝑦 ⊲ 𝑥 , there is a 𝑧 ⊲ 𝑦 such that z pre-refines x and x pre-refines z.

Note that if z pre-refines x and vice versa, then x and z belong to exactly the same propositions, i.e., 𝑐 ⊲ -fixpoints, by Lemma 4.12 (though they may reject different propositions).

We will see (Theorem 4.24.4) that lattices with weak pseudocomplementationsterm can be represented using pseudosymmetric reflexive frames—or even strongly pseudosymmetric ones at the expense of a bigger frame.

In Figure 9, the reflexive frame on the left is pseudosymmetric but not strongly pseudosymmetric; the frame on the right is strongly pseudosymmetric but not symmetric; and the frame below the other two is not pseudosymmetric. In Figure 10, the reflexive frame on the left is symmetric while the one on the right is strongly pseudosymmetric but not symmetric.

Finally, let us turn from lattices to our formal language 𝐿 . Proposition 4.5 leads immediately to the following relational semanticsterm for 𝐿 .

A relational model is a triple 𝑀 = ( 𝑋 , ⊲ , 𝑉 ) where ( 𝑋 , ⊲ ) is a relational frame and V maps each 𝑝 ∈ Prop to a 𝑐 ⊲ -fixpoint 𝑉 ( 𝑝 ) ⊆ 𝑋 . We define a forcing relation between states in 𝑀 and formulas of 𝐿 as follows: 1. 𝑀 , 𝑥 ⊩ 𝑝 iff 𝑥 ∈ 𝑉 ( 𝑝 ) ; 2. 𝑀 , 𝑥 ⊩ ¬ 𝜑 iff for all 𝑥 ′ ⊲ 𝑥 , 𝑀 , 𝑥 ′ ⊮ 𝜑 ; 3. 𝑀 , 𝑥 ⊩ 𝜑 ∧ 𝜓 iff 𝑀 , 𝑥 ⊩ 𝜑 and 𝑀 , 𝑥 ⊩ 𝜓 ; 4. 𝑀 , 𝑥 ⊩ 𝜑 ∨ 𝜓 iff ∀ 𝑥 ′ ⊲ 𝑥 ∃ 𝑥 ″ ⊳ 𝑥 ′ : 𝑀 , 𝑥 ″ ⊩ 𝜑 or 𝑀 , 𝑥 ″ ⊩ 𝜓 .

Given a class 𝐶 of relational frames, we define 𝜑 ⊧ 𝐶 𝜓 if for all ( 𝑋 , ⊲ ) ∈ 𝐶 , all models 𝑀 based on ( 𝑋 , ⊲ ) , and all 𝑥 ∈ 𝑋 , if 𝑀 , 𝑥 ⊩ 𝜑 , then 𝑀 , 𝑥 ⊩ 𝜓 .

Where ⟦ 𝜑 ⟧ 𝑀 = { 𝑥 ∈ 𝑋 ∣ 𝑀 , 𝑥 ⊩ 𝜑 } , an easy induction shows the following.

For any relational model 𝑀 = ( 𝑋 , ⊲ , 𝑉 ) and 𝜑 ∈ 𝐿 , ⟦ 𝜑 ⟧ 𝑀 is a 𝑐 ⊲ -fixpoint.

Consider a valuation V on the reflexive frame in Figure 11 that sets 𝑉 ( 𝑝 ) = { 𝑥 , 𝑦 } , 𝑉 ( 𝑞 ) = { 𝑥 } , and 𝑉 ( 𝑟 ) = { 𝑤 , 𝑧 } . Then observe that 𝑀 , 𝑦 ⊩ 𝑞 ∨ 𝑟 , even though 𝑀 , 𝑦 ⊮ 𝑞 and 𝑀 , 𝑦 ⊮ 𝑟 . Thus, 𝑀 , 𝑦 ⊩ 𝑝 ∧ ( 𝑞 ∨ 𝑟 ) . However, 𝑀 , 𝑦 ⊮ ( 𝑝 ∧ 𝑞 ) ∨ ( 𝑝 ∧ 𝑟 ) , since y can see w, but w cannot be seen from a state forcing 𝑝 ∧ 𝑞 (namely from x) or a state forcing 𝑝 ∧ 𝑟 (since there are no such states). Thus, this model provides a counterexample to the distributive lawterm. Also observe that no state forces ¬ 𝑝 , so 𝑀 , 𝑧 ⊩ ¬ ¬ 𝑝 , yet 𝑀 , 𝑧 ⊮ 𝑝 . Thus, this model provides a counterexample to double negation elimination. Similar calculations can be done upon evaluating propositional variables as other 𝑐 ⊲ -fixpoints in Figure 9 or Figure 10.

4.2. Discrete Representation of Lattices with Negation Having seen how to go from a relational frame to a lattice with negation, let us now consider the converse direction: given a lattice with negation, we build a relational frame into whose lattice of c⊲-fixpoints the given lattice embeds. The following definition and result are from [21] with some details expanded.

Let L be a lattice and P a set of pairs of elements of L. Define a binary relation ⊲ on P by ( 𝑎 , 𝑏 ) ⊲ ( 𝑐 , 𝑑 ) if 𝑐 ≰ 𝑏 . Then we say P is separating if for all 𝑎 , 𝑏 ∈ 𝐿 : 1. if 𝑎 ≰ 𝑏 , then there is a ( 𝑐 , 𝑑 ) ∈ 𝑃 with 𝑐 ≤ 𝑎 and 𝑐 ≰ 𝑏 ; 2. for all ( 𝑐 , 𝑑 ) ∈ 𝑃 , if 𝑐 ≰ 𝑏 , then there is a ( 𝑐 ′ , 𝑑 ′ ) ⊲ ( 𝑐 , 𝑑 ) such that for all ( 𝑐 ″ , 𝑑 ″ ) ⊳ ( 𝑐 ′ , 𝑑 ′ ) , we have 𝑐 ″ ≰ 𝑏 .

One can interpret the pairs in P intuitively as in Remark 4.2: the state ( 𝑎 , 𝑏 ) accepts everything entailed by proposition a and rejects everything that entails proposition b; and ( 𝑎 , 𝑏 ) is open to ( 𝑐 , 𝑑 ) if ( 𝑎 , 𝑏 ) does not reject anything that ( 𝑐 , 𝑑 ) accepts, i.e., 𝑐 ≰ 𝑏 .

A complete embedding of a lattice L into a lattice 𝐿 ′ is an injective map 𝑓 : 𝐿 ⟶ 𝐿 ′ that preserves all existing meets and joins of L. A complete embedding of lattice expansions ( 𝐿 , ¬ ) is defined in the same way but also requiring the preservation of ¬.

Let L be a lattice and P a separating set of pairs of elements of L. For 𝑎 ∈ 𝐿 , define 𝑓 ( 𝑎 ) = { ( 𝑥 , 𝑦 ) ∈ 𝑃 ∣ 𝑥 ≤ 𝑎 } . Then: 1. f is a complete embedding of L into 𝐿 ( 𝑃 , ⊲ ) ; 2. if L is complete, then f is an isomorphism from L to 𝐿 ( 𝑃 , ⊲ ) .

For part 1, condition 2 of Definition 4.22 implies that 𝑓 ( 𝑏 ) is a 𝑐 ⊲ -fixpoint for each 𝑏 ∈ 𝐿 . Clearly f preserves all existing meets: 𝑓 ( ⋀ 𝑎 ∈ 𝐴 𝑎 ) = { ( 𝑥 , 𝑦 ) ∈ 𝑃 ∣ 𝑥 ≤ ⋀ 𝑎 ∈ 𝐴 𝑎 } = ⋂ 𝑎 ∈ 𝐴 { ( 𝑥 , 𝑦 ) ∈ 𝑃 ∣ 𝑥 ≤ 𝑎 } = ⋂ 𝑎 ∈ 𝐴 𝑓 ( 𝑎 ) . For joins, to see that 𝑓 ( ⋁ 𝐴 ) ⊆ ⋁ { 𝑓 ( 𝑎 ) ∣ 𝑎 ∈ 𝐴 } , suppose that ( 𝑥 , 𝑦 ) ∈ 𝑓 ( ⋁ 𝐴 ) and ( 𝑥 ′ , 𝑦 ′ ) ⊲ ( 𝑥 , 𝑦 ) . Hence 𝑥 ≤ ⋁ 𝐴 but 𝑥 ≰ 𝑦 ′ , so ⋁ 𝐴 ≰ 𝑦 ′ , which implies 𝑎 ≰ 𝑦 ′ for some 𝑎 ∈ 𝐴 . Then part 1 of Definition 4.22 yields an ( 𝑥 ″ , 𝑦 ″ ) ∈ 𝑓 ( 𝑎 ) with ( 𝑥 ′ , 𝑦 ′ ) ⊲ ( 𝑥 ″ , 𝑦 ″ ) . This proves that ( 𝑥 , 𝑦 ) ∈ ⋁ { 𝑓 ( 𝑎 ) ∣ 𝑎 ∈ 𝐴 } . The converse inclusion ⋁ { 𝑓 ( 𝑎 ) ∣ 𝑎 ∈ 𝐴 } ⊆ 𝑓 ( ⋁ 𝐴 ) follows from order preservation, which follows from meet preservation. Finally, part 1 of Definition 4.22 ensures that f is injective.

For part 2, we claim f is surjective. Given a 𝑐 ⊲ -fixpoint A, define 𝑎 = ⋁ { 𝑎 𝑖 ∣ ∃ 𝑏 𝑖 : ( 𝑎 𝑖 , 𝑏 𝑖 ) ∈ 𝐴 } . We claim 𝐴 = 𝑓 ( 𝑎 ) . For 𝐴 ⊆ 𝑓 ( 𝑎 ) , suppose ( 𝑎 𝑖 , 𝑏 𝑖 ) ∈ 𝐴 . Then by definition of a, 𝑎 𝑖 ≤ 𝑎 , so ( 𝑎 𝑖 , 𝑏 𝑖 ) ∈ 𝑓 ( 𝑎 ) . For 𝐴 ⊇ 𝑓 ( 𝑎 ) , suppose ( 𝑐 , 𝑑 ) ∈ 𝑓 ( 𝑎 ) , so 𝑐 ≤ 𝑎 . Since A is a 𝑐 ⊲ -fixpoint, to show ( 𝑐 , 𝑑 ) ∈ 𝐴 , it suffices to show that for every ( 𝑐 , ′ 𝑑 ′ ) ⊲ ( 𝑐 , 𝑑 ) there is a ( 𝑐 ″ , 𝑑 ″ ) ⊳ ( 𝑐 ′ , 𝑑 ′ ) with ( 𝑐 ″ , 𝑑 ″ ) ∈ 𝐴 . Suppose ( 𝑐 , ′ 𝑑 ′ ) ⊲ ( 𝑐 , 𝑑 ) , so 𝑐 ≰ 𝑑 ′ , which with 𝑐 ≤ 𝑎 implies 𝑎 ≰ 𝑑 ′ . Then for some ( 𝑎 𝑖 , 𝑏 𝑖 ) ∈ 𝐴 , we have 𝑎 𝑖 ≰ 𝑑 ′ . Setting ( 𝑐 ″ , 𝑑 ″ ) = ( 𝑎 𝑖 , 𝑏 𝑖 ) , from 𝑎 𝑖 ≰ 𝑑 ′ we have ( 𝑐 ′ , 𝑑 ′ ) ⊲ ( 𝑐 ″ , 𝑑 ″ ) , and ( 𝑐 ″ , 𝑑 ″ ) ∈ 𝐴 , so we are done. □ Different choices of a separating set P of pairs can lead to more or less efficient representations of different types of lattices. Cases where L is an arbitrary lattice, ortholattice, or Heyting algebra are covered in [21] (Prop. 3.16). In the case of bounded latticesterm with ¬, we choose the pairs with the ¬ operation in mind. But the following theorem applies to bounded latticesterm in general, given the point in Section 3 that any bounded latticeterm can be equipped with a weak pseudocomplementationterm. In Section 6 and Appendix B, we prove analogous theorems for bounded latticesterm with implications. Recall that a set of elements in a lattice L is join-dense (resp. meet-dense) if every element of L is a join (resp. meet) of a (possibly infinite) set of elements of L. E.g., the set of all elements of L is trivially join- (and meet-) dense in L.

Let L be a bounded latticeterm, V a join-dense set of elements of L, and Λ a meet-dense set of elements of L. Given a set P of pairs of elements of L, define ⊲ on P by ( 𝑎 , 𝑏 ) ⊲ ( 𝑐 , 𝑑 ) if 𝑐 ≰ 𝑏 .

1. If ¬ is a precomplementation on L, then where 𝑃 = { ( 𝑎 , ¬ 𝑎 ) ∣ 𝑎 ∈ 𝐿 } ∪ { ( 1 , 𝑏 ) ∣ 𝑏 ∈ Λ } , there is a complete embedding of ( 𝐿 , ¬ ) into ( 𝐿 ( 𝑃 , ⊲ ) , ¬ ⊲ ) . 2. If ¬ is a protocomplementation on L, then where 𝑃 = { ( 𝑎 , ¬ 𝑎 ) ∣ 𝑎 ∈ 𝐿 , 𝑎 ≠ 0 } ∪ { ( 1 , 𝑏 ) ∣ 𝑏 ∈ Λ , 𝑏 ≠ 1 } , there is a complete embedding of ( 𝐿 , ¬ ) into ( 𝐿 ( 𝑃 , ⊲ ) , ¬ ⊲ ) , and ⊲ is reflexive. 3. If ¬ is an ultraweak pseudocomplementationterm on L, then where 𝑃 = { ( 𝑎 , ¬ 𝑎 ) ∣ 𝑎 ∈ V } ∪ { ( 1 , 𝑏 ) ∣ 𝑏 ∈ Λ } , there is a complete embedding of ( 𝐿 , ¬ ) into ( 𝐿 ( 𝑃 , ⊲ ) , ¬ ⊲ ) , and ⊲ is pseudosymmetric (and strongly pseudosymmetric if V = 𝐿 ). 4. If ¬ is a weak pseudocomplementationterm on L, then where 𝑃 = { ( 𝑎 , ¬ 𝑎 ) ∣ 𝑎 ∈ V , 𝑎 ≠ 0 } ∪ { ( 1 , 𝑏 ) ∣ 𝑏 ∈ Λ , 𝑏 ≠ 1 } , there is a complete embedding of ( 𝐿 , ¬ ) into ( 𝐿 ( 𝑃 , ⊲ ) , ¬ ⊲ ) , and ⊲ is reflexive and pseudosymmetric (and strongly pseudosymmetric if V = 𝐿 ). Moreover, if ¬ is a pseudocomplementationterm, then ⊲ is weakly compossible.

In each case, if L is complete, then the embedding is an isomorphism.

Note first that (i) for all parts of the theorem, for ( 𝑎 , 𝑏 ) ∈ 𝑃 , we have ¬ 𝑎 ≤ 𝑏 , using that ¬ 1 = 0 .

First we claim that in each part, P is separating in the sense of Definition 4.22. To prove part 1 of Definition 4.22, suppose 𝑎 ≰ 𝑏 . In parts 1 and 2 of the theorem, we take ( 𝑐 , 𝑑 ) = ( 𝑎 , ¬ 𝑎 ) . Since 𝑎 ≠ 0 , we have ( 𝑎 , ¬ 𝑎 ) ∈ 𝑃 . In parts 3 and 4, from 𝑎 ≰ 𝑏 we obtain a nonzero 𝑎 ′ ∈ V such that 𝑎 ′ ≤ 𝑎 and 𝑎 ′ ≰ 𝑏 , and we set ( 𝑐 , 𝑑 ) = ( 𝑎 ′ , ¬ 𝑎 ′ ) . To prove part 2 of Definition 4.22, suppose ( 𝑐 , 𝑑 ) ∈ 𝑃 and 𝑐 ≰ 𝑏 . Hence there is some 𝑏 ′ ∈ Λ such that 𝑐 ≰ 𝑏 ′ and 𝑏 ≤ 𝑏 ′ . Let ( 𝑐 ′ , 𝑑 ′ ) = ( 1 , 𝑏 ′ ) . Since 𝑐 ≰ 𝑏 ′ , we have 𝑏 ′ ≠ 1 and hence ( 𝑐 ′ , 𝑑 ′ ) ∈ 𝑃 , and also ( 𝑐 ′ , 𝑑 ′ ) ⊲ ( 𝑐 , 𝑑 ) . Now consider any ( 𝑐 ″ , 𝑑 ″ ) ∈ 𝑃 with ( 𝑐 ′ , 𝑑 ′ ) ⊲ ( 𝑐 ″ , 𝑑 ″ ) . Then 𝑐 ″ ≰ 𝑑 ′ = 𝑏 ′ , so 𝑐 ″ ≰ 𝑏 . Hence part 2 of Definition 4.22 holds. Thus, by Proposition 4.23, f is a complete embedding of L into 𝐿 ( 𝑃 , ⊲ ) , which is a lattice isomorphism if L is complete.

Next we claim that for each part, 𝑓 ( ¬ 𝑎 ) = ¬ ⊲ 𝑓 ( 𝑎 ) . Suppose ( 𝑥 , 𝑦 ) ∈ 𝑓 ( ¬ 𝑎 ) , so 𝑥 ≤ ¬ 𝑎 , and ( 𝑥 ′ , 𝑦 ′ ) ⊲ ( 𝑥 , 𝑦 ) . If 𝑥 ′ ≤ 𝑎 , then ¬ 𝑎 ≤ ¬ 𝑥 ′ , which with 𝑥 ≤ ¬ 𝑎 implies 𝑥 ≤ ¬ 𝑥 ′ , which with ¬ 𝑥 ′ ≤ 𝑦 ′ from (i) implies 𝑥 ≤ 𝑦 ′ , contradicting ( 𝑥 ′ , 𝑦 ′ ) ⊲ ( 𝑥 , 𝑦 ) . Thus, 𝑥 ′ ≰ 𝑎 , so ( 𝑥 ′ , 𝑦 ′ ) ∉ 𝑓 ( 𝑎 ) . Hence ( 𝑥 , 𝑦 ) ∈ ¬ ⊲ 𝑓 ( 𝑎 ) . Conversely, let ( 𝑥 , 𝑦 ) ∈ 𝑃 \ 𝑓 ( ¬ 𝑎 ) , so 𝑥 ≰ ¬ 𝑎 . In part 1, we immediately have ( 𝑎 , ¬ 𝑎 ) ∈ 𝑃 , and ( 𝑎 , ¬ 𝑎 ) ⊲ ( 𝑥 , 𝑦 ) , so ( 𝑥 , 𝑦 ) ∉ ¬ ⊲ 𝑓 ( 𝑎 ) . For part 2, we use that ¬ 0 = 1 , so from 𝑥 ≰ ¬ 𝑎 we have 𝑎 ≠ 0 , so ( 𝑎 , ¬ 𝑎 ) ∈ 𝑃 . For part 3, we have that 𝑥 ≰ ¬ 𝑎 implies 𝑎 ≰ ¬ 𝑥 (Lemma 3.4.2), so there is some 𝑎 ′ ∈ V such that 𝑎 ′ ≤ 𝑎 but 𝑎 ′ ≰ ¬ 𝑥 , so 𝑥 ≰ ¬ 𝑎 ′ . Hence ( 𝑎 ′ , ¬ 𝑎 ′ ) ∈ 𝑃 and ( 𝑎 ′ , ¬ 𝑎 ′ ) ⊲ ( 𝑥 , 𝑦 ) , which with 𝑎 ′ ≤ 𝑎 yields ( 𝑥 , 𝑦 ) ∉ ¬ ⊲ 𝑓 ( 𝑎 ) . For part 4, we again use that ¬ 0 = 1 , so from 𝑥 ≰ ¬ 𝑎 ′ we have 𝑎 ′ ≠ 0 , so ( 𝑎 ′ , ¬ 𝑎 ′ ) ∈ 𝑃 .

For parts 2 and 4, that ⊲ is reflexive follows from the anti-inflationary property of semicomplementations (Lemma 3.4.1). For parts 3 and 4, we prove pseudosymmetry. Suppose ( 𝑐 , 𝑑 ) ⊲ ( 𝑎 , 𝑏 ) , which implies ¬ 𝑐 ≤ 𝑑 by (i) and 𝑎 ≰ 𝑑 . Hence 𝑎 ≰ ¬ 𝑐 , so there is a nonzero 𝑎 ′ ∈ V such that 𝑎 ′ ≤ 𝑎 but 𝑎 ′ ≰ ¬ 𝑐 , which implies 𝑐 ≰ ¬ 𝑎 ′ (Lemma 3.4.2). Hence ( 𝑎 ′ , ¬ 𝑎 ′ ) ⊲ ( 𝑐 , 𝑑 ) , and since 𝑎 ′ ≤ 𝑎 , ( 𝑎 ′ , ¬ 𝑎 ′ ) pre-refines ( 𝑎 , 𝑏 ) . If V = 𝐿 , then we can take 𝑎 ′ = 𝑎 , in which case ( 𝑎 , ¬ 𝑎 ) pre-refines ( 𝑎 , 𝑏 ) and vice versa. Finally, for the claim about pseudocomplementationsterm in part 4, if ( 𝑎 , 𝑏 ) ⊲ ( 𝑐 , 𝑑 ) , then 𝑎 ∧ 𝑐 ≠ 0 , for otherwise 𝑐 ≤ ¬ 𝑎 , and ¬ 𝑎 ≤ 𝑏 by (i), so 𝑐 ≤ 𝑏 , contradicting ( 𝑎 , 𝑏 ) ⊲ ( 𝑐 , 𝑑 ) . Hence there is a nonzero 𝑒 ∈ V with 𝑒 ≤ 𝑎 ∧ 𝑐 . Then ( 𝑒 , ¬ 𝑒 ) ∈ 𝑃 , and since 𝑒 ≤ 𝑎 and 𝑒 ≤ 𝑐 , we have that ( 𝑒 , ¬ 𝑒 ) pre-refines ( 𝑎 , 𝑏 ) and ( 𝑐 , 𝑑 ) . Hence ⊲ is weakly compossible. □ As an illustration of part 4 of Theorem 4.24, consider the lattice with weak pseudocomplementationterm shown on the left of Figure 12. Setting V = Λ = { 2 , 3 } , we have 𝑃 = { ( 𝑎 , ¬ 𝑎 ) ∣ 𝑎 ∈ V , 𝑎 ≠ 0 } ∪ { ( 1 , 𝑏 ) ∣ 𝑏 ∈ Λ , 𝑏 ≠ 1 } = { ( 2 , 0 ) , ( 3 , 0 ) } ∪ { ( 1 , 2 ) , ( 1 , 3 ) } . Then the definition of ⊲ by ( 𝑎 , 𝑏 ) ⊲ ( 𝑐 , 𝑑 ) if 𝑐 ≰ 𝑏 yields the relational frame on the right of Figure 12. Figure 12. A lattice with weak pseudocomplementationterm (left) represented by a pseudosymmetric reflexive frame (right) (with reflexive loops assumed but not shown) as in Theorem 4.24.4.

Less economical choices of P than in Theorem 4.24 are possible, e.g., setting 𝑃 = { ( 𝑎 , 𝑏 ) ∣ 𝑎 , 𝑏 ∈ 𝐿 , ¬ 𝑎 ≤ 𝑏 } in parts 1 and 3 and 𝑃 = { ( 𝑎 , 𝑏 ) ∣ 𝑎 , 𝑏 ∈ 𝐿 , 𝑎 ≰ 𝑏 , ¬ 𝑎 ≤ 𝑏 } in parts 2 and 4, as in [21] (Thm. 3.19). Note that if we equip L with the weak pseudocomplementationterm defined by ¬ 0 = 1 and ¬ 𝑎 = 0 for 𝑎 ≠ 0 , then the latter choice of P reduces to { ( 𝑎 , 𝑏 ) ∣ 𝑎 , 𝑏 ∈ 𝐿 , 𝑎 ≰ 𝑏 } , which is used as the underlying set of the reflexive frame dual to a complete lattice in [77] (Thm. 2.11).

Theorem 4.24 yields five completeness theorems, as two come from part 4. Define a prelogic in the same way as an intro-elim logicterm in Definition 2.1 but dropping both part 6 ( 𝜑 ⊢ ¬ ¬ 𝜑 ) and part 7 ( 𝜑 ∧ ¬ 𝜑 ⊢ 𝜓 ).17 Let ⊢ pre be the weakest prelogic. Define a protologic in the same way as an intro-elim logicterm in Definition 2.1 but with part 6 replaced by 𝜓 ⊢ ¬ ( 𝜑 ∧ ¬ 𝜑 ) . Let ⊢ pro be the weakest protologic. Define a paraconsistent intro-elim logicterm in the same way as an intro-elim logicterm in Definition 2.1 but dropping part 7. Let ⊢ para be the weakest paraconsistent intro-elim logicterm, which can be equivalently defined using our Fitch-style proof system for ⊢ 𝐹 but without the ¬E rule. Finally, define a pseudocomplementary logic in the same way as an intro-elim logicterm in Definition 2.1 but with the added principle that if 𝜑 ∧ 𝜓 ⊢ ⊥ , then 𝜑 ⊢ ¬ 𝜓 . Let ⊢ psu be the weakest pseudocomplementary logic.

Let 𝐾 be the class of all relational frames, 𝑅 the class of reflexive frames, 𝑃 (resp. 𝑆 ) the class of pseudosymmetric (resp. strongly pseudosymmetric) frames, PR (resp. SR ) the class of pseudosymmetric (resp. strongly pseudosymmetric) reflexive frames, and WCR the class of weakly compossible reflexive frames. Then for any formulas 𝜑 , 𝜓 ∈ 𝐿 : 1. 𝜑 ⊢ pre 𝜓 if and only if 𝜑 ⊧ 𝐾 𝜓 ; 2. 𝜑 ⊢ pro 𝜓 if and only if 𝜑 ⊧ 𝑅 𝜓 ; 3. 𝜑 ⊢ para 𝜓 if and only if 𝜑 ⊧ 𝑃 𝜓 (resp. 𝜑 ⊧ 𝑆 𝜓 ); 4. 𝜑 ⊢ 𝐹 𝜓 if and only if 𝜑 ⊧ PR 𝜓 (resp. 𝜑 ⊧ SR 𝜓 ); 5. 𝜑 ⊢ psu 𝜓 if and only if 𝜑 ⊧ WCR 𝜓 .

Soundness follows from Propositions 4.5 and 4.14.

For completeness, we first prove parts 2, 4, and 5. The proof is structurally the same in each case. Given 𝜑 ⊬ 𝐹 𝜓 , where 𝜃 is the valuation on the Lindenbaum-Tarski algebra ( 𝐿 , ¬ ) of ⊢ 𝐹 for which 𝜃 ˜ ( 𝜑 ) ≰ 𝜃 ˜ ( 𝜓 ) , and f is the embedding of ( 𝐿 , ¬ ) into ( 𝐿 ( 𝑃 , ⊲ ) , ¬ ⊲ ) from Theorem 4.24.4, define a valuation V on 𝐿 ( 𝑃 , ⊲ ) by 𝑉 ( 𝑝 ) = 𝑓 ( 𝜃 ( 𝑝 ) ) , yielding a model 𝑀 = ( 𝑃 , ⊲ , 𝑉 ) . An easy induction shows that for any 𝜒 ∈ 𝐿 , ⟦ 𝜒 ⟧ 𝑀 = 𝑓 ( 𝜃 ˜ ( 𝜒 ) ) . Then from 𝜃 ˜ ( 𝜑 ) ≰ 𝜃 ˜ ( 𝜓 ) we have 𝑓 ( 𝜃 ˜ ( 𝜑 ) ) ⊆ 𝑓 ( 𝜃 ˜ ( 𝜓 ) ) , so ⟦ 𝜑 ⟧ 𝑀 ⊆ ⟦ 𝜓 ⟧ 𝑀 , so 𝜑 ⊭ SR 𝜓 .

For parts 1 and 3, the Lindenbaum-Tarski algebra of ⊢ pre (resp. ⊢ para ) is not bounded; but we can embed it into a bounded latticeterm by adjoining a new minimum 0 and maximum 1 to the lattice and setting ¬ 0 = 1 and ¬ 1 = 0 .18 Then the rest of the proof is the same as above, using Theorem 4.24.1 (resp. 4.24.3). □ Compare part 2 of Theorem 4.27 to Theorems 2 and 3 of [67], which axiomatize the logic of the class 𝑅 of reflexive frames in the { ¬ , ∧ } -fragment of 𝐿 .

One of the appealing aspects of this relational semanticsterm is how it allows us to apply reasoning that is very familiar from the intuitionistic setting to our non-distributive setting. For example, consider the following proof of the disjunction property for ⊢ 𝐹 that takes the disjoint union of two models and adds a new root as in the standard intuitionistic proof. Essentially the same proof applies to the other logics in Theorem 4.27.

For any 𝜑 , 𝜓 ∈ 𝐿 , if ⊤ ⊢ 𝐹 𝜑 ∨ 𝜓 , then ⊤ ⊢ 𝐹 𝜑 or ⊤ ⊢ 𝐹 𝜓 .

Suppose ⊤ ⊬ 𝐹 𝜑 and ⊤ ⊬ 𝐹 𝜓 , so by the completeness direction of Theorem 4.27.4, there are models 𝑀 1 = ( 𝑋 1 , ⊲ 1 , 𝑉 1 ) and 𝑀 2 = ( 𝑋 2 , ⊲ 2 , 𝑉 2 ) based on pseudosymmetric reflexive frames, 𝑥 1 ∈ 𝑋 1 , and 𝑥 2 ∈ 𝑋 2 such that 𝑀 1 , 𝑥 1 ⊮ 𝜑 and 𝑀 2 , 𝑥 2 ⊮ 𝜓 . Without loss of generality, assume 𝑋 1 ∩ 𝑋 2 = ⌀ . Define the disjoint union 𝑀 = ( 𝑋 , ⊲ , 𝑉 ) by 𝑋 = 𝑋 1 ∪ 𝑋 2 , ⊲ = ⊲ 1 ∪ ⊲ 2 , and 𝑉 ( 𝑝 ) = 𝑉 1 ( 𝑝 ) ∪ 𝑉 2 ( 𝑝 ) for 𝑝 ∈ Prop . Clearly ( 𝑋 , ⊲ ) is a pseudosymmetric reflexive frame, 𝑉 ( 𝑝 ) is a 𝑐 ⊲ -fixpoint, and 𝑀 , 𝑥 1 ⊮ 𝜑 and 𝑀 , 𝑥 2 ⊮ 𝜓 .

Fixing some 𝑟 ∉ 𝑋 , define 𝑀 ′ = ( 𝑋 ′ , ⊲ ′ , 𝑉 ′ ) such that 𝑋 ′ = 𝑋 ∪ { 𝑟 } , ⊲ ′ = ⊲ ∪ { ( 𝑥 , 𝑟 ) ∣ 𝑥 ∈ 𝑋 ′ } , and 𝑉 ′ ( 𝑝 ) = 𝑉 ( 𝑝 ) for 𝑝 ∈ Prop . Then ⊲ is clearly reflexive. For pseudosymmetry, for 𝑥 , 𝑦 ∈ 𝑋 , suppose 𝑦 ⊲ ′ 𝑥 . If 𝑥 ≠ 𝑟 , then 𝑦 ⊲ 𝑥 , so pseudosymmetry of ⊲ implies there is a 𝑧 ⊲ 𝑦 that pre-refines x with respect to ⊲. From 𝑧 ⊲ 𝑦 we have 𝑧 ⊲ ′ 𝑦 , and we claim that z pre-refines x with respect to ⊲ ′ . For suppose 𝑤 ⊲ ′ 𝑧 . Then 𝑤 ≠ 𝑟 , so 𝑤 ⊲ 𝑧 , which implies 𝑤 ⊲ 𝑥 since z pre-refines x with respect to ⊲, so 𝑤 ⊲ ′ 𝑥 . On the other hand, if 𝑥 = 𝑟 , then set 𝑧 = 𝑦 . Hence 𝑧 ⊲ 𝑦 , and clearly z pre-refines r, since 𝑣 ⊲ 𝑟 for all 𝑣 ∈ 𝑋 ′ . Thus, ⊲ ′ is pseudosymmetric. It is also easy to see that 𝑉 ′ ( 𝑝 ) is a 𝑐 ⊲ ′ -fixpoint, so 𝑀 ′ is a model.

Now we claim that for all 𝜒 ∈ 𝐿 and 𝑥 ∈ 𝑋 , 𝑀 , 𝑥 ⊩ 𝜒 iff 𝑀 ′ , 𝑥 ⊩ 𝜒 . The proof is by induction on 𝜒 . The base case for p is immediate from the definition of 𝑉 ′ ; the ∧ case is immediate from the inductive hypothesis; and the ¬ case and the implication from 𝑀 , 𝑥 ⊩ 𝜒 1 ∨ 𝜒 2 to 𝑀 ′ , 𝑥 ⊩ 𝜒 1 ∨ 𝜒 2 follow from the inductive hypothesis and the fact that 𝑟 ⊲ 𝑥 . Finally, suppose 𝑀 ′ , 𝑥 ⊩ 𝜒 1 ∨ 𝜒 2 and 𝑥 ′ ⊲ 𝑥 , so 𝑥 ′ ⊲ ′ 𝑥 . Hence there is some 𝑥 ″ ⊳ ′ 𝑥 ′ such that 𝑀 ′ , 𝑥 ″ ⊩ 𝜒 𝑖 for some 𝑖 ∈ { 1 , 2 } . If 𝑥 ″ ∈ 𝑋 , then 𝑥 ″ ⊳ 𝑥 ′ , and by the inductive hypothesis, 𝑀 , 𝑥 ″ ⊩ 𝜒 𝑖 . If 𝑥 ″ = 𝑟 , then since 𝑥 ′ pre-refines r, we have 𝑀 , 𝑥 ′ ⊩ 𝜒 𝑖 by Lemma 4.12. In either case, we have shown that for all 𝑥 ′ ⊲ 𝑥 there is a 𝑦 ⊳ 𝑥 ′ such that 𝑀 , 𝑦 ⊩ 𝜒 𝑖 for some 𝑖 ∈ { 1 , 2 } . Thus, 𝑀 , 𝑥 ⊩ 𝜒 1 ∨ 𝜒 2 .

By the previous paragraph, 𝑀 ′ , 𝑥 1 ⊮ 𝜑 and 𝑀 ′ , 𝑥 2 ⊮ 𝜓 . Then since 𝑥 1 and 𝑥 2 pre-refine r, 𝑀 ′ , 𝑟 ⊮ 𝜑 and 𝑀 ′ , 𝑟 ⊮ 𝜓 by Lemma 4.12. Then since r can see a state, namely itself, that cannot be seen by any state forcing 𝜑 or 𝜓 , we have 𝑀 ′ , 𝑟 ⊮ 𝜑 ∨ 𝜓 . Hence ⊤ ⊬ 𝐹 𝜑 ∨ 𝜓 by the soundness part of Theorem 4.27.4. □ We conclude this section by briefly following up on the idea from Remarks 3.3 and 4.8 of representing lattices with negations that do not necessarily satisfy ¬ 1 = 0 . We prove an analogue of Theorem 4.24.1 for such negations; analogues of the other parts of Theorem 4.24 can be similarly obtained.

Let L be a bounded latticeterm, Λ a meet-dense set of elements of L, and ¬ an antitone unary operation on L. Define 𝑃 = { ( 𝑎 , ¬ 𝑎 ) ∣ 𝑎 ∈ 𝐿 } ∪ { ( 1 , 𝑏 ) ∣ 𝑏 ∈ Λ } , ( 𝑎 , 𝑏 ) ⊲ ( 𝑐 , 𝑑 ) if 𝑐 ≰ 𝑏 , and 𝐹 = 𝑐 ⊲ ( { ( ¬ 1 , ¬ ¬ 1 ) } ) . Then there is a complete embedding of ( 𝐿 , ¬ ) into ( 𝐿 ( 𝑃 , ⊲ ) , ¬ ⊲ , 𝐹 ) with ¬ ⊲ , 𝐹 defined as in Remark 4.8, which is an isomorphism if L is complete.

The proof that the map f in Proposition 4.23 is a complete lattice embedding of L into 𝐿 ( 𝑃 , ⊲ ) , which is an isomorphism if L is complete, is exactly as in the proof of Theorem 4.24.1. It only remains to verify that 𝑓 ( ¬ 𝑎 ) = ¬ ⊲ , 𝐹 𝑓 ( 𝑎 ) .

Suppose ( 𝑥 , 𝑦 ) ∈ 𝑓 ( ¬ 𝑎 ) , so 𝑥 ≤ ¬ 𝑎 . Further suppose ( 𝑥 ′ , 𝑦 ′ ) ⊲ ( 𝑥 , 𝑦 ) and ( 𝑥 ′ , 𝑦 ′ ) ∈ 𝑓 ( 𝑎 ) , so 𝑥 ′ ≤ 𝑎 . Then ¬ 𝑎 ≤ ¬ 𝑥 ′ , which with 𝑥 ≤ ¬ 𝑎 implies 𝑥 ≤ ¬ 𝑥 ′ . Now if ( 𝑥 ′ , 𝑦 ′ ) ∈ { ( 𝑎 , ¬ 𝑎 ) ∣ 𝑎 ∈ 𝐿 } , then from 𝑥 ≤ ¬ 𝑥 ′ we have 𝑥 ≤ 𝑦 ′ , contradicting ( 𝑥 ′ , 𝑦 ′ ) ⊲ ( 𝑥 , 𝑦 ) . Thus, we have ( 𝑥 ′ , 𝑦 ′ ) ∈ { ( 1 , 𝑏 ) ∣ 𝑏 ∈ Λ } . Then from 𝑥 ≤ ¬ 𝑥 ′ , we have 𝑥 ≤ ¬ 1 , in which case we claim ( 𝑥 , 𝑦 ) ∈ 𝐹 . For if ( 𝑥 * , 𝑦 * ) ⊲ ( 𝑥 , 𝑦 ) , so 𝑥 ≰ 𝑦 * , then ¬ 1 ≰ 𝑦 * , so ( 𝑥 * , 𝑦 * ) ⊲ ( ¬ 1 , ¬ ¬ 1 ) , which shows ( 𝑥 , 𝑦 ) ∈ 𝑐 ⊲ ( { ( ¬ 1 , ¬ ¬ 1 ) } . Thus, for all ( 𝑥 ′ , 𝑦 ′ ) ⊲ ( 𝑥 , 𝑦 ) , if ( 𝑥 ′ , 𝑦 ′ ) ∈ 𝑓 ( 𝑎 ) , then ( 𝑥 , 𝑦 ) ∈ 𝐹 . It follows that ( 𝑥 , 𝑦 ) ∈ ¬ ⊲ , 𝐹 𝑓 ( 𝑎 ) . Conversely, let ( 𝑥 , 𝑦 ) ∈ 𝑃 \ 𝑓 ( ¬ 𝑎 ) , so 𝑥 ≰ ¬ 𝑎 . Then ( 𝑎 , ¬ 𝑎 ) ⊲ ( 𝑥 , 𝑦 ) . Moreover, since 𝑎 ≤ 1 , we have ¬ 1 ≤ ¬ 𝑎 , so ( 𝑎 , ¬ 𝑎 ) ⊲ ( ¬ 1 , ¬ ¬ 1 ) , which implies there is no ( 𝑧 , 𝑤 ) ⊳ ( 𝑎 , ¬ 𝑎 ) with ( 𝑧 , 𝑤 ) ∈ 𝐹 . It follows that ( 𝑥 , 𝑦 ) ∉ ¬ ⊲ , 𝐹 𝑓 ( 𝑎 ) . □ 4.3. Topological Representation of Lattices with Negations Topological representations of bounded latticesterm using reflexive frames endowed with a topology were developed in [49,84], building on [50,85]. In [21], we considered a variant of the approach of [84] using disjoint filter-ideal pairs but with a different topology in the spirit of the choice-free Stone duality of [86]. In this section, we briefly show how the filter-ideal representation can be adapted to bounded latticesterm equipped with protocomplementations and hence in particular weak pseudocomplementationsterm. For topological representations of ortholattices in particular, using symmetric and reflexive frames of proper filters equipped with a topology, see [87,88], and for associated categorical dualities, see [88,89,90].

Given a bounded latticeterm L and a protocomplementation ¬, define FI ( 𝐿 , ¬ ) = ( 𝑋 , ⊲ ) as follows: X is the set of all pairs ( 𝐹 , 𝐼 ) such that F is a filter in L, I is a ideal in L, 𝐹 ∩ 𝐼 = ⌀ , and { ¬ 𝑎 ∣ 𝑎 ∈ 𝐹 } ⊆ 𝐼 . One can interpret the states in X intuitively as in Remark 4.2: the state ( 𝐹 , 𝐼 ) accepts the propositions in F and rejects the propositions in I. Then define ( 𝐹 , 𝐼 ) ⊲ ( 𝐹 ′ , 𝐼 ′ ) iff 𝐼 ∩ 𝐹 ′ = ⌀ . Note that since ¬ is a protocomplementation, ⊲ is reflexive; but if we are interested in negations that are not semicomplementations, we can drop the condition that 𝐹 ∩ 𝐼 = ⌀ (see the end of Appendix B and compare the odd vs. even parts of Theorem 4.24). Given 𝑎 ∈ 𝐿 , let 𝑎 ^ = { ( 𝐹 , 𝐼 ) ∈ 𝑋 ∣ 𝑎 ∈ 𝐹 } . Finally, let 𝑆 ( 𝐿 ) be FI ( 𝐿 , ¬ ) endowed with the topology generated by { 𝑎 ^ ∣ 𝑎 ∈ 𝐿 } .

For any bounded latticeterm L and protocomplementation ¬ on L, the map 𝑎 ↦ 𝑎 ^ is 1. an embedding of ( 𝐿 , ¬ ) into ( 𝐿 ( FI ( 𝐿 , ¬ ) ) , ¬ ⊲ ) and 2. an isomorphism from L to the subalgebra of ( 𝐿 ( FI ( 𝐿 , ¬ ) ) , ¬ ⊲ ) consisting of 𝑐 ⊲ -fixpoints that are compact open in the space 𝑆 ( 𝐿 ) .

Given 𝑎 ∈ 𝐿 , let ↑ 𝑎 and ↓ 𝑎 be the filter and ideal, respectively, generated by a.

First observe that for any 𝑎 ∈ 𝐿 , 𝑎 ^ is a 𝑐 ⊲ -fixpoint. It suffices to show that if ( 𝐹 , 𝐼 ) ∉ 𝑎 ^ , then there is an ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 , 𝐼 ) such that for all ( 𝐹 ″ , 𝐼 ″ ) ⊳ ( 𝐹 ′ , 𝐹 ′ ) , we have ( 𝐹 ″ , 𝐼 ″ ) ∉ 𝑎 ^ . Suppose ( 𝐹 , 𝐼 ) ∉ 𝑎 ^ , so 𝑎 ∉ 𝐹 and hence 𝑎 ≠ 1 . Let 𝐹 ′ = ↑ 1 and 𝐼 ′ = ↓ 𝑎 . Then ( 𝐹 ′ , 𝐼 ′ ) ∈ 𝑋 . Now consider any ( 𝐹 ″ , 𝐼 ″ ) such that ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 ″ , 𝐼 ″ ) , so 𝐼 ′ ∩ 𝐹 ″ = ⌀ . Then since 𝑎 ∈ 𝐼 ′ , we have 𝑎 ∉ 𝐹 ″ , so ( 𝐹 ″ , 𝐼 ″ ) ∉ 𝑎 ^ , as desired.

Next, the map 𝑎 ↦ 𝑎 ^ is clearly injective: if 𝑎 ≰ 𝑏 , then ( ↑ 𝑎 , ↓ ¬ 𝑎 ) ∈ 𝑋 , ( ↑ 𝑎 , ↓ ¬ 𝑎 ) ∈ 𝑎 ^ , and ( ↑ 𝑎 , ↓ ¬ 𝑎 ) ∉ 𝑏 ^ . Obviously 1 ^ = 𝑋 and 0 ^ = ⌀ . The map also preserves ∧: 𝑎 ∧ 𝑏 ^ = { ( 𝐹 , 𝐼 ) ∈ 𝑋 ∣ 𝑎 ∧ 𝑏 ∈ 𝐹 } = { ( 𝐹 , 𝐼 ) ∈ 𝑋 ∣ 𝑎 , 𝑏 ∈ 𝐹 } = { ( 𝐹 , 𝐼 ) ∈ 𝑋 ∣ 𝑎 ∈ 𝐹 } ∩ { ( 𝐹 , 𝐼 ) ∈ 𝑋 ∣ 𝑏 ∈ 𝐹 } = 𝑎 ^ ∩ 𝑏 ^ = 𝑎 ^ ∧ 𝑏 ^ .

Next we show 𝑎 ∨ 𝑏 ^ ⊆ 𝑎 ^ ∨ 𝑏 ^ , as the converse inclusion follows from meet preservation. Recall from Proposition 4.3 that 𝑎 ^ ∨ 𝑏 ^ = 𝑐 ⊲ ( 𝑎 ^ ∪ 𝑏 ^ ) . Suppose ( 𝐹 , 𝐼 ) ∈ 𝑎 ∨ 𝑏 ^ , so 𝑎 ∨ 𝑏 ∈ 𝐹 . Consider any ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 , 𝐼 ) , so 𝐼 ′ ∩ 𝐹 = ⌀ and hence 𝑎 ∨ 𝑏 ∉ 𝐼 ′ . Then since 𝐼 ′ is an ideal, 𝑎 ∉ 𝐼 ′ or 𝑏 ∉ 𝐼 ′ . Without loss of generality, suppose 𝑎 ∉ 𝐼 ′ , so 𝑎 ≠ 0 . Then setting 𝐹 ″ = ↑ 𝑎 and 𝐼 ″ = ↓ ¬ 𝑎 , we have ( 𝐹 ″ , 𝐼 ″ ) ∈ 𝑋 and 𝐼 ′ ∩ 𝐹 ″ = ⌀ , so ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 ″ , 𝐼 ″ ) , and ( 𝐹 ″ , 𝐼 ″ ) ∈ 𝑎 ^ . Thus, we have shown that for any ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 , 𝐼 ) there is an ( 𝐹 ″ , 𝐼 ″ ) ⊳ ( 𝐹 ′ , 𝐼 ′ ) with ( 𝐹 ″ , 𝐼 ″ ) ∈ 𝑎 ^ ∪ 𝑏 ^ . Hence ( 𝐹 , 𝐼 ) ∈ 𝑎 ^ ∨ 𝑏 ^ . Finally, we show that ¬ 𝑎 ^ = ¬ ⊲ 𝑎 ^ . First suppose ( 𝐹 , 𝐼 ) ∈ ¬ 𝑎 ^ and ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 , 𝐼 ) . Since ( 𝐹 , 𝐼 ) ∈ ¬ 𝑎 ^ , we have ¬ 𝑎 ∈ 𝐹 , which with ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 , 𝐼 ) implies ¬ 𝑎 ∉ 𝐼 ′ , which with the definition of X implies 𝑎 ∉ 𝐹 ′ , so ( 𝐹 ′ , 𝐼 ′ ) ∉ 𝑎 ^ . Hence ( 𝐹 , 𝐼 ) ∈ ¬ ⊲ 𝑎 ^ . Conversely, if ( 𝐹 , 𝐼 ) ∉ ¬ 𝑎 ^ , so ¬ 𝑎 ∉ 𝐹 , then ( ↑ 𝑎 , ↓ ¬ 𝑎 ) ⊲ ( 𝐹 , 𝐼 ) and ( ↑ 𝑎 , ↓ ¬ 𝑎 ) ∈ 𝑎 ^ , so ( 𝐹 , 𝐼 ) ∉ ¬ ⊲ 𝑎 ^ .

For part 2, we first show that 𝑎 ^ is compact open. Since the 𝑏 ^ ’s form a basis, we need only show that if 𝑎 ^ ⊆ ⋃ { 𝑏 ^ 𝑘 ∣ 𝑘 ∈ 𝐾 } , then there is a finite subcover. Indeed, since ( ↑ 𝑎 , ↓ ¬ 𝑎 ) ∈ 𝑎 ^ , we have ( ↑ 𝑎 , ↓ ¬ 𝑎 ) ∈ 𝑏 𝑘 ^ for some 𝑘 ∈ 𝐾 , which implies 𝑎 ≤ 𝑏 𝑘 , so 𝑎 ^ ⊆ 𝑏 𝑘 ^ . Finally, we show that 𝑎 ↦ 𝑎 ^ is onto the set of compact open 𝑐 ⊲ -fixpoints. Suppose U is compact open, so 𝑈 = 𝑎 1 ^ ∪ ⋯ ∪ 𝑎 𝑛 ^ for some 𝑎 1 , … , 𝑎 𝑛 ∈ 𝐿 . Further suppose U is a 𝑐 ⊲ -fixpoint, so 𝑐 ⊲ ( 𝑈 ) = 𝑈 . Where 𝑑 = 𝑎 1 ∨ ⋯ ∨ 𝑎 𝑛 , an obvious induction using part 1 and the fact that 𝑐 ⊲ ( 𝑐 ⊲ ( 𝐴 ) ∪ 𝐵 ) = 𝑐 ⊲ ( 𝐴 ∪ 𝐵 ) for any 𝐴 , 𝐵 ⊆ 𝑋 yields 𝑑 ^ = 𝑐 ⊲ ( 𝑎 1 ^ ∪ ⋯ ∪ 𝑎 𝑛 ^ ) , so 𝑑 ^ = 𝑐 ⊲ ( 𝑈 ) = 𝑈 . □ In Appendix B, we prove an analogue of Theorem 4.30 for bounded latticesterm with implications.

The difference between the embedding part of Theorem 4.24 and the embedding part of Theorem 4.30 is that in the former we are embedding ( 𝐿 , ¬ ) into its MacNeille completion [91] (Thm. 2.2) whereas in the latter we are embedding ( 𝐿 , ¬ ) into its canonical extension [92,93].

Finally, consider the case where ¬ is a weak pseudocomplementationterm in line with our logic ⊢ 𝐹 .

If ¬ is a weak pseudocomplementationterm on L, then ⊲ in FI ( 𝐿 , ¬ ) is strongly pseudosymmetric.

Suppose ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 , 𝐼 ) . Where 𝐼 ″ is the ideal generated by { ¬ 𝑎 ∣ 𝑎 ∈ 𝐹 } , we claim that 𝐹 ∩ 𝐼 ″ = ⌀ . Otherwise there are 𝑎 1 , … , 𝑎 𝑛 , 𝑏 ∈ 𝐹 such that 𝑏 ≤ ¬ 𝑎 1 ∨ ⋯ ∨ ¬ 𝑎 𝑛 . Then where 𝑎 = 𝑎 1 ∧ ⋯ ∧ 𝑎 𝑛 , we have 𝑎 ∈ 𝐹 and 𝑏 ≤ ¬ 𝑎 , so ¬ 𝑎 ∈ 𝐹 , which implies 𝑎 ∧ ¬ 𝑎 ∈ 𝐹 and hence 0 ∈ 𝐹 , contradicting the fact that F is a proper filter. Hence ( 𝐹 , 𝐼 ″ ) ∈ 𝑋 . Now we claim that ( 𝐹 , 𝐼 ″ ) ⊲ ( 𝐹 ′ , 𝐼 ′ ) . For otherwise there is some 𝑏 ∈ 𝐹 ′ and 𝑎 1 , … , 𝑎 𝑛 ∈ 𝐹 such that 𝑏 ≤ ¬ 𝑎 1 ∨ ⋯ ∨ ¬ 𝑎 𝑛 , so where 𝑎 = 𝑎 1 ∧ ⋯ ∧ 𝑎 𝑛 , we have 𝑎 ∈ 𝐹 and 𝑏 ≤ ¬ 𝑎 , so ¬ 𝑎 ∈ 𝐹 ′ and hence ¬ ¬ 𝑎 ∈ 𝐼 ′ , which implies 𝑎 ∈ 𝐼 ′ , which contradicts ( 𝐹 ′ , 𝐼 ′ ) ⊲ ( 𝐹 , 𝐼 ) . Finally, since ( 𝐹 , 𝐼 ″ ) and ( 𝐹 , 𝐼 ) have the same first coordinate, ( 𝐹 , 𝐼 ″ ) pre-refines ( 𝐹 , 𝐼 ) and vice versa. □ Thus, by analogy with modal logic, we may say that our propositional logic ⊢ 𝐹 is canonical in the sense that it is validated by its canonical frame, whether one considers that to be the relational frame built from the Lindenbaum-Tarski algebra of the logic by Theorem 4.30 or by Theorem 4.24.4.

4.4. Modal Translations Relational semanticsterm for non-classical propositional logics immediately raise the possibility of translating such logics into modal logics on a classical base, as in Gödel’s translation of intuitionistic logicterm into the normal modal logic S4 [94,95], the modal logic of reflexive and transitive frames. In a similar spirit, Goldblatt [16] gave a full and faithful embedding of orthologicterm into the normal modal logic KTB, the modal logic of reflexive and symmetric frames. Below we will give a full and faithful embedding of our logic ⊢ 𝐹 into the extension of the minimal temporal logic 𝐾 𝑡 [96] (Def. 4.33) with the reflexivity axiom 𝐻 𝑞 → 𝑞 and the pseudosymmetry axiom 𝐻 𝑞 → 𝐻 𝑃 𝐻 𝑞 (or 𝐹 𝐻 𝑞 → 𝑃 𝐻 𝑞 ), based on viewing ⊲ in our frames as the temporal relation. We call this logic 𝐾 𝑡 TP . The pseudosymmetry axiom 𝑃 is Sahlqvist and hence canonical [96] (Thm. 4.42), so 𝐾 𝑡 TP is complete with respect to the class of pseudosymmetric reflexive frames. In fact, the canonical frame for 𝐾 𝑡 TP [96] (Def. 4.34) is strongly pseudosymmetric. For where Γ and Σ are maximally consistent sets and R is the canonical relation, we claim that if Γ 𝑅 Σ , then Δ 0 = { 𝜑 ∣ 𝐻 𝜑 ∈ Γ } ∪ { 𝐻 𝜓 ∣ 𝐻 𝜓 ∈ Σ } is consistent. If not, then for 𝐻 𝜑 1 , … , 𝐻 𝜑 𝑛 ∈ Γ and 𝐻 𝜓 1 , … , 𝐻 𝜓 𝑚 ∈ Σ , we have 𝜑 1 ∧ ⋯ ∧ 𝜑 𝑛 ⊢ ¬ ( 𝐻 𝜓 1 ∧ ⋯ ∧ 𝐻 𝜓 𝑚 ) ⊢ ¬ 𝐻 𝜒 where 𝜒 = 𝜓 1 ∧ ⋯ ∧ 𝜓 𝑚 , which implies 𝐻 𝜑 1 ∧ ⋯ ∧ 𝐻 𝜑 𝑛 ⊢ 𝐻 ¬ 𝐻 𝜒 , so 𝐻 ¬ 𝐻 𝜒 ∈ Γ . But 𝐻 𝜒 ∈ Σ , so we have 𝐻 𝑃 𝐻 𝜒 ∈ Σ by the 𝑃 axiom, which with Γ 𝑅 Σ implies 𝑃 𝐻 𝜒 ∈ Γ , contradicting 𝐻 ¬ 𝐻 𝜒 ∈ Γ . Extending Δ 0 to a maximally consistent set provides the desired witness for strong pseudosymmetry, as Δ 𝑅 Γ and Δ and Σ have the same temporal predecessors.

The translation t from our language 𝐿 to the temporal language is given by: 𝑡 ( 𝑝 ) = 𝐻 𝐹 𝑝 , 𝑡 ( ¬ 𝜑 ) = 𝐻 ¬ 𝑡 ( 𝜑 ) , 𝑡 ( 𝜑 ∧ 𝜓 ) = ( 𝑡 ( 𝜑 ) ∧ 𝑡 ( 𝜓 ) ) , and 𝑡 ( 𝜑 ∨ 𝜓 ) = 𝐻 𝐹 ( 𝑡 ( 𝜑 ) ∨ 𝑡 ( 𝜓 ) ) . Then the following is easy to prove using completeness for both logics (where 𝛼 ⊢ 𝐾 𝑡 TP 𝛽 means that 𝛼 → 𝛽 is a theorem of 𝐾 𝑡 TP ), transferring countermodels on one side to countermodels on the other side.

For all 𝜑 , 𝜓 ∈ 𝐿 , we have 𝜑 ⊢ 𝐹 𝜓 iff 𝑡 ( 𝜑 ) ⊢ 𝐾 𝑡 TP 𝑡 ( 𝜓 ) .

Similarly, the other logics in Theorem 4.27 embed via t into corresponding temporal logics; e.g., ⊢ pre embeds into 𝐾 𝑡 , so we obtain the decidability of the former from the known decidability of the latter.

A referee asked whether if we restrict attention to the { ∧ , ¬ } -fragment of 𝐿 , denoted 𝐿 ∧ , ¬ , then we obtain a full and faithful embedding of ⊢ 𝐹 into KTB by modifying Goldblatt’s [16] modal translation as follows: 𝑚 ( 𝑝 ) = 𝑝 ( instead of □ ⋄ 𝑝 ) , 𝑚 ( ¬ 𝜑 ) = □ ¬ 𝑚 ( 𝜑 ) , and 𝑚 ( 𝜑 ∧ 𝜓 ) = ( 𝑚 ( 𝜑 ) ∧ 𝑚 ( 𝜓 ) ) . Recall that KTB is the smallest normal modal logic containing the axioms □ 𝑝 → 𝑝 and 𝑝 → □ ⋄ 𝑝 , and let 𝛼 ⊢ KTB 𝛽 mean that 𝛼 → 𝛽 is a theorem of KTB . Under the m translation, 𝑝 ⊢ 𝐹 ¬ ¬ 𝑝 corresponds to 𝑝 ⊢ KTB □ ⋄ 𝑝 , while ¬ ¬ 𝑝 ⊬ 𝐹 𝑝 corresponds to □ ⋄ 𝑝 ⊬ KTB 𝑝 . More generally, we prove the following.

For all 𝜑 , 𝜓 ∈ 𝐿 ∧ , ¬ , we have 𝜑 ⊢ 𝐹 𝜓 iff 𝑚 ( 𝜑 ) ⊢ KTB 𝑚 ( 𝜓 ) .

Let an intro-elim logicterm for 𝐿 ∧ , ¬ be defined as in Definition 2.1 but without the conditions involving ∨. It is easy to check that the relation ⊢ defined on 𝐿 ∧ , ¬ by 𝜑 ⊢ 𝜓 iff 𝑚 ( 𝜑 ) ⊢ KTB 𝑚 ( 𝜓 ) is an intro-elim logicterm for 𝐿 ∧ , ¬ . Now where ⊢ 𝐹 ∧ , ¬ is the smallest intro-elim logicterm for 𝐿 ∧ , ¬ , we claim that 𝜑 ⊢ 𝐹 𝜓 implies 𝜑 ⊢ 𝐹 ∧ , ¬ 𝜓 for 𝜑 , 𝜓 ∈ 𝐿 ∧ , ¬ . For if 𝜑 ⊬ 𝐹 ∧ , ¬ 𝜓 , then the Lindenbaum-Tarski algebra of ⊢ 𝐹 ∧ , ¬ is a meet semilattice with 0 and 1 equipped with a weak pseudocomplementationterm, denoted ( 𝑀 , ¬ ) , that refutes the entailment from 𝜑 to 𝜓 . Now the proof of Theorem 4.24.4, replacing V with L, works for meet semilattices with 0 and 1 equipped with a weak pseudocomplementationterm, delivering a ( ∧ , ¬ ) -embedding of ( 𝑀 , ¬ ) into a complete lattice with weak pseudocomplementationterm, ( 𝐿 ( 𝑋 , ⊲ ) , ¬ ⊲ ) , that also refutes the entailment from 𝜑 to 𝜓 . Hence 𝜑 ⊬ 𝐹 𝜓 by Proposition 3.6. Thus, 𝜑 ⊢ 𝐹 𝜓 implies 𝜑 ⊢ 𝐹 ∧ , ¬ 𝜓 and therefore 𝑚 ( 𝜑 ) ⊢ KTB 𝑚 ( 𝜓 ) .

Conversely, if 𝜑 ⊬ 𝐹 𝜓 , then by Theorem 4.27.4, there is a model 𝑀 = ( 𝑋 , ⊲ , 𝑉 ) based on a pseudosymmetric reflexive frame and 𝑤 ∈ 𝑋 such that 𝑀 , 𝑤 ⊩ 𝜑 and 𝑀 , 𝑤 ⊮ 𝜓 . Let 𝑀 𝑠 = ( 𝑋 , ⊲ 𝑠 , 𝑉 ) be the model for the unimodal language where ⊲ 𝑠 is the symmetric closure of ⊲. Although 𝑉 ( 𝑝 ) may not be a 𝑐 ⊲ 𝑠 -fixpoint, this is not required for a modal model. Now we prove by induction on the structure of formulas 𝜑 ∈ 𝐿 ∧ , ¬ that for all 𝑥 ∈ 𝑋 , 𝑀 , 𝑥 ⊩ 𝜑 iff 𝑀 𝑠 , 𝑥 ⊧ 𝑚 ( 𝜑 ) , where ⊧ is the usual modal satisfaction relation with ⊳ as the accessibility relation for □. The base case and ∧ case are obvious. For the ¬ case, if 𝑀 , 𝑥 ⊮ ¬ 𝜑 , then there is a 𝑦 ⊲ 𝑥 with 𝑀 , 𝑦 ⊩ 𝜑 , which implies 𝑦 ⊲ 𝑠 𝑥 and 𝑀 𝑠 , 𝑦 ⊧ 𝑚 ( 𝜑 ) by the inductive hypothesis, so 𝑀 𝑠 , 𝑥 ⊭ □ ¬ 𝑚 ( 𝜑 ) . Conversely, suppose 𝑀 𝑠 , 𝑥 ⊭ □ ¬ 𝑚 ( 𝜑 ) , so there is some 𝑦 ⊲ 𝑠 𝑥 with 𝑀 𝑠 , 𝑦 ⊧ 𝑚 ( 𝜑 ) and hence 𝑀 , 𝑦 ⊩ 𝜑 by the inductive hypothesis. Given 𝑦 ⊲ 𝑠 𝑥 , we have either 𝑦 ⊲ 𝑥 or 𝑥 ⊲ 𝑦 . If 𝑦 ⊲ 𝑥 , then 𝑀 , 𝑥 ⊮ ¬ 𝜑 . If 𝑥 ⊲ 𝑦 , then by pseudosymmetry, there is a 𝑧 ⊲ 𝑥 that pre-refines y. Then from 𝑀 , 𝑦 ⊩ 𝜑 we obtain 𝑀 , 𝑧 ⊩ 𝜑 by Lemma 4.12, so again 𝑀 , 𝑥 ⊮ ¬ 𝜑 . Thus, we conclude 𝑀 𝑠 , 𝑤 ⊧ 𝑚 ( 𝜑 ) and 𝑀 𝑠 , 𝑤 ⊭ 𝑚 ( 𝜓 ) , so 𝑚 ( 𝜑 ) ⊬ KTB 𝑚 ( 𝜓 ) by the soundness of KTB with respect to reflexive and symmetric frames. □ Note that if we compose the m translation above with the g translation from orthologicterm to ⊢ 𝐹 in Section 2, then we obtain Goldblatt’s translation of orthologicterm into KTB .

5. Quantification In this section, we extend the logic ⊢ 𝐹 with rules for the universal and existential quantifiers. For simplicitly, we consider a first-order language LQ with no function symbols, no constants, and no identity symbol. Atomic formulas are of the form 𝑃 ( 𝑣 1 , … , 𝑣 𝑛 ) where P is an n-ary predicate and 𝑣 1 , … , 𝑣 𝑛 belong to a countably infinite set Var of variables. Thus, formulas are given by the grammar 𝜑 : : = 𝑃 ( 𝑣 1 , … , 𝑣 𝑛 ) ∣ ¬ 𝜑 ∣ ( 𝜑 ∧ 𝜑 ) ∣ ( 𝜑 ∨ 𝜑 ) ∣ ∀ 𝑣 𝜑 ∣ ∃ 𝑣 𝜑 where 𝑣 1 , … , 𝑣 𝑛 , 𝑣 ∈ Var . We assume familiarity with the notions of free variables and of one variable being substitutable for another in 𝜑 [97] (p. 113); 𝜑 𝑢 𝑣 is the result of substituting u for v in 𝜑 .

We define proofs for ⊢ FQ , fundamental first-order logic, as for ⊢ 𝐹 in Section 2 but with the following additional clauses, represented diagrammatically in Figure 13, where 1 ≤ 𝑖 ≤ 𝑛 : If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof, 𝜎 𝑖 is a formula 𝜑 , and v does not occur free in 𝜎 1 , then 〈 𝜎 1 , … , 𝜎 𝑛 , ∀ 𝑣 𝜑 〉 is a proof (∀I). If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof, 𝜎 𝑖 is a formula of the form ∀ 𝑣 𝜑 , and u is substitutable for v in 𝜑 , then 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜑 𝑢 𝑣 〉 is a proof (∀E). If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof, 𝜎 𝑖 is a formula of the form 𝜑 𝑢 𝑣 , and u is substitutable for v in 𝜑 , then 〈 𝜎 1 , … , 𝜎 𝑛 , ∃ 𝑣 𝜑 〉 is a proof (∃I). If 〈 𝜎 1 , … , 𝜎 𝑛 〉 is a proof, 𝜎 𝑖 is a formula of the form ∃ 𝑣 𝜑 , 𝜎 𝑛 is a proof beginning with 𝜑 and ending with 𝜓 , and v does not occur free in 𝜓 , then 〈 𝜎 1 , … , 𝜎 𝑛 , 𝜓 〉 is a proof (∃E).

As in the propositional case, by adding RAA we obtain first-order orthologicterm; by adding Reiteration19 we obtain intuitionistic first-order logic; and by adding both we obtain classical first-order logic. Moreover, the negative translation from orthologicterm to ⊢ 𝐹 in Section 2 also extends to a translation from first-order orthologicterm to ⊢ FQ by setting 𝑔 ( ∀ 𝑣 𝜑 ) = ∀ 𝑣 𝑔 ( 𝜑 ) and 𝑔 ( ∃ 𝑣 𝜑 ) = ¬ ∀ 𝑣 ¬ 𝑔 ( 𝜑 ) . Figure 13. Fitch-style rules for the logic with quantifiers.

By the kind of sequent calculus analysis mentioned at the end of Section 2, Aguilera and Bydžovský [34] have shown that in striking contrast to intuitionistic or classical first-order logic, fundamental first-order logic is decidable. Thus, just the addition of Reiterationterm takes us from decidability to undecidability.

(Aguilera and Bydžovský). It is decidable in double exponential time whether 𝜑 ⊢ FQ 𝜓 .

Turning to semantics, relational frames for LQ are triples ( 𝑋 , ⊲ , 𝐷 ) where ( 𝑋 , ⊲ ) is a relational frame and D is a nonempty set disjoint from X. A relational model ( 𝑋 , ⊲ , 𝐷 , 𝑉 ) adds a function V assigning to each n-ary predicate P and n-tuple of objects 𝑑 1 , … , 𝑑 𝑛 from D a 𝑐 ⊲ -fixpoint 𝑉 ( 𝑃 , 𝑑 1 , … , 𝑑 𝑛 ) ⊆ 𝑋 . Given 𝑣 ∈ Var and variable assignments 𝑔 , ℎ ∈ 𝐷 Var , let ℎ ∼ 𝑣 𝑔 mean that h and g differ at most at v. Then the forcing clauses are: 𝑀 , 𝑥 ⊩ 𝑔 𝑃 ( 𝑣 1 , … , 𝑣 𝑛 ) iff 𝑥 ∈ 𝑉 ( 𝑃 , 𝑔 ( 𝑣 1 ) , … , 𝑔 ( 𝑣 𝑛 ) ) ; clauses for ¬, ∧, and ∨ as before; 𝑀 , 𝑥 ⊩ 𝑔 ∀ 𝑣 𝜑 iff ∀ ℎ ∼ 𝑣 𝑔 , 𝑀 , 𝑥 ⊩ ℎ 𝜑 ; 𝑀 , 𝑥 ⊩ 𝑔 ∃ 𝑣 𝜑 iff ∀ 𝑥 ′ ⊲ 𝑥 ∃ 𝑥 ″ ⊳ 𝑥 ′ ∃ ℎ ∼ 𝑣 𝑔 : 𝑀 , 𝑥 ″ ⊩ ℎ 𝜑 .

Where ⟦ 𝜑 ⟧ 𝑔 𝑀 = { 𝑥 ∈ 𝑋 ∣ 𝑀 , 𝑥 ⊩ 𝑔 𝜑 } , an easy induction shows that ⟦ 𝜑 ⟧ 𝑔 𝑀 is a 𝑐 ⊲ -fixpoint, and ⟦ ∀ 𝑣 𝜑 ⟧ 𝑔 𝑀 = ⋀ { ⟦ 𝜑 ⟧ ℎ 𝑀 ∣ ℎ ∼ 𝑣 𝑔 } ⟦ ∃ 𝑣 𝜑 ⟧ 𝑔 𝑀 = ⋁ { ⟦ 𝜑 ⟧ ℎ 𝑀 ∣ ℎ ∼ 𝑣 𝑔 } . Given a class 𝐶 of relational frames for LQ , we define 𝜑 ⊧ 𝐶 𝜓 if for all ( 𝑋 , ⊲ , 𝐷 ) ∈ 𝐶 , all models 𝑀 = ( 𝑋 , ⊲ , 𝐷 , 𝑉 ) based on ( 𝑋 , ⊲ , 𝐷 ) , and all variable assignments 𝑔 ∈ 𝐷 Var , if 𝑀 , 𝑥 ⊩ 𝑔 𝜑 , then 𝑀 , 𝑥 ⊩ 𝑔 𝜓 .

Let PRQ be the class of pseudosymmetric reflexive frames for LQ . We can use Theorem 4.24.4 to prove completeness of ⊢ FQ with respect to PRQ . The Lindenbaum-Tarski algebra of ⊢ FQ is defined as usual.

In the Lindenbaum-Tarski algebra of ⊢ FQ , for all 𝜑 ∈ 𝐿 and 𝑣 ∈ Var : [ ∀ 𝑣 𝜑 ] = ⋀ { [ 𝜑 𝑢 𝑣 ] ∣ 𝑢 ∈ Var and substitutable for 𝑣 in 𝜑 } [ ∃ 𝑣 𝜑 ] = ⋁ { [ 𝜑 𝑢 𝑣 ] ∣ 𝑢 ∈ Var and substitutable for 𝑣 in 𝜑 } .

A standard exercise using the introduction and elimination rulesterm for the quantifiers. □ For all formulas 𝜑 , 𝜓 ∈ LQ , we have 𝜑 ⊢ FQ 𝜓 if and only if 𝜑 ⊧ PRQ 𝜓 .

Soundness is straightforward (cf. Proposition 3.6). For completeness, suppose that 𝜑 ⊬ FQ 𝜓 , so in the Lindenbaum-Tarski algebra ( 𝐿 , ¬ ) for ⊢ FQ , we have [ 𝜑 ] ≰ [ 𝜓 ] . By Theorem 4.24.4, there is a complete embedding f of ( 𝐿 , ¬ ) into ( 𝐿 ( 𝑋 , ⊲ ) , ¬ ⊲ ) for a pseudosymmetric reflexive frame ( 𝑋 , ⊲ ) . We turn ( 𝑋 , ⊲ ) into a model 𝑀 = ( 𝑋 , ⊲ , 𝐷 , 𝑉 ) for LQ by setting 𝐷 = Var and 𝑉 ( 𝑃 , 𝑣 1 , … , 𝑣 𝑛 ) = 𝑓 ( [ 𝑃 ( 𝑣 1 , … , 𝑣 𝑛 ) ] ) . Let the variable assignment g be the identity function on Var . Given Lemma 5.2 and the fact that f is a complete embedding, it is easy to show that for all formulas 𝜑 ∈ LQ , ⟦ 𝜑 ⟧ 𝑔 𝑀 = 𝑓 ( [ 𝜑 ] ) . Then from [ 𝜑 ] ≰ [ 𝜓 ] , we have 𝑓 ( [ 𝜑 ] ) ≰ 𝑓 ( [ 𝜓 ] ) , so ⟦ 𝜑 ⟧ 𝑔 𝑀 ⊆ ⟦ 𝜓 ⟧ 𝑔 𝑀 and hence 𝜑 ⊭ PRQ 𝜓 . □ Clearly the same strategy also works for quantified versions of other logics we have discussed.

6. Comments on Conditionals So far we have said nothing about “the” conditional. But there are many kinds of conditionals, especially when moving out of the classical or intuitionistic world and into the orthological world or beyond. Indeed, there are at least three paths we could pursue when adding a conditional to our language: add the traditional introduction and elimination rulesterm for → to ⊢ 𝐹 ; add rules meant to capture properties of the indicative conditional ‘if…then’ of natural language, which might differ from the traditional rules for →; or consider how the relational semanticsterm of Section 4 might be extended to treat conditionals. In this section, we consider these three paths in roughly reverse order. We will mention options without making definitive choices.

Semantically, where Φ ( 𝑦 , 𝐴 , 𝐵 ) is a condition on a state y and subsets 𝐴 , 𝐵 of a frame ( 𝑋 , ⊲ ) such that y is the only free state variable in Φ ( 𝑦 , 𝐴 , 𝐵 ) , the set 𝐴 → Φ 𝐵 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ⊲ 𝑥 ( 𝑦 ∈ 𝐴 ⇒ Φ ( 𝑦 , 𝐴 , 𝐵 ) ) } is a 𝑐 ⊲ -fixpoint and hence a candidate for a kind of conditional proposition. Examples of Φ ( 𝑦 , 𝐴 , 𝐵 ) include: 1. 𝑦 ∈ 𝐵 ; 2. ∃ 𝑧 ⊲ 𝑦 : 𝑧 ∈ 𝐵 ; 3. ∃ 𝑧 ⊳ 𝑦 : 𝑧 ∈ 𝐵 ; 4. ∃ 𝑧 ⊲ 𝑦 : 𝑧 ∈ 𝐴 ∩ 𝐵 ; 5. ∃ 𝑧 ⊳ 𝑦 : 𝑧 ∈ 𝐴 ∩ 𝐵 .

Let us consider these options from a technical point of view and a natural language point of view. On the technical side, option 1 has been considered a kind of “strict” implication (cf. [15] (p. 150), [98,99]) in the context of quantum logic. Options 3 and 5 both determine the Heyting implication in compossible reflexive frames representing Heyting algebras20 and are equivalent to options 2 and 4, respectively, in symmetric frames for ortholattices. Our representation theorem for negation, Theorem 4.24, smoothly generalizes to an implication of type 3 or 5, as we show for 5 in Theorem 6.3 below and for 3 in Appendix B.

From the point of view of ‘if…then’ in natural language, options 1-3 are all problematic, as they validate antecedent strengthening, i.e., if 𝐴 ⊆ 𝐶 , then 𝐶 → 𝐵 ⊆ 𝐴 → 𝐵 , which is apparently invalid for ‘if…then’ in natural language [100]. For example, ‘if it’s cloudy, then it might be raining’ ( 𝑐 → ⋄ 𝑟 ) clearly does not entail ‘if it’s cloudy and it’s not raining, then it might be raining’ ( ( 𝑐 ∧ ¬ 𝑟 ) → ⋄ 𝑟 ). The problem for option 4 (resp. 2) is that it renders 𝐴 → 𝐵 = ¬ ( 𝐴 ∩ ¬ ( 𝐴 ∩ 𝐵 ) ) (resp. 𝐴 → 𝐵 = ¬ ( 𝐴 ∩ ¬ 𝐵 ) ); but the right-to-left inclusion is rejected by semanticists for ‘if…then’ in natural language (see, e.g., [101]) and by intuitionists even for ‘if…then’ in mathematical proofs. Option 5 does not appear to enforce any problematic principles if we restrict attention to the operations ∧ , ∨ , → , as shown by Theorem 6.3 below. However, like all the other options, option 5 leads to ¬ 𝐴 ⊆ 𝐴 → 0 ; yet we can assign high probability to ’It’s not raining’ and yet almost no probability to ’If it is raining, then a tsunami is flattening Manhattan’, which shows that ¬ 𝑝 should not entail 𝑝 → ⊥ under an understanding of entailment with respect to which probability is monotonic (as it must be if we are to have anything like standard probability theory).

If we temporarily set aside the interaction of → and ¬, then the basic properties of the option 5 conditional, which we will write as 𝐴 ↠ ⊲ 𝐵 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ⊲ 𝑥 ( 𝑦 ∈ 𝐴 ⇒ ∃ 𝑧 ⊳ 𝑦 : 𝑧 ∈ 𝐴 ∩ 𝐵 ) } , appear quite plausible, as listed in the following definition. Note that in the terms of Remark 4.2, we have 𝑥 ∈ 𝐴 ↠ ⊲ 𝐵 iff no y open to x accepts A but rejects 𝐴 ∩ 𝐵 . Also note that our closure operator 𝑐 ⊲ is definable from ↠ ⊲ by 𝑐 ⊲ ( 𝐴 ) = 𝑋 ↠ ⊲ 𝐴 .

Given a bounded latticeterm L, a preconditional on L is a binary operation → on L satisfying the following for all 𝑎 , 𝑏 , 𝑐 ∈ 𝐿 : 1. 1 → 𝑎 ≤ 𝑎 ; 2. 𝑎 ∧ 𝑏 ≤ 𝑎 → 𝑏 ; 3. 𝑎 → 𝑏 ≤ 𝑎 → ( 𝑎 ∧ 𝑏 ) ; 4. if 𝑏 ≤ 𝑎 , then 𝑎 → ( 𝑏 → 𝑐 ) ≤ 𝑏 → 𝑐 ; 5. if 𝑏 ≤ 𝑐 , then 𝑎 → 𝑏 ≤ 𝑎 → 𝑐 .

Any bounded latticeterm can be equipped with a preconditional defined by: if 𝑎 ≤ 𝑏 , then 𝑎 → 𝑏 = 1 ; otherwise 𝑎 → 𝑏 = 𝑎 ∧ 𝑏 . Moreover, in any bounded latticeterm with a precomplementation ¬, the operation → defined by 𝑎 → 𝑏 = ¬ 𝑎 ∨ ( 𝑎 ∧ 𝑏 ) is a preconditional with ¬ 𝑎 = 𝑎 → 0 . In Appendix B, we give an axiomatization of preimplications that differs from that of preconditionals by replacing the ability to combine antecedent and consequent as in axiom 3 above with the ability to strengthen the antecedent. In a Heyting algebra, the relative pseudocomplementationterm → is both a preconditional and a preimplication.21 For any relational frame ( 𝑋 , ⊲ ) , the operation ↠ ⊲ is a preconditional on 𝐿 ( 𝑋 , ⊲ ) .

Part 1 of Definition 6.1 follows from the observation that 𝑐 ⊲ ( 𝐴 ) = 𝑋 ↠ ⊲ 𝐴 , so if A is a 𝑐 ⊲ -fixpoint, then 𝐴 = 𝑋 ↠ ⊲ 𝐴 . Parts 2, 3, and 5 are immediate from the definition of ↠ ⊲ . For part 4, suppose 𝐵 ⊆ 𝐴 , 𝑥 ∈ 𝐴 ↠ ⊲ ( 𝐵 ↠ ⊲ 𝐶 ) , 𝑥 ′ ⊲ 𝑥 , and 𝑥 ′ ∈ 𝐵 , so 𝑥 ′ ∈ 𝐴 . It follows that there is a 𝑦 ⊳ 𝑥 ′ such that 𝑦 ∈ 𝐵 ↠ ⊲ 𝐶 , which with 𝑥 ′ ∈ 𝐵 implies there is an 𝑥 ″ ⊳ 𝑥 ′ with 𝑥 ″ ∈ 𝐵 ∩ 𝐶 . This shows that 𝑥 ∈ 𝐵 ↠ ⊲ 𝐶 . □ We now show that any preconditional can be represented as ↠ ⊲ in a relational frame.

Let L be a bounded latticeterm and → preconditional on L. Then where 𝑃 = { ( 𝑥 , 𝑥 → 𝑦 ) ∣ 𝑥 , 𝑦 ∈ 𝐿 } and ( 𝑎 , 𝑏 ) ⊲ ( 𝑐 , 𝑑 ) if 𝑐 ≰ 𝑏 , there is a complete embedding of ( 𝐿 , → ) into ( 𝐿 ( 𝑃 , ⊲ ) , ↠ ⊲ ) , which is an isomorphism if L is complete.

First we claim that P is separating as in Definition 4.22. For part 1 of Definition 4.22, given 𝑎 ≰ 𝑏 , set ( 𝑐 , 𝑑 ) = ( 𝑎 , 𝑎 → 0 ) . For part 2 of Definition 4.22, suppose ( 𝑐 , 𝑑 ) ∈ 𝑃 and 𝑐 ≰ 𝑏 . Then set ( 𝑐 ′ , 𝑑 ′ ) = ( 1 , 1 → 𝑏 ) . From 𝑐 ≰ 𝑏 , we have 𝑐 ≰ 1 → 𝑏 by Definition 6.1.1, so ( 𝑐 ′ , 𝑑 ′ ) ⊲ ( 𝑐 , 𝑑 ) . Now consider any ( 𝑐 ″ , 𝑑 ″ ) ∈ 𝑃 with ( 𝑐 ′ , 𝑑 ′ ) ⊲ ( 𝑐 ″ , 𝑑 ″ ) . Then 𝑐 ″ ≰ 𝑑 ′ = 1 → 𝑏 and hence 𝑐 ″ ≰ 1 ∧ 𝑏 = 𝑏 by Definition 6.1.2, so 𝑐 ″ ≰ 𝑏 . Hence parts 1 and 2 of Definition 4.22 hold, so by Proposition 4.23, f is a complete embedding of L into 𝐿 ( 𝑃 , ⊲ ) , which is a lattice isomorphism if L is complete.

Next we claim that 𝑓 ( 𝑎 → 𝑏 ) = 𝑓 ( 𝑎 ) ↠ ⊲ 𝑓 ( 𝑏 ) . First suppose ( 𝑥 , 𝑥 → 𝑦 ) ∈ 𝑓 ( 𝑎 → 𝑏 ) , so 𝑥 ≤ 𝑎 → 𝑏 . Further suppose that ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ⊲ ( 𝑥 , 𝑥 → 𝑦 ) and ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ∈ 𝑓 ( 𝑎 ) , so 𝑥 ′ ≤ 𝑎 . From ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ⊲ ( 𝑥 , 𝑥 → 𝑦 ) , we have 𝑥 ≰ 𝑥 ′ → 𝑦 ′ . Now we claim that 𝑎 ∧ 𝑏 ≰ 𝑥 ′ → 𝑦 ′ . For if 𝑎 ∧ 𝑏 ≤ 𝑥 ′ → 𝑦 ′ , then by Definitions 6.1.3, 6.1.5, and 6.1.4 (given 𝑥 ′ ≤ 𝑎 ), we have 𝑥 ≤ 𝑎 → 𝑏 ≤ 𝑎 → ( 𝑎 ∧ 𝑏 ) ≤ 𝑎 → ( 𝑥 ′ → 𝑦 ′ ) ≤ 𝑥 ′ → 𝑦 ′ , contradicting 𝑥 ≰ 𝑥 ′ → 𝑦 ′ . Let ( 𝑥 ″ , 𝑥 ″ → 𝑦 ″ ) = ( 𝑎 ∧ 𝑏 , ( 𝑎 ∧ 𝑏 ) → 0 ) . Then ( 𝑥 ″ , 𝑥 ″ → 𝑦 ″ ) ∈ 𝑃 , ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ⊲ ( 𝑥 ″ , 𝑥 ″ → 𝑦 ″ ) , and ( 𝑥 ″ , 𝑥 ″ → 𝑦 ″ ) ∈ 𝑓 ( 𝑏 ) . Hence ( 𝑥 , 𝑥 → 𝑦 ) ∈ 𝑓 ( 𝑎 ) ↠ ⊲ 𝑓 ( 𝑏 ) .

Conversely, suppose ( 𝑥 , 𝑥 → 𝑦 ) ∈ 𝑃 \ 𝑓 ( 𝑎 → 𝑏 ) , so 𝑥 ≰ 𝑎 → 𝑏 . Let ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) = ( 𝑎 , 𝑎 → 𝑏 ) , so ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ⊲ ( 𝑥 , 𝑥 → 𝑦 ) . Now suppose ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ⊲ ( 𝑥 ″ , 𝑥 ″ → 𝑦 ″ ) , so 𝑥 ″ ≰ 𝑥 ′ → 𝑦 ′ = 𝑎 → 𝑏 . It follows by Definition 6.1.2 that 𝑥 ″ ≰ 𝑎 ∧ 𝑏 , so ( 𝑥 ″ , 𝑦 ″ ) ∉ 𝑓 ( 𝑎 ) ∩ 𝑓 ( 𝑏 ) . Hence ( 𝑥 , 𝑥 → 𝑦 ) ∉ 𝑓 ( 𝑎 ) ↠ ⊲ 𝑓 ( 𝑏 ) . □ A completeness theorem for a preconditional logic with a connective → obeying principles matching those of Definition 6.1 can easily be obtained from Theorem 6.3, just as we obtained completeness theorems for logics with ¬ from Theorem 4.24. It is also straightforward to add the quantifiers ∀ and ∃ (recall Theorem 5.3) to such a logic. The next step is to consider reasonable axioms to add to those of preconditionals and to characterize the corresponding classes of relational frames, though we will not do so here. (Some of the correspondence facts for ↠ ⊲ are the same as for → ⊲ in Appendix B, such as Lemmas B.1.1 and B.1.4.) There are multiple ways to deal with the problem that ¬ ⊲ 𝐴 ⊆ 𝐴 ↠ ⊲ 0 . One is to work with frames ( 𝑋 , ⊲ , ◂ ) with two relations ⊲ and ◂, interpreting negation as ¬ ◂ and the conditional as ↠ ⊲ , with an interaction condition between ⊲ and ◂ equivalent to the condition that ¬ ◂ maps 𝑐 ⊲ -fixpoints to 𝑐 ⊲ -fixpoints.22 Since presumably we want 𝐴 ↠ ⊲ 0 ⊆ ¬ ◂ 𝐴 , we require ◂ ⊆ ⊲ . Then we extend Theorem 6.3 as follows.

Let L be a bounded latticeterm, → preconditional on L, and ¬ an antitone operation on L such that for all 𝑎 ∈ 𝐿 , 𝑎 → 0 ≤ ¬ 𝑎 . Then where P and ⊲ are defined as in Theorem 6.3, and ◂ is defined by ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ◂ ( 𝑥 , 𝑥 → 𝑦 ) iff ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ⊲ ( 𝑥 , 𝑥 → 𝑦 ) and for all 𝑎 ∈ 𝐿 , 𝑥 ≤ ¬ 𝑎 implies 𝑥 ′ ≰ 𝑎 , there is a complete embedding of ( 𝐿 , → , ¬ ) into ( 𝐿 ( 𝑃 , ⊲ ) , ↠ ⊲ , ¬ ◂ ) , which is an isomorphism if L is complete.

We need only add to the proof of Theorem 6.3 that 𝑓 ( ¬ 𝑎 ) = ¬ ◂ 𝑓 ( 𝑎 ) . Suppose ( 𝑥 , 𝑥 → 𝑦 ) ∈ 𝑓 ( ¬ 𝑎 ) , so 𝑥 ≤ ¬ 𝑎 . Then for all ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ◂ ( 𝑥 , 𝑥 → 𝑦 ) , we have 𝑥 ′ ≰ 𝑎 and hence ( 𝑥 ′ , 𝑥 ′ → 𝑦 ′ ) ∉ 𝑓 ( 𝑎 ) , so ( 𝑥 , 𝑥 → 𝑦 ) ∈ ¬ ◂ 𝑓 ( 𝑎 ) . Conversely, suppose ( 𝑥 , 𝑥 → 𝑦 ) ∈ 𝑓 ( ¬ 𝑎 ) , so 𝑥 ≰ ¬ 𝑎 . Then 𝑥 ≰ 𝑎 → 0 , so ( 𝑎 , 𝑎 → 0 ) ⊲ ( 𝑥 , 𝑥 → 𝑦 ) . Moreover, for all 𝑏 ∈ 𝐿 , if 𝑥 ≤ ¬ 𝑏 , then given 𝑥 ≰ ¬ 𝑎 we have ¬ 𝑏 ≰ ¬ 𝑎 , so 𝑎 ≰ 𝑏 by the antitonicity of ¬. Thus, ( 𝑎 , 𝑎 → 0 ) ◂ ( 𝑥 , 𝑥 → 𝑦 ) , which shows ( 𝑥 , 𝑥 → 𝑦 ) ∉ ¬ ◂ 𝑓 ( 𝑎 ) . □ One can then impose additional conditions on ◂ to validate additional principles for ¬ ◂ . Moreover, an analogue of the topological representation of lattices with ¬ in Theorem 4.3 can be given for lattices with → and ¬ based on the idea of Theorem 6.4 (cf. Theorem B.7 in Appendix B). We leave for future work the systematic investigation of this approach to handling negation and conditionals.

A different semantic approach continues to represent ( 𝐿 , ¬ ) as ( 𝐿 ( 𝑋 , ⊲ ) , ¬ ⊲ ) but treats 𝐴 → ( · ) as a normal modal operation interpreted by an accessibility relation 𝑅 𝐴 on X, as in “set-selection function” semantics [103] (Section 2.7), such that 𝑥 𝑅 𝐴 𝑦 implies 𝑦 ∈ 𝐴 . Thus, 𝑥 𝑅 𝐴 𝑦 means that y is one of the relevant A-possibilities at which B must hold in order for 𝐴 → 𝐵 to hold at x. Representation theorems for bounded latticesterm equipped with both a negation ¬ and a normal modal □ are given in [21] (Section 4) using triples ( 𝑋 , ⊲ , 𝑅 ) where R is a binary relation on X satisfying an interaction condition with ⊲ that guarantees that the □ 𝑅 operation defined by □ 𝑅 𝐵 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑅 𝑦 ⇒ 𝑦 ∈ 𝐵 ) } sends 𝑐 ⊲ -fixpoints to 𝑐 ⊲ -fixpoints. The same approach can be applied to conditionals, only we now represent each normal modal operation 𝐴 → ( · ) by a binary relation 𝑅 𝐴 . In the filter-ideal space of ( 𝐿 , ¬ , → ) as in Section 4.3,23 one defines ( 𝐹 , 𝐼 ) 𝑅 𝑎 ^ ( 𝐹 ′ , 𝐼 ′ ) iff for all 𝑏 ∈ 𝐿 , 𝑎 → 𝑏 ∈ 𝐹 implies 𝑏 ∈ 𝐹 ′ , and then the modal operation 𝑎 → ( · ) is represented by □ 𝑅 𝑎 ^ [21] (Prop. 4.10). Assuming ( 𝐿 , ¬ , → ) satisfies 𝑎 → 𝑎 = 1 for all 𝑎 ∈ 𝐿 , then 𝑅 𝑎 ^ satisfies the constraint that 𝑅 𝑎 ^ -successors belong to 𝑎 ^ .

Treating 𝐴 → ( · ) as a normal modality matches a natural proof-theoretic approach to → based on Fitch-style proofs for modal logic [14]. Fitch distinguishes between ordinary subproofs, used for ¬I and ∨E, and box subproofs (his terms is ’strict column’), used for □I. Similarly, we distinguish between ordinary subproofs, used for ¬I and ∨E, and arrow subproofs, used for →I. This slightly complicates the rigorous inductive definition of proofs, but the basic idea is straightforward. Just as Fitch indicates his box subproofs with a □ symbol to the left of the vertical subproof line, we will indicate our arrow subproofs with a → symbol to the left of the vertical subproof line. A more important difference is that since Fitch [14] dealt only with a unary modal □, rather than our binary or indexed operators, his box subproofs have no assumptions, whereas our arrow subproofs will. Our →I rule says that if a proof contains an arrow subproof beginning with 𝜑 and ending with 𝜓 , then one can add 𝜑 → 𝜓 on the next line of the proof. The →E rules says that if a proof contains 𝜑 → 𝜓 and ends with an arrow subproof whose assumption is 𝜑 , then that arrow subproof can be extended with 𝜓 . The rules are shown diagramatically in Figure 14.

One might argue for adding to the →E rule that if a proof contains 𝜑 and 𝜑 → 𝜓 , then one can extend the proof with 𝜓 , per Modus Ponens, the traditional → elimination rule, as shown on the left of Figure 15. But McGee [104] has famously argued that one can assign higher probability to 𝑝 ∧ ( 𝑝 → ( 𝑞 → 𝑟 ) ) than to 𝑞 → 𝑟 , so the former does not entail the latter (cf. [105] (Section 4)). On the other hand, if instead of trying to capture a notion of entailment with respect to which probability is monotonic, we try to capture preservation of probability 1, then Modus Ponens seems unimpeachable: if the probability of 𝜑 is 1 and the probability of 𝜑 → 𝜓 is 1, then the probability of 𝜓 should be 1 as well. Now if we simply extend ⊢ 𝐹 with the traditional introduction and elimination rulesterm for → (left of Figure 14, left of Figure 15), but without →E from Figure 14 (in which case there is no real difference between arrow subproofs and ordinary subproofs), then we obtain a logic whose algebraic semantics is given by bounded latticesterm equipped with a weak pseudocomplementationterm and a binary operation → satisfying the properties that if 𝑎 ≤ 𝑏 , then 𝑎 → 𝑏 = 1 (for →I), and 𝑎 ∧ ( 𝑎 → 𝑏 ) ≤ 𝑏 (for MP). But it would seem that if Modus Ponens is acceptable, then so is the →E rule of Figure 14, so we should have both. Under the interpretation of 𝐴 → ( · ) as □ 𝑅 𝐴 above, which matches the rules in Figure 14, to validate Modus Ponens it suffices to assume weak centering [103]: if 𝑥 ∈ 𝐴 , then 𝑥 𝑅 𝐴 𝑥 .

One might also argue for strengthening →E so that if a proof contains 𝜑 → 𝜓 and an ordinary subproof beginning with 𝜑 , then one can extend that ordinary subproof with 𝜓 . But applying this to ordinary subproofs for ¬I yields the Modus Tollens inference, ¬ 𝜓 ∧ ( 𝜑 → 𝜓 ) ⊢ ¬ 𝜑 , which Veltman [106] (p. 3) has argued is invalid using examples in which 𝜓 contains conditionals and Yalcin [107] has argued is invalid using examples in which 𝜓 contains epistemic modalsterm; e.g., from ’The card might not be diamonds or hearts, but if it is red, then it must be diamonds or hearts’, it does not follow that ’The card is not red’ (we assume that ’might not’ entails ’not must’). The idea of applying →E to ordinary subproofs for ∨E yields ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 → 𝜒 ) ∧ ( 𝜓 → 𝜒 ) ⊢ 𝜒 , which arguably also admits counterexamples with epistemic modalsterm: from ’the card is red or black; if it’s red, it must be diamonds or hearts; and if it’s black, it must be clubs or spades’, it does not follow that ’it must be diamonds or hearts, or it must be clubs or spades’, since surely it might not be diamonds or hearts, and it might not be clubs or spades (cf. [108] for examples with deontic modals). The basic problem is that an ordinary subproof beginning with 𝜑 corresponds to considering a possibility where 𝜑 is merely true, whereas the natural language uses of ‘if’ above seem to involve a hypothetical update of a body of information to a new body of information in which the antecedent is “known.” In contrast to ordinary subproofs, one can interpret an arrow subproof beginning with 𝜑 as corresponding to a hypothetical update of that kind. See [8] for further discussion of the logic of conditionals and epistemic modalsterm. Figure 15. Modus Ponens (left) and another way to introduce negation (right).

In the context of the proof system with the rules of Figure 14, one might argue for another way of introducing negation: if a hypothetical update with 𝜑 leads to a contradiction, then conclude ¬ 𝜑 . Supposing we now have ⊥ as a primitive symbol in our language (interpreted as 0 in our lattices), this rule is shown on the right of Figure 15. Algebraically, this is just 𝑎 → 0 ≤ ¬ 𝑎 again. With respect to our pseudosymmetric reflexive frames equipped with accessibility relations 𝑅 𝐴 to define 𝐴 → ( · ) , the condition that 𝐴 → 0 ⊆ ¬ 𝐴 corresponds to the condition that if 𝑥 ⊳ 𝑦 ∈ 𝐴 , then 𝑅 𝐴 ( 𝑥 ) ≠ ⌀ .

None of the above is meant to suggest that the proof system for ∧, ∨, ¬, and → consisting of the I and E rules in Figure 2, Figure 14, and Figure 15 (and perhaps Modus Ponens, depending on one’s target notion of entailment) is the strongest reasonable system. But our goal has not been to formulate as strong a logic as ultimately reasonable but rather to identify a fundamental starting point based on introduction and elimination rulesterm.

7. Conclusions We have presented a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that is based purely on the introduction and elimination rulesterm for the logical constants. The corresponding algebraic semantics is based on bounded latticesterm with weak pseudocomplementationsterm. We have seen that such lattice expansions admit representation theorems using pseudosymmetric reflexive frames, furnishing an elegant relational semanticsterm for the logic. From this starting point, intuitionistic logicterm, orthologicterm, and classical logicterm can be obtained either proof-theoretically—by adding to our Fitch-style proof system Reiterationterm, Reductio ad Absurdumterm, or both—or semantically—by adding to our relational frames the properties of compossibility, symmetry, or both. We also sketched options for adding a conditional to our logic, though it remains to fill out this sketch in future work.

The relational semanticterm approach we have developed applies far beyond the fundamental logicterm, both to stronger and weaker logics that can be systematically investigated in the style of investigations of logics intermediate between intuitionistic and classical logicterm. Moreover, adding to our relational frames a second relation of accessibility yields semantics for modal versions of these logics [21]. In richer modal languages, we may be able to delineate those fragments of a language for which classical, intuitionistic, or orthological reasoning is safe from those that call for the caution of the fundamental logicterm.