# Classical Logic and Quantum Logic with Multiple and Common Lattice Models

Authors: Mladen Pavičić
Journal: Advances in Mathematical Physics
 (2016)

---

## Abstract

We consider a proper propositional quantum logic and show that it has multiple disjoint lattice models, only one of which is an orthomodular lattice (algebra) underlying Hilbert (quantum) space. We give an equivalent proof for the classical logic which turns out to have disjoint distributive and nondistributive ortholattices. In particular, we prove that both classical logic and quantum logic are sound and complete with respect to each of these lattices. We also show that there is one common nonorthomodular lattice that is a model of both quantum and classical logic. In technical terms, that enables us to run the same classical logic on both a digital (standard, two-subset, 0-1-bit) computer and a nondigital (say, a six-subset) computer (with appropriate chips and circuits). With quantum logic, the same six-element common lattice can serve us as a benchmark for an efficient evaluation of equations of bigger lattice models or theorems of the logic.


---

## Body

## 1. Introduction: Is Logic Empirical?

In his seminal paper “Is Logic Empirical?” [1], Putnam argues that logic we make use of to handle the statements and propositions of the theories we employ to describe the world around us is uniquely determined by it. “Logic is empirical. It makes … sense to speak of ‘physical logic.’ We live in a world with a nonclassical logic [of subspaces of the quantum Hilbert space H which form an orthomodular (non-distributive, non-Boolean) lattice]. Certain statements—just the ones we encounter in daily life—do obey classical logic, but this is so because the corresponding subspaces of H form a Boolean lattice” [1, Ch. V].We see that Putnam, in effect, reduces the logic to lattices, while they should only be their models. “[We] just read the logic off from the Hilbert spaceH” [1, Ch. III]. This technical approach has often been adopted in both classical and quantum logic. In classical logic, it has been known as two-valued interpretation for more than a century. In quantum logic, it has been introduced by Birkhoff and von Neumann in 1936 [2] and it is still embraced by many authors [3]. Subsequently, varieties of relational logic formulations, which closely follow lattice ordering relations, have been developed, for example, by Dishkant [4], Goldblatt [5], Chiara [6], Nishimura [7, 8], Mittelstaedt [9], Stachow [10], and Pták and Pulmannová [11]. More recently, Engesser and Gabbay [12] made related usage of nonmonotonic consequence relation, Rawling and Selesnick [13] of binary sequent, Herbut [14] of state-dependent implication of lattice of projectors in the Hilbert space, Tylec and Kuś [15] of partially ordered set (poset) map, and Bikchentaev et al. [16] of poset binary relation.Another version of Birkhoff-von-Neumann style of viewing propositions as projections in Hilbert space rather than closed subspaces and their lattices as in the original Birkhoff-von-Neumann paper has been introduced by Engesser et al. [17]. Recently, other versions of quantum logic have been developed, such as a dynamic quantum logic by Baltag and Smets [18, 19], exogenous quantum propositional logic by Mateus and Sernadas [20], a categorical quantum logic by Abramsky and Duncan [21, 22], and a projection orthoalgebraic approach to quantum logic by Harding [23].However, we are interested in nonrelational kinds of logic which combine propositions according to a set of true formulas/axioms and rules imposed on them. The propositions correspond to statements from a theory, say classical or quantum mechanics, and are not directly linked to particular measurement values. Such kinds of logic employ models which evaluate a particular combination of propositions and tell us whether it is true or not. Evaluation means mapping from a set of logic propositions to an algebra, for example, a lattice, through which a correspondence with measurement values emerges, but indirectly. Therefore we shall consider a classical and a quantum logic defined as a set of axioms whose Lindenbaum-Tarski algebras of equivalence classes of expressions from appropriate lattices correspond to the models of the logic. Let us call such a logic anaxiomatic logic. An axiomatic logic (L) is a language consisting of propositions and a set of conditions and rules imposed on them called axioms and rules of inference. We shall consider classical and quantum axiomatic logic.We show that an axiomatic logic is wider than its relational logic variety in the sense of having many possible models and not only distributive ortholattice (Boolean algebra) for the classical logic and not only orthomodular lattice for the quantum logic. We shall make use of the PM classical logical system—Whitehead and Russell’sPrincipia Mathematica axiomatization in Hilbert and Ackermann’s presentation [24] in the schemata form and of Kalmbach’s axiomatic quantum logic [25, 26] (slightly modified by Pavičić and Megill [27, 28]—original Kalmbach axioms A1, A11, and A15 are dropped because they were proven redundant in [29]), as typical examples of axiomatic logic.It is well-known that there are many interpretations of the classical logic, for example, two-valued, general Boolean algebra (distributive ortholattice) and set-valued ones [30, Ch. 8, 9]. These different interpretations are tantamount to different models of the classical logic and in this paper and several previous papers of ours we show that they are enabled by different definitions of the relation of equivalence for its different Lindenbaum-Tarski algebras. One model of the classical logic is a distributive numerically valued, mostly two-valued, lattice, while the others are nondistributive nonorthomodular lattices, one of them being the so-called O6 lattice, which can also be given set-valuations [30, Ch. 8, 9].As for quantum logic, one of its models is an orthomodular lattice, while others are nonorthomodular lattices, one of them being again O6—the common model of both kinds of logic.Within a logic we establish a unique deduction of all logic theorems from valid algebraic equations in a model and vice versa by proving the soundness and completeness of logic with respect to a chosen model. That means that we can infer the distributivity or orthomodularity in one model and disprove them in another by means of the same set of logical axioms and theorems. We can also consider O6 in which both the distributivity and orthomodularity fail; however, particular nondistributive and nonorthomodular conditions pass O6 only to map into the distributivity and orthomodularity through classical and quantum logic in other models of these kinds of logic.We see that logic is at least notuniquely empirical since it can simultaneously describe distinct realities.The paper is organised as follows. In Section2 we define classical and quantum logic. In Section 3 we introduce distributive (ortho)lattices and orthomodular lattices as well as two nondistributive (one is O6) and four nonorthomodular ones (one is again O6), all of which are our models for classical and quantum logic, respectively. In Section 4, we prove soundness and completeness of classical and quantum logic with respect to the models introduced in Section 3. In Section 5, we discuss the obtained results.


## 2. Kinds of Logic

In our axiomatic logic (L) the propositions are well-formed formulae (wffs), defined as follows.We denote elementary, or primitive, propositions byp0,p1,p2,…; we have the following primitive connectives: ¬ (negation) and ∨ (disjunction). pj is a wff for j=0,1,2,…; ¬A is a wff if A is a wff; A∨B is a wff if A and B are wffs.Operations are defined as follows.Definition 1 (conjunction).
One has(1)A∧B=def¬¬A∨¬B.Definition 2 (classical implication).
One has(2)A⟶cB=def¬A∨B.Definition 3 (Kalmbach’s implication).
One has(3)A⟶3B=def¬A∧B∨¬A∧¬B∨A∧¬A∨B.Definition 4 (quantum equivalence).
One has(4)A≡qB=defA∧B∨¬A∧¬B.Definition 5 (classical Boolean equivalence).
One has(5)A≡cB=defA⟶cB∧B⟶cA.Connectives bind from weakest to strongest in the order→, ≡, ∨, ∧, ¬.LetF∘ be the set of all propositions, that is, of all wffs. wffs containing ∨ and ¬ within logic L are used to build an algebra F=〈F∘,¬,∨〉. In L, a set of axioms and rules of inference are imposed on F. From a set of axioms by means of rules of inference, we get other expressions which we call theorems. Axioms themselves are also theorems. A special symbol ⊢ is used to denote the set of theorems. Hence A∈⊢ iff A is a theorem. The statement A∈⊢ is usually written as ⊢A. We read this as follows: “A is provable,” meaning that if A is a theorem, then there is a proof of it. We present the axiom systems of our propositional logic in the schemata form (so that we dispense with the rule of substitution).Definition 6.
ForΓ⊆F∘ one says that A is derivable from Γ and writes Γ⊢LA or just Γ⊢A if there is a finite sequence of formulae, the last of which is A, and each of which is either one of the axioms of L or is a member of Γ or is obtained from its precursors with the help of a rule of inference of the logic.


### 2.1. Classical Logic

In the classical logicCL, the sign ⊢CL will denote provability from the axioms and the rule of CL, but we shall omit the subscript when it is obvious from context as, for example, in the following axioms and the rule of inference that define CL.Axioms (6) A 1  ⊢ A ∨ A  ⟶ c  A A 2  ⊢ A  ⟶ c  A ∨ B A 3  ⊢ A ∨ B  ⟶ c  B ∨ A A 4  ⊢ A  ⟶ c  B ⟶ c C ∨ A  ⟶ c  C ∨ B .Rule of Inference (Modus Ponens) (7) R 1  ⊢ A  &  A  ⟶ c  B ⟹  ⊢ B .We assume that the only legitimate way of inferring theorems inCL is by means of these axioms and the Modus Ponens rule. We make no assumption about valuations of the primitive propositions from which wffs are built but instead are interested in wffs that are valid, that is, true in all possible valuations of the underlying models. Soundness and completeness will show that those theorems that can be inferred from the axioms and the rule are exactly those that are valid.


### 2.2. Quantum Logic

Quantum logic (QL) is defined as a language consisting of propositions and connectives (operations) as introduced above and the following axioms and a rule of inference. We will use ⊢QL to denote provability from the axioms and the rule of QL and omit the subscript when it is obvious from the context, for example, in the list of axioms and the rule of inference that follow.Axioms (8) A 2  ⊢ A  ≡ q  B  ⟶ c B  ≡ q  C  ⟶ c  A  ≡ q  C (9) A 3  ⊢ A  ≡ q  B  ⟶ c  ¬ A  ≡ q  ¬ B (10) A 4  ⊢ A  ≡ q  B  ⟶ c  A ∧ C  ≡ q  B ∧ C (11) A 5  ⊢ A ∧ B  ≡ q  B ∧ A (12) A 6  ⊢ A ∧ B ∧ C ≡ q  A ∧ B ∧ C (13) A 7  ⊢ A ∧ A ∨ B ≡ q  A (14) A 8  ⊢ ¬ A ∧ A  ≡ q ¬ A ∧ A ∧ B (15) A 9  ⊢ A  ≡ q  ¬ ¬ A (16) A 10  ⊢ ¬ A ∨ B ≡ q  ¬ A ∧ ¬ B (17) A 12  ⊢ A  ≡ q  B ≡ q  B  ≡ q  A (18) A 13  ⊢ A  ≡ q  B  ⟶ c A  ⟶ c  B (19) A 14  ⊢ A  ⟶ c  B ⟶ 3 A  ⟶ 3 A  ⟶ 3  B .Rule of Inference (Modus Ponens) (20) R 1  ⊢ A  &  ⊢ A  ⟶ 3  B ⟹  ⊢ B .Soundness and completeness will show that those theorems that can be inferred from the axioms and the rule of inference are exactly those that are valid.


## 2.1. Classical Logic

In the classical logicCL, the sign ⊢CL will denote provability from the axioms and the rule of CL, but we shall omit the subscript when it is obvious from context as, for example, in the following axioms and the rule of inference that define CL.Axioms (6) A 1  ⊢ A ∨ A  ⟶ c  A A 2  ⊢ A  ⟶ c  A ∨ B A 3  ⊢ A ∨ B  ⟶ c  B ∨ A A 4  ⊢ A  ⟶ c  B ⟶ c C ∨ A  ⟶ c  C ∨ B .Rule of Inference (Modus Ponens) (7) R 1  ⊢ A  &  A  ⟶ c  B ⟹  ⊢ B .We assume that the only legitimate way of inferring theorems inCL is by means of these axioms and the Modus Ponens rule. We make no assumption about valuations of the primitive propositions from which wffs are built but instead are interested in wffs that are valid, that is, true in all possible valuations of the underlying models. Soundness and completeness will show that those theorems that can be inferred from the axioms and the rule are exactly those that are valid.


## 2.2. Quantum Logic

Quantum logic (QL) is defined as a language consisting of propositions and connectives (operations) as introduced above and the following axioms and a rule of inference. We will use ⊢QL to denote provability from the axioms and the rule of QL and omit the subscript when it is obvious from the context, for example, in the list of axioms and the rule of inference that follow.Axioms (8) A 2  ⊢ A  ≡ q  B  ⟶ c B  ≡ q  C  ⟶ c  A  ≡ q  C (9) A 3  ⊢ A  ≡ q  B  ⟶ c  ¬ A  ≡ q  ¬ B (10) A 4  ⊢ A  ≡ q  B  ⟶ c  A ∧ C  ≡ q  B ∧ C (11) A 5  ⊢ A ∧ B  ≡ q  B ∧ A (12) A 6  ⊢ A ∧ B ∧ C ≡ q  A ∧ B ∧ C (13) A 7  ⊢ A ∧ A ∨ B ≡ q  A (14) A 8  ⊢ ¬ A ∧ A  ≡ q ¬ A ∧ A ∧ B (15) A 9  ⊢ A  ≡ q  ¬ ¬ A (16) A 10  ⊢ ¬ A ∨ B ≡ q  ¬ A ∧ ¬ B (17) A 12  ⊢ A  ≡ q  B ≡ q  B  ≡ q  A (18) A 13  ⊢ A  ≡ q  B  ⟶ c A  ⟶ c  B (19) A 14  ⊢ A  ⟶ c  B ⟶ 3 A  ⟶ 3 A  ⟶ 3  B .Rule of Inference (Modus Ponens) (20) R 1  ⊢ A  &  ⊢ A  ⟶ 3  B ⟹  ⊢ B .Soundness and completeness will show that those theorems that can be inferred from the axioms and the rule of inference are exactly those that are valid.


## 3. Lattices

For the presentation of the main result it would be pointless and definitely unnecessarily complicated to work with the full-fledged models, that is, Hilbert space, and the new non-Hilbert models that would be equally complex. It would be equally too complicated to present complete quantum or classical logic of the second order with all the quantifiers. Instead, we shall deal with lattices and the propositional logic we introduced in Section2. We start with a general lattice which contains all the other lattices we shall use later on. The lattice is called anortholattice and we shall first briefly present how one arrives at it starting with Hilbert space.A Hilbert lattice is a kind of orthomodular lattice which we define below. In any Hilbert lattice the operationmeet, a∩b, corresponds to set intersection, Ha⋂Hb, of subspaces Ha,Hb of the Hilbert space H; the ordering relation a≤b corresponds to Ha⊆Hb; the operationjoin, a∪b, corresponds to the smallest closed subspace of H containing Ha⋃Hb; and theorthocomplementa′ corresponds to Ha⊥, the set of vectors orthogonal to all vectors in Ha. Within the Hilbert space there is also an operation which has no parallel in the Hilbert lattice: the sum of two subspaces Ha+Hb which is defined as the set of sums of vectors from Ha and Hb. We also have Ha+Ha⊥=H. One can define all the lattice operations on the Hilbert space itself following the above definitions (Ha∩Hb=Ha⋂Hb, etc.). Thus we have Ha∪Hb=Ha+Hb¯=(Ha+Hb)⊥⊥=(Ha⊥⋂Hb⊥)⊥ [33, p. 175], where Hc¯ is the closure of Hc, and therefore Ha+Hb⊆Ha∪Hb. When H is finite dimensional or when the closed subspaces Ha and Hb are orthogonal to each other then Ha+Hb=Ha∪Hb [34, pp. 21–29], [25, pp. 66, 67], and [9, pp. 8–16].The projection associated withHa is given by Pa(x)=y for vector x from H that has a unique decomposition x=y+z for y from Ha and z from Ha⊥. The closed subspace belonging to P is HP={x∈H∣P(x)=x}. Let Pa∩Pb denote a projection on Ha∩Hb, Pa∪Pb a projection on Ha∪Hb, and Pa+Pb a projection on Ha+Hb if Ha⊥Hb, and let Pa≤Pb mean Ha⊆Hb. Then a∩b corresponds to Pa∩Pb=limn→∞(PaPb)n [9, p. 20], a′ to I-Pa, a∪b to Pa∪Pb=I-limn→∞[(I-Pa)(I-Pb)]n [9, p. 21], and a≤b to Pa≤Pb. a≤b also corresponds to either Pa=PaPb or Pa=PbPa or Pa-Pb=Pa∩b′. Two projectors commute iff their associated closed subspaces commute. This means that a∩(a′∪b)≤b corresponds to PaPb=PbPa. In the latter case we have Pa∩Pb=PaPb and Pa∪Pb=Pa+Pb-PaPb. a⊥b; that is, Pa⊥Pb is characterised by PaPb=0 [33, pp. 173–176], [25, pp. 66, 67], [9, pp. 18–21], and [35, pp. 47–50].Closed subspacesHa,Hb,… as well as the corresponding projectors Pa,Pb,… form an algebra called the Hilbert lattice which is an ortholattice. The conditions of the following definition can be easily read off from the properties of the aforementioned Hilbert subspaces or projectors.Definition 7.
An ortholattice, OL, is an algebra〈OL0,′,∪,∩〉 such that the following conditions are satisfied for any a,b,c∈OL0 [36]:(21)a∪b=b∪aa∪b∪c=a∪b∪ca′′=aa∪b∪b′=b∪b′a∪a∩b=aa∩b=a′∪b′′.In addition, since a∪a′=b∪b′ for any a,b∈OL0, we define the greatest and the least element of the lattice:(22)1=defa∪a′,0=defa∩a′,and the ordering relation (≤) on the lattice:(23)a≤b⟺defa∩b=a⟺a∪b=b.Definition 8 (Sasaki hook).
One has(24)a⟶1b=defa′∪a∩b.Definition 9 (quantum equivalence).
One has(25)a≡qb=defa∩b∪a′∩b′.Definition 10 (classical equivalence).
One has(26)a≡cb=defa′∪b∩b′∪a.Connectives bind from weakest to strongest in the order→, ≡, ∪, ∩, and ′.Definition 11 (Pavičić, [37]).
An orthomodular lattice (OML) is an OL in which the following condition (orthomodularity) holds:(27)a≡qb=1⟹a=b.Every Hilbert space (finite and infinite) and every phase space is orthomodular.Definition 12 (Pavičić, [38]).
(The proof of the opposite claim in [37, Theorem 3.2] is wrong.) A distributive ortholattice (DL) (also called a Boolean algebra) is an OL in which the following condition (distributivity) holds:(28)a≡cb=1⟹a=b.Every phase space is distributive and, of course, orthomodular since every distributive ortholattice is orthomodular.The opposite directions of metaimplications in (27) and (28) hold in any OL.Definition 13 (Pavičić and Megill, [27]).
An OL in which either of the following conditions (weak orthomodularity) holds(29)a⟶1b=1⟹b′⟶1a′=1(30)a≡b=1⟹a∪c≡b∪c=1is called a weakly orthomodular ortholattice, WOML.Definition 14 (Pavičić, this paper).
A WOML in which the following condition holds(31)a⟶1b≡b⟶1a=a≡bis called a WOML1.Definition 15 (Pavičić, this paper).
A WOML1 in which the following condition holds(32)a≡b′⟶1a′=a⟶1bis called a WOML2.Definition 16 (Pavičić, this paper).
A WOML in which neither (27), (32), nor (31) hold is called a WOML∗.Definition 17 (Pavičić and Megill, [27, 39]).
An OL in which the following condition (commensurability) holds(33)a∩b∪a∩b′∪a′∩b∪a′∩b′=1is called a weakly distributive ortholattice, WDL.Definition 18 (Pavičić and Megill, [27]).
A WOML in which the following condition (weak distributivity) holds(34)a∪b∩c≡ca∪b∩a∪c=1is called a weakly distributive ortholattice, WDL.Definitions17 and 18 are equivalent. We give both definitions here in order to, on the one hand, stress that a WDL is a lattice in which all variables are commensurable and, on the other, to show that in WDL the distributivity holds only in its weak form given by (34) which we will use later on.Definition 19 (Pavičić and Megill, [39]).
A WDL in which (28) does not hold is called a WDL∗.Any finite lattice can be represented by a Hasse diagram that consists of points (vertices) and lines (edges). Each point represents an element in a lattice, and positioning element a above element b and connecting them by a line means a≤b. For example, in Figure 1(a) we have 0≤x≤y≤1. We also see that in this lattice, for example, x does not have a relation with either x′ or y′.Figure 1
(a) O6; (b) O7 (Beran, Figure  7b [31]); (c) O8 (Rose–Wilkinson-1 [32]).
(a) (b) (c)The statement “orthomodularity (27) does not hold in WOML∗” reads ~[(∀a,b∈WOML∗)((a≡b=1)⇒(a=b))] which can be written as (∃a,b∈WOML∗)(a≡b=1&a≠b), where “~” is a metanegation and “&” a metaconjunction. An example of a WOML∗ is O6 from Figure 1(a) and we can easily check the statement on it. O6 is also an example of a WDL∗ and we can verify the statement “distributivity (28) does not hold in WDL∗” on it, as well. Similarly, “condition (32) does not hold in WOML∗” can be written as (∃a,b∈WOML∗)((a≡b′→1a′)≠(a→1b)).Definition 20 (Pavičić, this paper).
A WOML1 in which neither (27) nor (32) hold is called a WOML1∗.An example of aWOML1∗ is O7 from Figure 1(b).Definition 21 (Pavičić, this paper).
A WOML2 in which (27) does not hold is called a WOML2∗.An example of aWOML2∗ is O8 from Figure 1(c).Lemma 22.
OML is properly included in (i.e., it is stronger than) WOML2, WOML2 is properly included in WOML1, and WOML1 is properly included in WOML.Proof.
Equation (29) passes O6, O7, and O8 from Figure 1. Equation (31) passes O7 and O8 but fails in O6. Equation (32) passes O8 but fails in both O6 and O7. Equation (27) fails in O6, O7, and O8. To find the failures and passes we used our program lattice [40].Lemma 23.
OML is included in neitherWOML2∗, WOML1∗, nor WOML∗. WOML2∗ is included in neither WOML1∗ nor WOML∗. WOML1∗ is not included in WOML∗.Proof.
The proof follows straightforwardly from the proof of Lemma22 and the definitions of WOML∗, WOML1∗, WOML2∗, and OML.According to Definitions16, 20, 21, and 19, of WOML∗, WOML1∗, WOML2∗, and WDL∗, respectively, these lattices denote set-theoretical differences and that is going to play a crucial role in our proof of completeness in Section 4.2 in contrast to [27] where we considered only WOML without excluding the orthomodular equation. In Section 4.2 we shall come back to this decisive difference between the two approaches. Note that the set-differences are not equational varieties. For instance, WOML2∗ is a WOML2 in which the orthomodularity condition does not hold, but we cannot obtain WOML2∗ from WOML2 byadding new equational conditions to those defining WOML. Instead, WOML2∗ can be viewed as a set of lattices in all of which the orthomodularity condition is violated.Remarks on Implications. As we could see above, the implications do not play any decisive role in the definition of lattices, especially not in the definitions of OML and DL where they do not appear at all, and they also do not play a decisive role in the definition of logic. A few decades ago that was a major issue, though: “I would argue that a ‘logic’ without an implication … is radically incomplete, and indeed, hardly qualifies as a theory of deduction” (Jay Zeman) [41]. So, an extensive search was undertaken in the seventies and eighties to single proper implications from possible ones [42–44]. Apart from →1 and →3 it turns out [25] that one can also define a→0b=defa′∪b (classical), a→2b=defb′→1a′ (Dishkant), a→4b=defb′→3a′ (non-tollens), and a→5b=def(a∩b)∪(a′∩b)∪(a′∩b′) (relevance). In 1987 Pavičić [45] proved that an OL in which a→ib=1⇒a≤b, i=1,…,5, holds is an OML. In 1987 Pavičić [45] also proved that an OL in which a→0b=1⇒a≤b holds is a DL. Therefore 5 different but nevertheless equivalent relational kinds of logic could be obtained by linking lattice inequality to 5 implications. With our linking of a single equivalence to lattice equality this ambiguity is avoided and we obtain a uniquely defined axiomatic quantum logic. Note that we have a≡qb=(a→ib)∩(b→ia), i=1,…,5, in every OML but not in every OL.


## 4. Soundness and Completeness

We shall connect our types of logic with our lattices so as to show that the latter are the models of the former.Definition 24.
One callsM=〈L,h〉 a model if L is an algebra and h:F∘→L, called a valuation, is a morphism of formulae F∘ into L, preserving the operations ¬,∨ while turning them into ′,∪.Whenever the base setL of a model belongs to O6, WOML∗, WOML1∗, WOML2∗, OML, WDL∗, or DL we say (informally) that the model belongs to WOML∗, …, DL. In particular, if we say “for all models in O6, WOML∗, …, DL,” we mean for all base sets in O6, WOML∗, …, DL and for all valuations on each base set. The term “model” may refer either to a specific pair 〈L,h〉 or to all such possible pairs with the base set L, depending on the context.Definition 25.
One calls a formulaA∈F∘ valid in the model M and writes ⊨MA, if h(A)=1 for all valuations h on the model, that is, for all h associated with the base set L of the model. We call a formula A∈F∘ a consequence of Γ⊆F∘ in the model M and write Γ⊨MA if h(X)=1 for all X in Γ implies h(A)=1, for all valuations h.


### 4.1. Soundness

To prove soundness means to prove that all axioms as well as the rules of inference (and therefore all theorems) ofQL hold in its models. The models of QL are O6, WOML∗, WOML1∗, WOML2∗, and OML and of CL are O6, WDL∗, and DL. With the exception of O6 which is a special case of both WOML∗ and WDL∗, they do not properly include each other.For brevity, whenever we do not make it explicit, the notations⊨MA and Γ⊨MA will always be implicitly quantified over all models of the appropriate type, in this section for all proper lattice models M. Similarly, when we say “valid” without qualification, we will mean valid in all models of that type.The following theorems show that ifA is a theorem of QL, then A will be valid in O6 and any WOML∗, WOML1∗, WOML2∗, or OML model, and if A is a theorem of CL, then A will be valid in O6 and any WDL∗ or DL model. In [27, 28] we proved the soundness for WOML. Since that proof uses no additional conditions that hold in O6, WOML∗, …, OML the proof given there for WOML is a proof of soundness for O6, WOML∗, WOML1∗, WOML2∗, and OML, as well. Also, in [27, 28] we proved the soundness for WDL. Since that proof uses no additional conditions that hold in O6, WDL∗, and DL, the proof given there for WDL is a proof of soundness for O6, WDL∗, and DL, as well. Hence, we can prove the soundness of quantum and classical logic by means of WOML and WDL conditions without referring to condition (28), (27), (32), or (31), that is, to any condition in addition to those that hold in the WOML and WDL themselves.Theorem 26 (soundness ofCL).
One has(35)Γ⊢CLA⟹Γ⊨WDLA.Proof.
By Theorem  4.3 of [27] any WDL (in particular, O6, WDL∗, or DL) is a model for CL.Theorem 27 (soundness ofQL).
One has(36)Γ⊢QLA⟹Γ⊨WOMLA.Proof.
By Theorem  3.10 of [27] any WOML (in particular, O6, WOML∗, WOML1∗, WOML2∗, or OML) is a model for QL.Theorems26 and 27 express the fact that Γ⊢CLA and Γ⊢QLA in axiomatic logic types CL and QL correspond to a=h(A)=1 in their lattice models, from O6 and WOML till WDL. That means that we do not arrive at equations of the form a=b and that starting from Γ⊢A≡qB we cannot arrive at a=h(A)=b=h(B) but only at a≡qb=1. We can obtain a better understanding of this through the following properties of OML and DL.The equational theory of OML consists of equality conditions, (21) together with the orthomodular equality condition [28](37)a∪a′∩a∪b=a∪bwhich is equivalent to the condition given by (27). We now map each of these OML equations, which are of the form t=s, to the form t≡qs=1. This is possible in any WOML since(38)a∪a′∩a∪b≡qa∪b=1holds in every OL [28] and (21) mapped to the form t≡qs=1 also hold in any OL. Any equational proof in OML can then be simulated in WOML by replacing each axiom reference in the OML proof with its corresponding WOML mapping. Such mapped proof will make use of just a proper subset of the equations that hold in WOML.It follows that equations of the formt≡qs=1, where t and s are such that t=s holds in OML, cannot determine OML when added to an OL since all such forms pass O6 and an OL is an OML if and only if it does not include a subalgebra isomorphic to O6 [35].As forCL, the equational theory of distributive ortholattices can be simulated by a proper subset of the equational theory of WDLs since it consists of equality conditions equations (21) together with the distributivity equation(39)a∩b∪c=a∩b∪a∩cwhich is equivalent to condition (28). As with WOML above, we map these algebra conditions of the form t=s to the conditions of the form t≡cs=1, which hold in any WDL since the weak distributivity condition given by (34) holds in any WDL. Any equational proof in a DL can then be simulated in WDL by replacing each condition in a DL proof with its corresponding WDL mapping. Such a mapped proof will use only a proper subset of the equations that hold in WDL.Therefore, no set of equations of the formt≡cs=1, where t=s holds in DL, can determine a DL when added to an OL. Such equations hold in WDL and none of the WDL equations (21) and (39) is violated by O6 which itself violates the distributivity condition [28].Similar reasoning applies to O6,WOML∗, WOML1, WOML1∗, WOML2, and WOML2∗ which are all WOMLs and to O6 and WDL∗ which are WDLs. Soundness applies to them all through WOML and WDL and which particular model we shall use for QL and CL is determined by a particular Lindenbaum-Tarski algebra which we use for the completeness proof in the next subsection.


### 4.2. Completeness

Our main task in proving the soundness ofCL and QL in the previous section was to show that all axioms as well as the rules of inference (and therefore all theorems) from CL and QL hold in any WOML. The task of proving the completeness of CL and QL is the opposite one: we have to impose the structures of O6, WDL∗, and DL and O6, WOML∗, WOML1∗, WOML2∗, and OML on the sets F∘ of formulae of CL and QL, respectively. But here, as opposed to the soundness proof, we shall have as many completeness proofs as there are models. The completeness proofs for O6, WOML∗, WOML1∗, and WOML2∗ can be inferred neither from the proof for OML nor from the proofs for the other two. The same holds for O6, WDL∗, and DL.We start with a relation of congruence, that is, a relation of equivalence compatible with the operations inQL and CL. We make use of an equivalence relation to establish a correspondence between formulae of QL and CL and formulae of O6, WOML∗, WOML1∗, WOML2∗, and OML and O6, WDL∗, and DL, respectively. The resulting equivalence classes stand for elements of these lattices and enable the completeness proof of QL and CL for them.Our definition of congruence involves a special set of valuations on lattices O6, O7, and O8 (shown in Figure1) called O6, O7, and O8 and defined as follows.Definition 28.
LettingOi, i=6,7,8, represent the lattices from Figure 1, one defines Oi as the set of all mappings oi:F∘→Oi such that for A,B∈F∘, oi(¬A)=oiA′, and oi(A∨B)=oi(A)∪oi(B).The purpose ofOi, i=6,7,8, is to let us refine the equivalence class used for the completeness proof, so that the Lindenbaum-Tarski algebras are O6, WOML∗, WOML1∗, and WOML2∗.This is accomplished by conjoining the term(∀oi∈Oi)[(∀X∈Γ)(oi(X)=1)⇒oi(A)=oi(B)], i=6,7,8, to the equivalence relation definition, meaning that for equivalence we require also that (whenever the valuations oi of the wffs in Γ are all 1) the valuations of wffs A and B map to the same point in the lattice Oi. Thus, for example, in O6 wffs A∨B and A∨(¬A∧(A∨B)) become members of two separate equivalence classes, which by Theorem 39 amounts to nonorthomodularity of WOML. Without the conjoined term, these two wffs would belong to the same equivalence class. The point of doing this is to provide a completeness proof that is not in any way dependent on the orthomodular law and to show that completeness does not require that any of the underlying models be an OML. The equivalence classes so defined work for WOML1∗ and WOML2∗ as well since O7 will let (31) through but will not let through either the orthomodularity or (32), and O8 will let neither the orthomodularity, (32), nor (31) through.O6 will also let us refine the equivalence class used for the completeness proof of CL, so that the Lindenbaum-Tarski algebras are O6 and WDL∗.To obtain OML and DL Lindenbaum algebras we will make use of the standard equivalence classes without the conjoined terms.All these equivalence classes are relations of congruence.Theorem 29.
The relations ofequivalence≈Γ,QL,i, i=6,7,8, or simply ≈i, i=6,7,8, defined as(40)A≈iB=defΓ⊢A≡qB&∀oi∈Oi∀X∈ΓoiX=1⟹oiA=oiBi=6,7,8are relations of congruence, where Γ⊆F∘.Proof.
Let us first prove that≈ is an equivalence relation. A≈A follows from A1 [(8)] of system QL and the identity law of equality. If Γ⊢A≡B, we can detach the left-hand side of A12 to conclude Γ⊢B≡A, through the use of A13 and repeated uses of A14 and R1. From this and commutativity of equality, we conclude A≈B⇒B≈A. (For brevity we will mostly not mention further uses of A12, A13, A14, and R1 in what follows.) The proof of transitivity runs as follows (i=6,7,8).(41)A≈B&B≈C⟹Γ⊢A≡B&Γ⊢B≡C&∀o∈Oi∀X∈ΓoX=1⟹oA=oB&∀o∈Oi∀X∈ΓoX=1⟹oB=oC⟹Γ⊢A≡C&∀o∈Oi∀X∈ΓoX=1⟹oA=oB&oB=oC⟹Γ⊢A≡C&∀o∈Oi∀X∈ΓoX=1⟹oA=oC⟹A≈C.Γ⊢A≡C above follows from A2 and the metaconjunction in the second but last line reduces to o(A)=o(C) by transitivity of equality.
In order to be a relation of congruence, the relation of equivalence must be compatible with the operations¬ and ∨. These proofs run as follows (i=6,7,8).(42)A≈B⟹Γ⊢A≡B&∀o∈Oi∀X∈ΓoX=1⟹oA=oB⟹Γ⊢¬A≡¬B&∀o∈Oi∀X∈ΓoX=1⟹oA′=oB′⟹Γ⊢¬A≡¬B&∀o∈Oi∀X∈ΓoX=1⟹o¬A=o¬B⟹¬A≈¬B(43)A≈B⟹Γ⊢A≡B&∀o∈Oi∀X∈ΓoX=1⟹oA=oB⟹Γ⊢A∨C≡B∨C&∀o∈Oi∀X∈ΓoX=1⟹oA∪oC=oB∪oC⟹A∨C≈B∨C.In the second step of (42), we used A3. In the second step of (43), we used A4 and A10. For the quantified part of these expressions, we applied the definition of Oi, i=6,7,8.Theorem 30.
The relation ofequivalence≈Γ,QL,1, or simply ≈1, defined as(44)A≈1B=defΓ⊢A≡qBis a relation of congruence, where Γ⊆F∘.Proof.
The proof for the relation of equivalence given by (44) is the well-known standard one.Theorem 31.
The relation ofequivalence≈Γ,CL,6, or simply ≈6¯, defined as(45)A≈6¯B=defΓ⊢A≡cB&∀o6∈Oi∀X∈Γo6X=1⟹o6A=o6Bis a relation of congruence, where Γ⊆F∘.Proof.
It is as given  in [28].Theorem 32.
The relation ofequivalence≈Γ,CL,2, or simply ≈2, defined as(46)A≈2B=defΓ⊢A≡cBis a relation of congruence, where Γ⊆F∘.Proof.
The proof for the relation of equivalence given by (46) is the well-known standard one.Definition 33.
The equivalence class for wffA under the relation of equivalence ≈ given by (40), (44), (45), and (46) is defined as |A|={B∈F∘:A≈B}, and one denotes F∘/≈={|A|:A∈F∘}. The equivalence classes define the natural morphism f:F∘→F∘/≈, which gives f(A)=def|A|. One writes a=f(A), b=f(B), and so forth.Lemma 34.
The relationa=b on F∘/≈ is given by (47)A=B⟺A≈B.Lemma 35.
The Lindenbaum-Tarski algebrasAj=〈F∘/≈j,¬/≈j,∨/≈j〉, j=6,7,8,1,6¯,2, are WOML∗ (or O6), or WOML1∗, or WOML2∗, or OML, or WDL∗ (O6), or DL; that is, (21) and (30), or (31), or (32), or (27), or (33), or (28) hold for ¬/≈j and ∨/≈j, j=6,7,8,1,6¯,2, as ′ and ∪, respectively, where—for simplicity—one uses the same symbols (′ and ∪) as for Oi, since there are no ambiguous expressions in which the origin of the operations would not be clear from the context.Proof.
For theΓ⊢A≡B part of the A≈B definition, the proofs of the ortholattice conditions, (21), follow from A5, A6, A9, the dual of A8, the dual of A7, and DeMorgan’s laws, respectively. (The duals follow from DeMorgan’s laws, derived from A10, A9, and A3.) For (31) and (32) we use Lemma  3.5 from [27] according to which any t=1 condition that holds in OML also holds in any WOML. Program beran [32] shows that the expressions ((a→1b)≡(b→1a))≡(a≡b) and (a≡b′→1a′)≡(a→1b) reduce to 1 in an OML. By Lemma  3.5 this means that ((a→1b)≡(b→1a))≡(a≡b)=1 and (a≡b′→1a′)≡(a→1b)=1 in any WOML. Now the Γ⊢A≡B part from (40) forces these WOML conditions into (31) and (32). For the quantified part of the A≈B definition, lattice O6 is a (proper) WOML. For the OML, we carry out the proof with the relation of equivalence without the quantified part in (40). Then the Γ⊢A≡B part from (40) forces the condition (a∪(a′∩(a∪b)))≡(a∪b)=1 which holds in any ortholattice into the OM law given by (27).We stress here that the Lindenbaum-Tarski algebrasAj, j=6,7,8,6¯, from Lemma 35 will be uniquely assigned to QL and CL via Theorems 42 and 43 in the sense that we have to use the relations of congruence given by (40) and (45) and that we cannot use those given by (44) and (46). For Aj, j=1,2, we have to use the latter ones and we cannot use the former ones. This is in contrast to the completeness proof given in [27] where we did not consider the set-theoretical difference WOML∗ but only WOML. But since WOML contains OML (unlike WOML∗), in [27] (unlike in this paper) we can use both relations of congruence (40), (45) and (44), and (46) to prove the completeness. We see that the usage of set-theoretical differences in this paper establishes a correlation between lattice models and equivalence relations for a considered logic as shown in Figure 2.Figure 2
Lattice models of quantum and classical logic together with the corresponding equivalence relations which define their Lindenbaum-Tarski algebras.Lemma 36.
In the Lindenbaum-Tarski algebraA, if f(X)=1 for all X in Γ implies f(A)=1, then Γ⊢A.Proof.
We carry out the proof just forA6. Proofs for other cases run analogously. Let us assume that f(X)=1 for all X in Γ imply f(A)=1, that is, |A|=1=|A|∪A′=|A∨¬A|, where the first equality is from Definition 33, the second equality follows from (22) (the definition of 1 in an ortholattice), and the third from the fact that ≈ is a congruence. Thus A≈(A∨¬A), which by definition means Γ⊢A≡(A∨¬A)&(∀o∈O6)[(∀X∈Γ)(o(X)=1)⇒o(A)=o((A∨¬A))]. The same holds for O7 and O8. This implies, in particular (by dropping the second conjunct), Γ⊢A≡(A∨¬A). Now in any ortholattice, a≡(a∪a′)=a holds. By mapping the steps in the proof of this ortholattice identity to steps in a proof in the logic, we can prove ⊢(A≡(A∨¬A))≡A from QL axioms A2–A14. (A direct proof of ⊢(A≡(A∨¬A))≡A is also not difficult.) Detaching the left-hand side (using A12, A13, A14, and R1), we conclude Γ⊢A.Theorem 37.
The orthomodular law does not hold inAj, j=6,7,8, for models WOML* (O6), WOML1∗, and WOML2∗.Proof.
We assumeF∘ contains at least two elementary (primitive) propositions p0,p1,…. We pick a valuation o that maps two of them, A and B, to distinct nodes o(A) and o(B) of O6 that are neither 0 nor 1 such that o(A)≤o(B) [i.e., o(A) and o(B) are on the same side of hexagon O6 in Figure 1]. From the structure of O6, we obtain o(A)∪o(B)=o(B) and o(A)∪(oA′∩(o(A)∪o(B)))=o(A)∪(oA′∩o(B))=o(A)∪0=o(A). Therefore o(A)∪o(B)≠o(A)∪(oA′∩(o(A)∪o(B)), that is, o(A∨B)≠o(A∨(¬A∧(A∨B))). This falsifies (A∨B)≈(A∨(¬A∧(A∨B)) which is an alternative way of expressing the orthomodularity property [45, 46]. Therefore a∪b≠a∪(a′∩(a∪b)), providing a counterexample to the orthomodular law for F∘/≈. We can follow the steps given above by taking o(A)=x and o(B)=y in Figure 1(a). For O7 and O8 the proofs are analogous. For instance, the orthomodularity is violated in Figure 1(b) for o(A)=x and o(B)=y and in Figure 1(c) for o(A)=w and o(B)=y.Theorem 38.
The orthomodular law holds inA1 for an OML model.Proof.
It is well-known.Theorem 39.
The distributive law does not hold inA6¯, for WDL∗ (O6).Proof.
It is as given in [28].Schechter [30, Sec. 9.4] gives O6 a set-valued interpretation by assigning {-1,0,1,} to 1 in Figure 1(a), {-1,0} to y, {0,1} to x′, {-1} to x, {1} to y′, and ⌀ to 0 and calls it the hexagon interpretation. “The hexagon interpretation is not distributive. That fact came as a surprise to some logicians, since the two-valued logic itself is distributive” [30, Sec. 9.5]. Schechter also gives crystal (6 subsets) and Church’s diamond (4 subsets) set-valued interpretations of CL in his Sections  9.7.–13. and 9.14.–17.Theorem 40.
The distributive law holds inA2 for a DL model (Boolean algebra).Proof.
It is well-known.Lemma 41.
M A j = 〈 A j , f 〉, j=6,7,8,1,6¯,2, is a proper WOML∗ (O6), WOML1∗, WOML2∗, OML, WDL∗ (O6), or DL model.Proof.
It follows from Lemma35.Now we are able to prove the completeness ofQL and CL; that is, if a formula A is a consequence of a set of wffs Γ in all O6, WOML∗, WOML1∗, WOML2∗, and OML models and in all O6, WDL∗, and DL models then Γ⊢QLA and Γ⊢CLA, respectively. In particular, when Γ=⌀, all valid formulae are provable in QL.Theorem 42 (completeness of quantum logic).
One has(48)Γ⊨MAjA⟹Γ⊢QLA,j=6,7,8,1.Proof.
Γ  ⊨ M  A means that, in all WOML∗ (O6), WOML1∗, WOML2∗, and OML models M, if f(X)=1 for all X in Γ, then f(A)=1 holds. In particular, it holds for MA=〈A,f〉, which is a WOML∗ (O6), WOML1∗, WOML2∗, or OML model by Lemma 41. Therefore, in the Lindenbaum-Tarski algebra A, if f(X)=1 for all X in Γ, then f(A)=1 holds. By Lemma 36, it follows that Γ⊢A.Theorem 43 (completeness of classical logic).
One has(49)Γ⊨MAjA⟹Γ⊢CLA,j=6¯,2.Proof.
It is as  given in [28].


## 4.1. Soundness

To prove soundness means to prove that all axioms as well as the rules of inference (and therefore all theorems) ofQL hold in its models. The models of QL are O6, WOML∗, WOML1∗, WOML2∗, and OML and of CL are O6, WDL∗, and DL. With the exception of O6 which is a special case of both WOML∗ and WDL∗, they do not properly include each other.For brevity, whenever we do not make it explicit, the notations⊨MA and Γ⊨MA will always be implicitly quantified over all models of the appropriate type, in this section for all proper lattice models M. Similarly, when we say “valid” without qualification, we will mean valid in all models of that type.The following theorems show that ifA is a theorem of QL, then A will be valid in O6 and any WOML∗, WOML1∗, WOML2∗, or OML model, and if A is a theorem of CL, then A will be valid in O6 and any WDL∗ or DL model. In [27, 28] we proved the soundness for WOML. Since that proof uses no additional conditions that hold in O6, WOML∗, …, OML the proof given there for WOML is a proof of soundness for O6, WOML∗, WOML1∗, WOML2∗, and OML, as well. Also, in [27, 28] we proved the soundness for WDL. Since that proof uses no additional conditions that hold in O6, WDL∗, and DL, the proof given there for WDL is a proof of soundness for O6, WDL∗, and DL, as well. Hence, we can prove the soundness of quantum and classical logic by means of WOML and WDL conditions without referring to condition (28), (27), (32), or (31), that is, to any condition in addition to those that hold in the WOML and WDL themselves.Theorem 26 (soundness ofCL).
One has(35)Γ⊢CLA⟹Γ⊨WDLA.Proof.
By Theorem  4.3 of [27] any WDL (in particular, O6, WDL∗, or DL) is a model for CL.Theorem 27 (soundness ofQL).
One has(36)Γ⊢QLA⟹Γ⊨WOMLA.Proof.
By Theorem  3.10 of [27] any WOML (in particular, O6, WOML∗, WOML1∗, WOML2∗, or OML) is a model for QL.Theorems26 and 27 express the fact that Γ⊢CLA and Γ⊢QLA in axiomatic logic types CL and QL correspond to a=h(A)=1 in their lattice models, from O6 and WOML till WDL. That means that we do not arrive at equations of the form a=b and that starting from Γ⊢A≡qB we cannot arrive at a=h(A)=b=h(B) but only at a≡qb=1. We can obtain a better understanding of this through the following properties of OML and DL.The equational theory of OML consists of equality conditions, (21) together with the orthomodular equality condition [28](37)a∪a′∩a∪b=a∪bwhich is equivalent to the condition given by (27). We now map each of these OML equations, which are of the form t=s, to the form t≡qs=1. This is possible in any WOML since(38)a∪a′∩a∪b≡qa∪b=1holds in every OL [28] and (21) mapped to the form t≡qs=1 also hold in any OL. Any equational proof in OML can then be simulated in WOML by replacing each axiom reference in the OML proof with its corresponding WOML mapping. Such mapped proof will make use of just a proper subset of the equations that hold in WOML.It follows that equations of the formt≡qs=1, where t and s are such that t=s holds in OML, cannot determine OML when added to an OL since all such forms pass O6 and an OL is an OML if and only if it does not include a subalgebra isomorphic to O6 [35].As forCL, the equational theory of distributive ortholattices can be simulated by a proper subset of the equational theory of WDLs since it consists of equality conditions equations (21) together with the distributivity equation(39)a∩b∪c=a∩b∪a∩cwhich is equivalent to condition (28). As with WOML above, we map these algebra conditions of the form t=s to the conditions of the form t≡cs=1, which hold in any WDL since the weak distributivity condition given by (34) holds in any WDL. Any equational proof in a DL can then be simulated in WDL by replacing each condition in a DL proof with its corresponding WDL mapping. Such a mapped proof will use only a proper subset of the equations that hold in WDL.Therefore, no set of equations of the formt≡cs=1, where t=s holds in DL, can determine a DL when added to an OL. Such equations hold in WDL and none of the WDL equations (21) and (39) is violated by O6 which itself violates the distributivity condition [28].Similar reasoning applies to O6,WOML∗, WOML1, WOML1∗, WOML2, and WOML2∗ which are all WOMLs and to O6 and WDL∗ which are WDLs. Soundness applies to them all through WOML and WDL and which particular model we shall use for QL and CL is determined by a particular Lindenbaum-Tarski algebra which we use for the completeness proof in the next subsection.


## 4.2. Completeness

Our main task in proving the soundness ofCL and QL in the previous section was to show that all axioms as well as the rules of inference (and therefore all theorems) from CL and QL hold in any WOML. The task of proving the completeness of CL and QL is the opposite one: we have to impose the structures of O6, WDL∗, and DL and O6, WOML∗, WOML1∗, WOML2∗, and OML on the sets F∘ of formulae of CL and QL, respectively. But here, as opposed to the soundness proof, we shall have as many completeness proofs as there are models. The completeness proofs for O6, WOML∗, WOML1∗, and WOML2∗ can be inferred neither from the proof for OML nor from the proofs for the other two. The same holds for O6, WDL∗, and DL.We start with a relation of congruence, that is, a relation of equivalence compatible with the operations inQL and CL. We make use of an equivalence relation to establish a correspondence between formulae of QL and CL and formulae of O6, WOML∗, WOML1∗, WOML2∗, and OML and O6, WDL∗, and DL, respectively. The resulting equivalence classes stand for elements of these lattices and enable the completeness proof of QL and CL for them.Our definition of congruence involves a special set of valuations on lattices O6, O7, and O8 (shown in Figure1) called O6, O7, and O8 and defined as follows.Definition 28.
LettingOi, i=6,7,8, represent the lattices from Figure 1, one defines Oi as the set of all mappings oi:F∘→Oi such that for A,B∈F∘, oi(¬A)=oiA′, and oi(A∨B)=oi(A)∪oi(B).The purpose ofOi, i=6,7,8, is to let us refine the equivalence class used for the completeness proof, so that the Lindenbaum-Tarski algebras are O6, WOML∗, WOML1∗, and WOML2∗.This is accomplished by conjoining the term(∀oi∈Oi)[(∀X∈Γ)(oi(X)=1)⇒oi(A)=oi(B)], i=6,7,8, to the equivalence relation definition, meaning that for equivalence we require also that (whenever the valuations oi of the wffs in Γ are all 1) the valuations of wffs A and B map to the same point in the lattice Oi. Thus, for example, in O6 wffs A∨B and A∨(¬A∧(A∨B)) become members of two separate equivalence classes, which by Theorem 39 amounts to nonorthomodularity of WOML. Without the conjoined term, these two wffs would belong to the same equivalence class. The point of doing this is to provide a completeness proof that is not in any way dependent on the orthomodular law and to show that completeness does not require that any of the underlying models be an OML. The equivalence classes so defined work for WOML1∗ and WOML2∗ as well since O7 will let (31) through but will not let through either the orthomodularity or (32), and O8 will let neither the orthomodularity, (32), nor (31) through.O6 will also let us refine the equivalence class used for the completeness proof of CL, so that the Lindenbaum-Tarski algebras are O6 and WDL∗.To obtain OML and DL Lindenbaum algebras we will make use of the standard equivalence classes without the conjoined terms.All these equivalence classes are relations of congruence.Theorem 29.
The relations ofequivalence≈Γ,QL,i, i=6,7,8, or simply ≈i, i=6,7,8, defined as(40)A≈iB=defΓ⊢A≡qB&∀oi∈Oi∀X∈ΓoiX=1⟹oiA=oiBi=6,7,8are relations of congruence, where Γ⊆F∘.Proof.
Let us first prove that≈ is an equivalence relation. A≈A follows from A1 [(8)] of system QL and the identity law of equality. If Γ⊢A≡B, we can detach the left-hand side of A12 to conclude Γ⊢B≡A, through the use of A13 and repeated uses of A14 and R1. From this and commutativity of equality, we conclude A≈B⇒B≈A. (For brevity we will mostly not mention further uses of A12, A13, A14, and R1 in what follows.) The proof of transitivity runs as follows (i=6,7,8).(41)A≈B&B≈C⟹Γ⊢A≡B&Γ⊢B≡C&∀o∈Oi∀X∈ΓoX=1⟹oA=oB&∀o∈Oi∀X∈ΓoX=1⟹oB=oC⟹Γ⊢A≡C&∀o∈Oi∀X∈ΓoX=1⟹oA=oB&oB=oC⟹Γ⊢A≡C&∀o∈Oi∀X∈ΓoX=1⟹oA=oC⟹A≈C.Γ⊢A≡C above follows from A2 and the metaconjunction in the second but last line reduces to o(A)=o(C) by transitivity of equality.
In order to be a relation of congruence, the relation of equivalence must be compatible with the operations¬ and ∨. These proofs run as follows (i=6,7,8).(42)A≈B⟹Γ⊢A≡B&∀o∈Oi∀X∈ΓoX=1⟹oA=oB⟹Γ⊢¬A≡¬B&∀o∈Oi∀X∈ΓoX=1⟹oA′=oB′⟹Γ⊢¬A≡¬B&∀o∈Oi∀X∈ΓoX=1⟹o¬A=o¬B⟹¬A≈¬B(43)A≈B⟹Γ⊢A≡B&∀o∈Oi∀X∈ΓoX=1⟹oA=oB⟹Γ⊢A∨C≡B∨C&∀o∈Oi∀X∈ΓoX=1⟹oA∪oC=oB∪oC⟹A∨C≈B∨C.In the second step of (42), we used A3. In the second step of (43), we used A4 and A10. For the quantified part of these expressions, we applied the definition of Oi, i=6,7,8.Theorem 30.
The relation ofequivalence≈Γ,QL,1, or simply ≈1, defined as(44)A≈1B=defΓ⊢A≡qBis a relation of congruence, where Γ⊆F∘.Proof.
The proof for the relation of equivalence given by (44) is the well-known standard one.Theorem 31.
The relation ofequivalence≈Γ,CL,6, or simply ≈6¯, defined as(45)A≈6¯B=defΓ⊢A≡cB&∀o6∈Oi∀X∈Γo6X=1⟹o6A=o6Bis a relation of congruence, where Γ⊆F∘.Proof.
It is as given  in [28].Theorem 32.
The relation ofequivalence≈Γ,CL,2, or simply ≈2, defined as(46)A≈2B=defΓ⊢A≡cBis a relation of congruence, where Γ⊆F∘.Proof.
The proof for the relation of equivalence given by (46) is the well-known standard one.Definition 33.
The equivalence class for wffA under the relation of equivalence ≈ given by (40), (44), (45), and (46) is defined as |A|={B∈F∘:A≈B}, and one denotes F∘/≈={|A|:A∈F∘}. The equivalence classes define the natural morphism f:F∘→F∘/≈, which gives f(A)=def|A|. One writes a=f(A), b=f(B), and so forth.Lemma 34.
The relationa=b on F∘/≈ is given by (47)A=B⟺A≈B.Lemma 35.
The Lindenbaum-Tarski algebrasAj=〈F∘/≈j,¬/≈j,∨/≈j〉, j=6,7,8,1,6¯,2, are WOML∗ (or O6), or WOML1∗, or WOML2∗, or OML, or WDL∗ (O6), or DL; that is, (21) and (30), or (31), or (32), or (27), or (33), or (28) hold for ¬/≈j and ∨/≈j, j=6,7,8,1,6¯,2, as ′ and ∪, respectively, where—for simplicity—one uses the same symbols (′ and ∪) as for Oi, since there are no ambiguous expressions in which the origin of the operations would not be clear from the context.Proof.
For theΓ⊢A≡B part of the A≈B definition, the proofs of the ortholattice conditions, (21), follow from A5, A6, A9, the dual of A8, the dual of A7, and DeMorgan’s laws, respectively. (The duals follow from DeMorgan’s laws, derived from A10, A9, and A3.) For (31) and (32) we use Lemma  3.5 from [27] according to which any t=1 condition that holds in OML also holds in any WOML. Program beran [32] shows that the expressions ((a→1b)≡(b→1a))≡(a≡b) and (a≡b′→1a′)≡(a→1b) reduce to 1 in an OML. By Lemma  3.5 this means that ((a→1b)≡(b→1a))≡(a≡b)=1 and (a≡b′→1a′)≡(a→1b)=1 in any WOML. Now the Γ⊢A≡B part from (40) forces these WOML conditions into (31) and (32). For the quantified part of the A≈B definition, lattice O6 is a (proper) WOML. For the OML, we carry out the proof with the relation of equivalence without the quantified part in (40). Then the Γ⊢A≡B part from (40) forces the condition (a∪(a′∩(a∪b)))≡(a∪b)=1 which holds in any ortholattice into the OM law given by (27).We stress here that the Lindenbaum-Tarski algebrasAj, j=6,7,8,6¯, from Lemma 35 will be uniquely assigned to QL and CL via Theorems 42 and 43 in the sense that we have to use the relations of congruence given by (40) and (45) and that we cannot use those given by (44) and (46). For Aj, j=1,2, we have to use the latter ones and we cannot use the former ones. This is in contrast to the completeness proof given in [27] where we did not consider the set-theoretical difference WOML∗ but only WOML. But since WOML contains OML (unlike WOML∗), in [27] (unlike in this paper) we can use both relations of congruence (40), (45) and (44), and (46) to prove the completeness. We see that the usage of set-theoretical differences in this paper establishes a correlation between lattice models and equivalence relations for a considered logic as shown in Figure 2.Figure 2
Lattice models of quantum and classical logic together with the corresponding equivalence relations which define their Lindenbaum-Tarski algebras.Lemma 36.
In the Lindenbaum-Tarski algebraA, if f(X)=1 for all X in Γ implies f(A)=1, then Γ⊢A.Proof.
We carry out the proof just forA6. Proofs for other cases run analogously. Let us assume that f(X)=1 for all X in Γ imply f(A)=1, that is, |A|=1=|A|∪A′=|A∨¬A|, where the first equality is from Definition 33, the second equality follows from (22) (the definition of 1 in an ortholattice), and the third from the fact that ≈ is a congruence. Thus A≈(A∨¬A), which by definition means Γ⊢A≡(A∨¬A)&(∀o∈O6)[(∀X∈Γ)(o(X)=1)⇒o(A)=o((A∨¬A))]. The same holds for O7 and O8. This implies, in particular (by dropping the second conjunct), Γ⊢A≡(A∨¬A). Now in any ortholattice, a≡(a∪a′)=a holds. By mapping the steps in the proof of this ortholattice identity to steps in a proof in the logic, we can prove ⊢(A≡(A∨¬A))≡A from QL axioms A2–A14. (A direct proof of ⊢(A≡(A∨¬A))≡A is also not difficult.) Detaching the left-hand side (using A12, A13, A14, and R1), we conclude Γ⊢A.Theorem 37.
The orthomodular law does not hold inAj, j=6,7,8, for models WOML* (O6), WOML1∗, and WOML2∗.Proof.
We assumeF∘ contains at least two elementary (primitive) propositions p0,p1,…. We pick a valuation o that maps two of them, A and B, to distinct nodes o(A) and o(B) of O6 that are neither 0 nor 1 such that o(A)≤o(B) [i.e., o(A) and o(B) are on the same side of hexagon O6 in Figure 1]. From the structure of O6, we obtain o(A)∪o(B)=o(B) and o(A)∪(oA′∩(o(A)∪o(B)))=o(A)∪(oA′∩o(B))=o(A)∪0=o(A). Therefore o(A)∪o(B)≠o(A)∪(oA′∩(o(A)∪o(B)), that is, o(A∨B)≠o(A∨(¬A∧(A∨B))). This falsifies (A∨B)≈(A∨(¬A∧(A∨B)) which is an alternative way of expressing the orthomodularity property [45, 46]. Therefore a∪b≠a∪(a′∩(a∪b)), providing a counterexample to the orthomodular law for F∘/≈. We can follow the steps given above by taking o(A)=x and o(B)=y in Figure 1(a). For O7 and O8 the proofs are analogous. For instance, the orthomodularity is violated in Figure 1(b) for o(A)=x and o(B)=y and in Figure 1(c) for o(A)=w and o(B)=y.Theorem 38.
The orthomodular law holds inA1 for an OML model.Proof.
It is well-known.Theorem 39.
The distributive law does not hold inA6¯, for WDL∗ (O6).Proof.
It is as given in [28].Schechter [30, Sec. 9.4] gives O6 a set-valued interpretation by assigning {-1,0,1,} to 1 in Figure 1(a), {-1,0} to y, {0,1} to x′, {-1} to x, {1} to y′, and ⌀ to 0 and calls it the hexagon interpretation. “The hexagon interpretation is not distributive. That fact came as a surprise to some logicians, since the two-valued logic itself is distributive” [30, Sec. 9.5]. Schechter also gives crystal (6 subsets) and Church’s diamond (4 subsets) set-valued interpretations of CL in his Sections  9.7.–13. and 9.14.–17.Theorem 40.
The distributive law holds inA2 for a DL model (Boolean algebra).Proof.
It is well-known.Lemma 41.
M A j = 〈 A j , f 〉, j=6,7,8,1,6¯,2, is a proper WOML∗ (O6), WOML1∗, WOML2∗, OML, WDL∗ (O6), or DL model.Proof.
It follows from Lemma35.Now we are able to prove the completeness ofQL and CL; that is, if a formula A is a consequence of a set of wffs Γ in all O6, WOML∗, WOML1∗, WOML2∗, and OML models and in all O6, WDL∗, and DL models then Γ⊢QLA and Γ⊢CLA, respectively. In particular, when Γ=⌀, all valid formulae are provable in QL.Theorem 42 (completeness of quantum logic).
One has(48)Γ⊨MAjA⟹Γ⊢QLA,j=6,7,8,1.Proof.
Γ  ⊨ M  A means that, in all WOML∗ (O6), WOML1∗, WOML2∗, and OML models M, if f(X)=1 for all X in Γ, then f(A)=1 holds. In particular, it holds for MA=〈A,f〉, which is a WOML∗ (O6), WOML1∗, WOML2∗, or OML model by Lemma 41. Therefore, in the Lindenbaum-Tarski algebra A, if f(X)=1 for all X in Γ, then f(A)=1 holds. By Lemma 36, it follows that Γ⊢A.Theorem 43 (completeness of classical logic).
One has(49)Γ⊨MAjA⟹Γ⊢CLA,j=6¯,2.Proof.
It is as  given in [28].


## 5. Discussion

We have shown that quantum and classical axiomatic logic are metastructures for dealing with different algebras, in our case lattices, as their models. On the one hand, well- formed formulas in logic can be mapped to equations in different lattices, and on the other, equations from one lattice, which we are more familiar with or which are simpler or easier to handle, can be translated into equations of another lattice, through the logic which they are both models of.In Section4 we proved that quantum logic can be modelled by five different lattice models only one of which is orthomodular and that classical logic can be modelled by at least three lattice models only one of which is distributive. As we indicated in [39] there might be many more, possibly infinitely many, different lattice models quantum and classical axiomatic logic can be modelled with. (See also the remarks below Theorem 39.)The models are presented in a chart in Figure2. The key step that allows the multiplicity of lattice models for both kinds of logic is the refinement of the equivalence relations for the Lindenbaum-Tarski algebras in Theorems 29, 30, 31, and 32. They are also given in the chart where we can see that two different equivalence relations enable O6 to be a model of both quantum and classical logic. This is possible because both the weak orthomodularity (30) and the weak distributivity (34) pass O6 as pointed out below Definition 19.The essence of the equivalence classes of the Lindenbaum-Tarski algebras is that they are determined by special simple lattices, for example, those shown in Figure1, in which conditions that define definite other lattice models fail. The failure is significant because it proves that the orthomodularity (27) of OML is not needed to prove the completeness of quantum logic for WOML2∗, that neither orthomodularity (27) nor condition (32) is needed to prove the completeness for WOML1∗, and that neither orthomodularity (27) nor condition (32) nor condition (31) is needed for WOML∗.At the level of logical gates, classical or quantum, with today’s technology for computers and artificial intelligence, we can use only bits and qubits, respectively, that is, only valuations corresponding to two-valued DL (digital, binary, two-valued Boolean algebra) and OML, respectively. And when we talk about logic today, we take for granted that they have the latter valuation—TRUE, FALSE in the case of classical logic and Hasse diagrams in the case of quantum logic [40]. This is because a valuation is all we use to implement a logic. In its final application, we do not use a logic as given by its axioms and rules of inferences but as given by its models. So, it would be interesting to investigate how other valuations, that is, various WOMLs and WDLs, might be implemented in complex circuits. That would provide us with the possibility of controlling essentially different algebraic structures (logical models) implemented into radically different hardware (logic circuits consisting of logic gates) by the same logic that we use today with the standard bit and qubit gate technology.With these possible applications of quantum and classical logic we come back to the question which we started with: “Is Logic Empirical?” We have seen that logic is notuniquely empirical since it can simultaneously describe distinct realities. However, we have also seen (cf. Figure 2) that by means of chosen relations of equivalence we can link particular kinds of “empirical” models to quantum logic on the one hand and classical logic, on the other. Let us therefore briefly review the most recent elaborations on the question given by Bacciagaluppi [47] and Baltag and Smets [19]. They state “quantum logic is suitable as a logic that locally replaces classical logic when used to describe ‘a class of propositions in the context of quantum mechanical experiments.’”Our results show that this point can be supported as follows. The propositions of quantum logic correspond to elements of a Hilbert lattice and are not directly linked to measurement values. Such logic employs models which evaluate particular combinations of propositions and tells us whether they are true or not. Evaluation means mapping from a set of propositions to an algebra (lattice), through which a correspondence with measurement values indirectly emerges. Since the algebra must be an orthomodular lattice and cannot be a Boolean algebra we can say that quantum logic which has an orthomodular lattice as one of its models is “empirical” whenever we theoretically describe quantum measurements, simply because it can be linked to its algebraic model which serves for such a description: an orthomodular Hilbert lattice, that is, the lattice of closed subspaces of a complex Hilbert space.



---

*Source: 6830685-2016-08-31.xml*