A NATURAL DEDUCTION SYSTEM FOR ORTHOMODULAR LOGIC

Abstract

Orthomodular logic is a weakening of quantum logic in the sense of Birkhoff and von Neumann. Orthomodular logic is shown to be a nonlinear noncommutative logic. Sequents are given a physically motivated semantics that is consistent with exactly one semantics for propositional formulas that use negation, conjunction, and implication. In particular, implication must be interpreted as the Sasaki arrow, which satisfies the deduction theorem in this logic. As an application, this deductive system is extended to two systems of predicate logic: the first is sound for Takeuti’s quantum set theory, and the second is sound for a variant of Weaver’s quantum logic.

1 Introduction

Quantum logic as it was first defined by Birkhoff and von Neumann [5] is a semantics for propositional formulas that use conjunction, disjunction, and negation. In quantum logic, propositional formulas are interpreted as closed subspaces of a separable infinite-dimensional complex Hilbert space. Conjunction is interpreted as the intersection of closed subspaces, and negation is interpreted as their orthogonal complementation. Quantum logic satisfies De Morgan’s laws, so for convenience we use only conjunction and negation. The inclusion of closed subspaces yields a notion of entailment for propositional formulas. Because the separable infinite-dimensional Hilbert space is unique up to isomorphism, this notion of entailment may be regarded as canonical.

This semantics for propositional formulas is well motivated physically. The physical system that consists of a single quantum particle may be modeled by a separable infinite-dimensional complex Hilbert space [86], and it may be that every physical system can be modeled in this way [38]. In this context, the closed subspaces of the Hilbert space model true-false-valued physical quantities that are measurable in principle. In short, the closed subspaces of the Hilbert space are propositions about the physical system.

The inclusion of one closed subspace into another models the entailment of propositions in the fully literal sense that measuring the antecedent proposition to be true guarantees that a successive measurement of the consequent proposition will find it to be true as well. The orthocomplementation of closed subspaces likewise models the negation of propositions in the fully literal sense that measuring the negation of a proposition to be true guarantees that a successive measurement of that proposition will find it to be false. Unfortunately, there is no such simple account of conjunction and disjunction because measuring the truth-value of one proposition may alter the truth-value of another. Nevertheless, the conjunction of two propositions is the weakest proposition that entails both conjuncts.

Formally, we define quantum logic to be a binary consequence relation on the set of propositional formulas in the connectives $\mathbin {\wedge }$ and $\neg $ . We use a fixed countable infinite set of propositional variables throughout, and we treat $\phi \mathbin {\vee } \psi $ as an abbreviation of $\neg (\neg \phi \mathbin {\wedge } \neg \psi )$ . Let $L_0$ be the set of these propositional formulas, and let $\mathcal C$ be the set of closed subspaces of Hilbert space. A valuation of quantum logic is defined to be a function such that and . A sequent $\phi \vdash \psi $ is defined to be valid in quantum logic if for every valuation of quantum logic. We do not define the validity of $\Phi \vdash \psi $ in quantum logic for arbitrary $\Phi \subseteq L_0$ .

The study of quantum logic has proceeded slowly by modern standards. Shortly after the introduction of quantum logic, Husimi observed that this orthocomplemented lattice of propositions satisfies the orthomodular law [37]:

$$ \begin{align*} a \leq b \quad\Longrightarrow\quad a \mathbin{\vee} (\neg a \mathbin{\wedge} b) = b, \end{align*} $$

where $\neg a$ is the orthocomplement of a. Those orthocomplemented lattices that satisfy the orthomodular law are called orthomodular lattices [36]. The first entailment that is valid in quantum logic but not in orthomodular lattices was discovered by Greechie [26]. A number of other examples were then found and investigated [23, 55–60, 73]. Recently, building on the work of Slofstra [80], Fritz showed that the first-order theory of the ortholattice of closed subspaces of a separable infinite-dimensional Hilbert space is undecidable [17]. It is apparently still unknown whether the validity of an entailment in quantum logic is decidable.

This paper introduces a deductive system for orthomodular logic, which is also known as orthomodular quantum logic and sometimes simply as quantum logic. We define a valuation of orthomodular logic to be a function such that and , where ${\mathcal Q}$ is any orthomodular lattice. Thus, a sequent $\phi \vdash \psi $ is defined to be valid in orthomodular logic if for every valuation of orthomodular logic. Orthomodular logic may be regarded as a pragmatic approximation to quantum logic or, more speculatively, as a generalization of quantum logic that is applicable to physical models with exotic scalars such as formal Laurent series [28, 41]. An abundance of deductive systems for orthomodular logic has been proposed [6–10, 24, 31, 40, 62, 64, 71, 72, 83, 90]; most are glossed in [74] along with other systems of derivation. These deductive systems range from Hilbert-style systems such as [8, 40] to Gentzen-style systems such as [9, 64]. What is the use of yet another deductive system?

Quantum logic has been the subject of criticism on several fronts: that it is defective as a logic, that it is conceptually misguided, and that it is useless. The first of these critiques often focuses on the absence of a well-behaved implication that satisfies the deduction theorem, e.g., “there is no obvious notion of implication or deduction” [1], “no satisfactory implication operator has been found (so that there is no deductive system in quantum logic)” [35]. The former authors go on to observe that “quantum logic was therefore always seen as logically very weak, or even a non-logic.” The second critique is more philosophical and has reached extreme conclusions, e.g., “the tale of quantum logic is not the tale of a promising idea gone bad, it is rather the tale of the unrelenting pursuit of a bad idea” [54], “quantum logic was a mistake a priori” [21]. The third critique is simply that quantum logic has not played its hoped-for role in either physics or in mathematics, e.g., “quantum logic … has never yielded the goods” [54], “it has proved to be mathematically sterile: it fails to link up in interesting ways with mainstream developments in mathematical physics” [29].

This paper offers some evidence to the contrary for each of these three critiques. First, it introduces a natural deductive system for orthomodular logic that does carry a canonical notion of implication that satisfies the deduction theorem. Second, it introduces a natural semantics for sequents that mirrors experimental procedure. Third, it generalizes this deductive system to a quantum predicate logic that is applicable to discrete quantum structures in the sense of noncommutative geometry. This is the application that motivated this research.

The immediate subject of this paper is the following deductive system:

Definition 1.1 We define the propositional deductive system $SOM$ :

1. (1) A formula is built up from propositional letters using the connectives $\mathbin {\wedge }$ , $\mathbin {\rightarrow }$ , and $\neg $ .

2. (2) A sequent is an expression of the form $\phi _1, \ldots , \phi _n \vdash \psi $ , where $\phi _1 \ldots , \phi _n$ , and $\psi $ are formulas with $n \geq 0$ .

3. (3) A sequent is derivable if it can be derived using the inference rules in Figure 1, where $\phi $ , $\psi $ , and $\chi $ are formulas and $\Gamma $ is a finite sequence of formulas, possibly empty.

   

   Fig. 1 The deductive system $SOM$ . Top to bottom and left to right in Figure 1, the inference rules of $SOM$ are the assumption rule, the cut rule, the paste rule, the compatible exchange rule, the $\mathbin {\wedge }$ -introduction rule, the left $\mathbin {\wedge }$ -elimination rule, the right $\mathbin {\wedge }$ -elimination rule, the $\mathbin {\rightarrow }$ -introduction rule, the $\mathbin {\rightarrow }$ -elimination rule, the excluded middle rule, and the deductive explosion rule.

The antecedent of a sequent is a sequence of formulas, not a set. The intuitive meaning of a judgement $\phi _1, \ldots , \phi _n \vdash \psi $ is that after verifying each of the formulas $\phi _1, \ldots , \phi _n$ via measurement and in that order, a measurement of the truth-value of $\psi $ is guaranteed to find that it is true. The semantics that we will shortly define is entirely faithful to this intuition.

The deductive system $SOM$ includes an implication connective that satisfies the deduction theorem by fiat. Furthermore, it uniquely determines a notion of implication in orthomodular logic:

Result 1 (Sasaki arrow)

The following rules of inference are derivable in $SOM$ :

This implication connective is of course the familiar Sasaki arrow [34, 79]. A number of authors have argued that the Sasaki arrow is the natural implication connective for quantum logic [15, 30, 32, 46, 61, 62]. Result 1 motivates the Sasaki arrow purely from logical considerations; we have made no assumptions on the implication connective except those that are implicit in the notion itself (cf. [63, p. 187]).

The deductive system $SOM$ might be called a substructural logic because its logical rules are all familiar rules of inference from classical logic. The weakening and contraction rules

are both admissible in $SOM$ , but the exchange rule

is not admissible. The addition of this exchange rule recovers classical logic:

Result 2 (Noncommutativity)

Let $\phi _1, \ldots , \phi _n$ , and $\psi $ be propositional formulas in the connectives $\mathbin {\wedge }$ , $\mathbin {\rightarrow }$ , and $\neg $ . Then, the following are equivalent:

1. (1) The sequent $\phi _1, \ldots , \phi _n \vdash \psi $ is derivable in $SOM$ with the exchange rule.

2. (2) The formula $(\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi $ is classically derivable.

The deductive system $SOM$ is not formally a substructural logic [77] because the cut rule that is standard in substructural logics is not admissible. Nevertheless, Result 2 justifies the conceptual claim that $SOM$ is a noncommutative logic.

The idea that orthomodular logic could be a structurally noncommutative logic is natural and even expected due to the prominent role of noncommutativity in quantum theory. Noncommutativity is a key feature in the standard general formulation of Heisenberg’s uncertainty principle [27]. It is also the defining feature of quantum mathematics in the sense noncommutative geometry [25]. This noncommutativity is closely related to the noncommutativity of $SOM$ as Lemma A.2 demonstrates. Furthermore, Malinowski proved in essence that no commutative formulation of orthomodular logic can satisfy the deduction theorem [51, theorem 2.7], though a “semiclassical” deductive theorem may be formulated [83, p. 668].

It is therefore surprising that no noncommutative deductive systems for orthomodular logic have appeared in the literature. This is all the more surprising because the idea that the order of assumptions should be significant to quantum logic has been investigated before. In this respect, the nearest proof system to $SOM$ is probably Mittelstaedt’s quantum dialogic [63]. This is essentially a game-theoretic semantics that formalizes a debate between a proponent and an opponent of a proposition. The players are constrained in when they may cite a previously proved proposition, and this constraint reflects that the result of one measurement may be “destroyed” by another [63, p. 178]. The same intuition explains why all sequents of the form $\Gamma , \phi , \psi \vdash \psi $ are derivable in $SOM$ , but not all sequents of the form $\Gamma , \psi , \phi \vdash \psi $ are derivable. Surprisingly, the natural deduction system that has been obtained from quantum dialogic is commutative [81].

A noncommutative semantics for sequents was previously considered by Bell, and furthermore, his semantics satisfies the deduction theorem [4, eq. (4.5)]. However, the deductive system $SOM$ is not sound for Bell’s semantics [4, p. 95], and Bell describes the specification of a deductive system for his semantics as an “open problem” [4, p. 97]. Instead, $SOM$ is sound for an experimentally motivated semantics, as anticipated by Lehmann [49, p. 62].

This semantics for $SOM$ interprets each sequent of experimentally decidable propositions as an experimentally falsifiable proposition. For any interpretation of formulas of any kind as true-false-valued observables on a physical system, the naive meaning of a judgement $\phi _1, \ldots , \phi _n \vdash \psi $ is that whenever we have verified the formulas $\phi _1, \ldots , \phi _n$ , we may also be certain of the truth of $\psi $ . If we formalize these observables by closed subspaces of Hilbert space and we notate our interpretation by , then this condition is equivalent to the inclusion , where $\mathbin {\&}$ is the Sasaki projection [79]. This equivalence appears to be folklore; we record a proof of it in Appendix A.

In principle, the same observable can be measured by different experimental procedures that may be distinguished by their effect on the system. This distinction is clearly significant to any discussion of sequential measurements. We assume minimally destructive procedures, which are characterized by the property that any state in which the truth or falsehood of the proposition is certain is left unaltered by the measurement. We may gloss this assumption by saying that other procedures measure more than they purport to measure.

If A and B are closed subspaces of Hilbert space, then $A \mathbin {\&} B$ may be defined as the closure of the projection of A onto B. Thus, $A \mathbin {\&} B$ is spanned by those vector states that may be obtained by verifying A and then verifying B, where the term “verify” means “measure to be true.” The four structural rules of $SOM$ are valid for this interpretation of sequents in any physical system that can modeled using Hilbert space, in contrast to the structural rules of classical natural deduction. The seven logical rules of $SOM$ simply express the familiar meanings of the logical connectives $\mathbin {\wedge }$ , $\mathbin {\rightarrow }$ , and $\neg $ .

We may formalize this discussion. In any orthomodular lattice, we may define the Sasaki projection of elements a and b to be the element $a \mathbin {\&} b = (a \mathbin {\vee } \neg b) \mathbin {\wedge } b$ . Our convention is that the connective $\mathbin {\&}$ associates to the left. A sequent $\phi _1, \ldots , \phi _n \vdash \psi $ is defined to be valid in orthomodular logic if for every valuation of orthomodular logic. We extend the notion of a valuation to the language $L_1 \supset L_0$ that includes the implication connective by requiring that for all formulas $\phi $ and $\psi $ , because $a\mathbin {\&} b \leq c$ if and only if $a \leq \neg b \mathbin {\vee } (b \mathbin {\wedge } c)$ for all elements a, b, and c of any orthomodular lattice. Furthermore, the uniqueness of right adjoints implies that this is the only choice of implication for which $SOM$ could be sound. So it is:

Result 3 (Soundness and completeness)

A sequent $\phi _1, \ldots , \phi _n \vdash \psi $ is derivable in $SOM$ if and only if it is valid in orthomodular logic.

The deductive system $SOM$ is presented as a calculus of sequents, but in substance, it is a system of natural deduction. No proof of this claim is possible because natural deduction remains an informal notion. Nevertheless, Appendix B provides an argument in three parts: First, a sequent calculus may be a natural deduction system [75]. Second, $SOM$ may also be presented as a natural deduction system in the style of Fitch [16, 39]. Third, the given formulation of $SOM$ can be adjusted to exclude all rules that allow an assertion only after one or more additional assumptions. This third argument addresses readers who, unlike the author, find such rules to be incompatible with their conception of natural deduction.

In contrast, $SOM$ is not a sequent calculus in the vein of $LJ$ and $LK$ , Gentzen’s prototypical sequent calculuses [18]. In these systems, logical rules have the subformula property: each formula in a premise is a subformula of a formula in the conclusion. This feature is typical of the sequent calculuses for orthomodular logic and related logics that have appeared in the literature [7, 9, 64, 65, 83]. However, the elimination rules of $SOM$ do not have the subformula property. Instead, they follow the pattern typical of natural deduction.

The experience of the author is that $SOM$ formalizes a coherent mode of reasoning as in the case of intuitionistic logic. To provide evidence for this claim, we include derivations that might otherwise be left as exercises for the reader. In particular, we continue the development of the deductive system $SOM$ by deriving the primitive rules of inference for the defined connectives $\mathbin {\vee }$ and $\mathbin {\bot \!\!\!\bot }$ :

Result 4 (Disjunction and compatibility)

Let $\phi \mathbin {\vee } \psi $ be an abbreviation for $\neg (\neg \phi \mathbin {\wedge } \neg \psi )$ , and let $\phi \mathbin {\bot \!\!\!\bot } \psi $ be an abbreviation for $(\phi \mathbin {\rightarrow } (\psi \mathbin {\rightarrow } \phi )) \mathbin {\wedge } (\psi \mathbin {\rightarrow } (\phi \mathbin {\rightarrow } \psi ))$ . Then, the rules of inference in Figure 2 are derivable in $SOM$ .

Fig. 2 Primitive rules of inference for $\mathbin {\vee }$ and $\mathbin {\bot \!\!\!\bot }$ .

We also exhibit a derivation that the compatibility connective $\mathbin {\bot \!\!\!\bot }$ is equivalent to the commutator that was introduced by Marsden [53]. This notation is due to Takeuti [82, sec. 1].

Result 5 (Commutator)

The following rules of inference are derivable in $SOM$ :

The primitive rules of inference given for $\mathbin {\bot \!\!\!\bot }$ in Figure 2 clearly imply that $\phi \mathbin {\bot \!\!\!\bot } \psi $ is equivalent to $(\phi \mathbin {\rightarrow } (\psi \mathbin {\rightarrow } \phi )) \mathbin {\wedge } (\psi \mathbin {\rightarrow } (\phi \mathbin {\rightarrow } \psi ))$ , and hence Result 5 is comparable to Result 1 in that it motivates the common interpretation of a connective from the primitive inference rules for that connective.

We also extend $SOM$ to a deductive system for quantum predicate logic. We do so in two distinct ways because there are broadly two distinct notions of a quantum set. These two notions do not represent competing conceptions of quantum mathematics but rather distinct generalizations of sets within the same conception of quantum mathematics.

The term “quantum set theory” commonly refers to a generalization of the Boolean-valued models $V^{(\mathcal B)}$ in which the complete Boolean algebra $\mathcal B$ is replaced with a complete orthomodular lattice ${\mathcal Q}$ [11, 66, 69, 70, 82]. In the case of primary interest, this complete orthomodular lattice ${\mathcal Q}$ consists of the closed subspaces of a Hilbert space $\mathcal H$ . By Gleason’s theorem, the states of a physical system modeled by $\mathcal H$ are in one-to-one correspondence with countably additive measures on ${\mathcal Q}$ , as long as the dimension of $\mathcal H$ is greater than two [22]. In this way, each state assigns a probability to each sentence of the language of set theory with constants from the orthomodular-valued model $V^{({\mathcal Q})}$ . The canonical name of a generic ultrafilter behaves in some ways like a “hidden variable” of the physical system.

Result 6 (Takeuti’s semantics)

Let ${\mathcal Q}$ be a complete orthomodular lattice. Let

be Takeuti’s interpretation of formulas in the language of set theory with constants from $V^{({\mathcal Q})}$ [76, 82]. Let $SOM_{{\mathcal Q}}$ be the deductive system of single-sorted predicate logic whose rules of inference are those of Figure 1 together with

where the former rule is subject to the standard constraint that y must not appear freely in $\Gamma \vdash (\forall x)\phi $ . Then, for each closed formula $\psi $ , if $\vdash \psi $ is derivable in $SOM_{{\mathcal Q}}$ , then

.

The most prominent connection between quantum set theory and quantum mechanics is the so-called Takeuti correspondence, which is a canonical bijection between the real numbers in $V^{({\mathcal Q})}$ and the real-valued observables on a physical system modeled by $\mathcal H$ , when ${\mathcal Q}$ consists of the closed subspaces of $\mathcal H$ [82, p. 321], [66, theorem 6.1]. In this context, Ozawa has analyzed the compatibility of real-valued observables from the perspective of quantum logic [67, 68]. We do not treat bounded quantifiers because they are not expressible within the language of set theory in quantum set theory [82, p. 315]. However, if we treat quantum sets extensionally rather than intentionally, then we may clearly treat bounded quantifiers as abbreviations in the obvious way.

The term “quantum set” may also refer to the discrete quantum spaces of noncommutative geometry [43, 76]. A quantum set in this sense is essentially just a von Neumann algebra that may be noncommutative but that is otherwise very similar to the von Neumann algebra of all bounded complex-valued functions on a set. We show that $SOM$ extends to a natural deductive system that is sound for Weaver’s quantum predicate logic [87, sec. 2.6] as it applies to these quantum sets, albeit only for nonduplicating formulas. A formula of first-order logic is defined to be nonduplicating if no variable occurs more than once in any atomic subformula. This syntactic constraint reflects the absence of diagonal functions in noncommutative geometry [89] and the impossibility of broadcasting quantum states [3].

Result 7 (Weaver’s semantics)

Let be the semantics that is defined in [44]. Let $SOM_{\mathbf q}$ be the deductive system of many-sorted predicate logic whose rules of inference are those of Figure 1 together with the following:

1. (1) where y does not appear freely in $\Gamma \vdash (\forall x) \phi $ ,

2. (2) where $\phi $ and t have no free variables in common,

3. (3) where $\phi $ and $\psi $ have no free variables in common.

Then, for each closed formula $\psi $ , if $\vdash \psi $ is derivable in $SOM_{\mathbf q}$ , then .

Many classes of discrete quantum structures may be axiomatized within quantum predicate logic [44, sec. 1.5] including discrete quantum graphs, discrete quantum groups, and discrete quantum isomorphisms [45]. Such discrete quantum structures are quantum sets equipped with suitably generalized relations and functions of various arity. The ubiquitous qualifier “discrete” addresses the fact that within noncommutative geometry many structures are implicitly topological or measurable. For example, quantum groups generalize locally compact groups [48], and quantum graphs generalize measurable graphs [88]. These discrete quantum structures all originate in mathematical physics. Quantum graphs were motivated by quantum error correction [12], quantum groups were motivated by the quantization of physical symmetry [76], and quantum graph isomorphisms were motivated by quantum nonlocality [2, 52]. The general notion of a discrete quantum structure also traces its origins to the problem of quantum error correction [43, 44, 47, 88]. With these examples in hand, we may begin to address the third cited critique of quantum logic that it has no meaningful connection to physics or to mathematics.

The deductive systems $SOM_{{\mathcal Q}}$ and $SOM_{\mathbf q}$ are incomparable, even if we restrict $SOM_{\mathbf q}$ to a single sort. This is to be expected because we are generalizing the set-theoretic universe in two very different ways. Intuitively, a Boolean-valued model is a classical space whose points are copies of the cumulative hierarchy, even if the Boolean algebra has no complete ultrafilters and thus the space has no points in the literal sense. An orthomodular-valued model is similarly a quantum space whose points are copies of the cumulative hierarchy, but its universe, i.e., its class of constants, is entirely classical. Each member of the universe is a mathematical object, which may be named and duplicated. In contrast, the universe of a single-sorted structure in noncommutative geometry is a single discrete quantum space, whose points are just a figure of speech. In short, intuitively, $SOM_{{\mathcal Q}}$ is the logic of a quantum space of classical structures, whereas $SOM_{\mathbf q}$ is the logic of a classical space of quantum structures. For this reason, the closed formulas of $SOM_{\mathbf q}$ satisfy classical logic; this is reflected in rule (3) of Result 7. One convenient consequence of this principle is that a theorem that follows from a sequence of axioms may be asserted after any sequence of additional assumptions, because the theorem is a closed formula and it therefore commutes with each of the assumptions.

This paper does not include a completeness theorem that is converse to Result 6 or Result 7. A general completeness result for $SOM_{{\mathcal Q}}$ appears to be out of reach, because it is unknown whether every orthomodular lattice has a completion [33, sec. 6]. A completeness result for $SOM_{\mathbf q}$ appears to be even further out of reach because orthomodular logic is far from being complete for finite-dimensional Hilbert spaces. A symmetric monoidal category of orthomodular quantum sets [78] along the lines of [43] might bridge that gap.

Finally, we define the existential quantifier and derive its primitive rules of inference:

Result 8 (Existential quantification)

Let $(\exists x)\phi $ be an abbreviation for $\neg (\forall x)\neg \phi $ . Then, the following rules of inference are derivable in $SOM_{{\mathcal Q}}$ and $SOM_{\mathbf q}$ :

where the latter rule is subject to the standard constraint that y must not appear freely in $\Gamma \vdash (\exists x)\phi $ or in $\psi $ . In the case of $SOM_{\mathbf q}$ , the former rule is also subject to the constraint that t and $\phi $ must have no free variables in common.

We offer an intuitive justification of the new premise in the $\exists $ -elimination rule. The assumption $\phi [x/y]$ may be regarded as creating an element y that satisfies $\phi $ . If $\Gamma \vdash (\exists x) \phi $ is derivable, then we may create such an element consistently: if $\Gamma \vdash (\exists x) \phi $ and $\Gamma , \phi [x/y] \vdash \psi \mathbin {\wedge } \neg \psi $ are both derivable, then so is $\Gamma \vdash \psi \mathbin {\wedge } \neg \psi $ . However, the formula $\psi $ may be a consequence of creating y and not a consequence of the possibility of creating y. In this sense, the existential quantifier expresses a potential rather than an actual existence. Modulo $\Gamma , \phi [x/y] \vdash \psi $ , the sequent $\Gamma , \psi , \phi [x/y] \vdash \psi $ expresses that $\psi $ is compatible with the creation of y.

The first deductive system for quantum predicate logic was introduced by Dishkant [10]. His inference rules for the existential quantifier,

where $\phi \mathbin {\rightarrow }_D \psi $ abbreviates $\neg \psi \mathbin {\rightarrow } \neg \phi $ , are easily derived in $SOM_{{\mathcal Q}}$ by using the primitive rules for the universal quantifier. An equivalent deductive system was then investigated by Dunn, who showed that within quantum predicate logic, the axioms of Peano arithmetic imply those of classical logic [13]. More recently, Titani has formulated a sequent calculus for quantum predicate logic [83, sec. 3.2], which use a modally closed implication connective that satisfies a restricted deduction theorem.

The development of $SOM$ coincided with development of several other deductive systems that incorporate the Sasaki adjunction. In the Implicational Quantum Logic of Tokuo [84], the Sasaki projection is a primitive logical connective. Furthermore, in the Orthomodular Groupoid Calculus of Fazio, Ledda, Paoli and St. John [14] and the Projective Linear Logic of Lehmann [50], the Sasaki projection is a structural connective, as it is in $SOM$ . Tokuo has also introduced a natural deduction system for orthomodular logic in the style of Gentzen’s $NJ$ and $NK$ [85]. It satisfies a restricted deduction theorem.

Conventions

The unqualified terms “formula,” “sequent,” and “derivation” refer to the formulas, sequents, and derivations of $SOM$ . Hilbert spaces are over the complex numbers.

2 Conjunction, implication, and negation

This section exhibits a number of derivations, beginning with a few simple derivations of some familiar rules of inference and ending with two derivations that characterize the implication connective as the Sasaki arrow.

Proposition 2.1. The following inference rules are derivable:

Proof.

Lemma 2.2. The following sequents are derivable:

1. (1) $\Gamma , \neg \phi , \phi \vdash \psi $ ,

2. (2) $\Gamma , \neg \neg \phi \vdash \phi $ ,

3. (3) $\Gamma , \phi , \neg \phi \vdash \psi $ ,

4. (4) $\Gamma , \phi \vdash \neg \neg \phi $ .

Proof.

Proposition 2.3. The following inference rules are derivable:

Proof. Refer to Proposition 2.1 and Lemma 2.2.

Lemma 2.4. The following inference rules are derivable:

Proof. Refer to Lemma 2.2.

Theorem 2.5. The inference rules in Figure 3 are derivable.

Fig. 3 Some generalized rules of inference that are derivable in $SOM$ .

Proof. In the special case that $\Delta $ is empty, each of the rules in Figure 3 is derivable either because it is a primitive rule of $SOM$ or by Lemmas 2.2 and 2.4. For each of these rules, the general case follows from this special case via the $\mathbin {\rightarrow }$ -introduction and $\mathbin {\rightarrow }$ -elimination rules, as in Lemma 2.2. For illustration, we prove that the generalized paste rule is derivable. The proof proceeds by induction on the length of $\Delta $ . The special case that $\Delta $ is empty is the base case of the induction.

Let $\ell \geq 0$ , and assume that the generalized paste rule is derivable for all sequences $\Delta $ of length $\ell $ . Let $\Delta '$ be a sequence of length $\ell +1$ ; it is of the form $\Delta , \delta '$ for some sequence $\Delta $ of length $\ell $ and some formula $\delta '$ . We now derive $\Gamma , \phi , \Delta , \delta ' \vdash \psi $ from $\Gamma \vdash \phi $ and $\Gamma , \Delta , \delta ' \vdash \psi $ :

In other words, we have derived $\Gamma , \phi , \Delta ' \vdash \psi $ from $\Gamma \vdash \phi $ and $\Gamma , \Delta ' \vdash \psi $ . Proceeding by induction on $\ell $ , we conclude that the generalized paste rule is derivable for all sequences $\Delta $ of arbitrary length. The derivability of the other nine rules is proved similarly.

Lemma 2.6. The following sequents are derivable:

1. (1) $\Gamma , \phi \mathbin {\wedge } \psi , \neg \phi \vdash \phi \mathbin {\wedge } \psi $ and $\Gamma , \phi \mathbin {\wedge } \psi , \neg \psi \vdash \phi \mathbin {\wedge } \psi $ ,

2. (2) $\Gamma , \neg \phi , \phi \mathbin {\wedge } \psi \vdash \neg \phi $ and $\Gamma , \neg \psi , \phi \mathbin {\wedge } \psi \vdash \neg \psi $ ,

3. (3) $\Gamma , \neg (\phi \mathbin {\wedge } \psi ), \phi \vdash \neg (\phi \mathbin {\wedge } \psi )$ and $\Gamma , \neg (\phi \mathbin {\wedge } \psi ), \psi \vdash \neg (\phi \mathbin {\wedge } \psi )$ ,

4. (4) $\Gamma , \phi , \neg (\phi \mathbin {\wedge } \psi ) \vdash \phi $ and $\Gamma , \psi , \neg (\phi \mathbin {\wedge } \psi ) \vdash \psi $ .

Proof. We exhibit the derivations of four of these sequents because the derivations of the other four sequents are entirely similar. Refer to Proposition 2.3 and Theorem 2.5.

Proposition 2.7. The following inference rules are derivable:

Proof. We exhibit the derivation of one of these rules because the derivations of the other three rules are entirely similar. Refer to Theorem 2.5 and Lemma 2.6.

Proposition 2.8. The following inference rules are derivable:

Proof. We exhibit the derivations of two of these rules because the derivations of the other two rules are entirely similar. Refer to Proposition 2.3 and Lemma 2.6.

Theorem 2.9. The following inference rules are derivable:

Proof. Refer to Proposition 2.8.

Refer to Propositions 2.3 and 2.7.

3 Noncommutativity, soundness, and completeness

This section contains proofs establishing the basic metamathematical properties of $SOM$ . We begin with the admissibility of the weakening rule.

Proposition 3.1. If a sequent $\Gamma \vdash \phi $ is derivable, then $\Delta ,\Gamma \vdash \phi $ is also derivable.

Proof. Recall that the length of a derivation is the number of inferences in that derivation. We prove the proposition by induction on the length of a derivation of $\Gamma \vdash \phi $ . If $\Gamma \vdash \phi $ has a derivation of length one, then it is of the form $\Gamma _0, \phi \vdash \phi $ , and hence $\Delta , \Gamma \vdash \phi $ is of the form $\Delta ,\Gamma _0, \phi \vdash \phi $ . Therefore, if $\Gamma \vdash \phi $ has a derivation of length $\ell = 1$ , then $\Delta , \Gamma \vdash \phi $ is derivable.

Let $\ell> 1$ , and assume that the proposition holds for all sequents that have a derivation of length smaller than $\ell $ . Let $\Gamma \vdash \phi $ be a sequent that has a derivation of length $\ell $ . Then, there exist sequents $\Gamma _1 \vdash \phi _1$ , $\Gamma _2 \vdash \phi _2$ , and $\Gamma _3 \vdash \phi _3$ , which may be identical, that have derivations of length less than $\ell $ and that yield $\Gamma \vdash \phi $ via a primitive inference of $SOM$ :

Perusing Figure 1, we conclude that

is also a primitive inference of $SOM$ . By the induction hypothesis, the sequents $\Delta , \Gamma _1 \vdash \phi _1$ , $\Delta , \Gamma _2 \vdash \phi _2$ , and $\Delta , \Gamma _3 \vdash \phi _3$ are all derivable, and thus the sequent $\Delta , \Gamma \vdash \phi $ is also derivable. Therefore, the proposition holds for all sequents that have a derivation of length smaller than or equal to $\ell $ . By induction on $\ell $ , the proposition holds for all sequents that have a derivation of any length.

Let H be the Hilbert-type deductive system given in [42, sec. 19]. Let $LK$ be the deductive system $G1$ given in [42, sec. 77]. Let the exchange rule (E) be the following rule of inference:

Theorem 3.2. Let $\phi _1, \ldots , \phi _n \vdash \psi _0$ be a sequent. Then, the following are equivalent:

1. (1) $\phi _1, \ldots , \phi _n \vdash \psi _0$ is derivable in $SOM + E$ .

2. (2) $\phi _1, \ldots , \phi _n \vdash \psi _0$ is derivable in $LK$ .

3. (3) $(\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi _0$ is derivable in H.

When $n=0$ , the expression $(\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi _0$ means $\psi _0$ .

Proof. To prove the implication $(1) \Rightarrow (2)$ , it is sufficient to prove that each of the inference rules of $SOM + E$ is derivable in $LK$ . This is a set of exercises in introductory logic. We further remark only that each inference rule of $SOM+E$ is derivable in $LK$ because $LK$ does include the cut rule, which is merely admissible rather than derivable in the rest of that system. The implication $(2) \Rightarrow (3)$ is essentially just [42, theorem 47] [19, sec. V.6]. Indeed the deduction theorem for H implies that $\psi _0$ may be derived from the assumptions $\phi _1, \ldots , \phi _n$ if and only if the formula $(\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi _0$ may be derived without any assumptions [42, theorem 1]. It remains to prove the implication $(3) \Rightarrow (1)$ .

Assume that the formula $(\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi _0$ has a derivation in H. As a consequence of the cut elimination theorem, this formula has a derivation in H that uses only those logical axioms of H that contain the symbols $\mathbin {\wedge }$ , $\mathbin {\rightarrow }$ , and $\neg $ [42, theorems 46 and 47 and corollary 2]. For each such logical axiom $\alpha $ , the sequent $\vdash \alpha $ is derivable in $SOM + E$ : The sequent $\vdash \phi \mathbin {\rightarrow } (\psi \mathbin {\rightarrow } \phi )$ has the derivation

The sequent $\vdash (\phi \mathbin {\rightarrow } \psi ) \mathbin {\rightarrow } ((\phi \mathbin {\rightarrow } (\psi \mathbin {\rightarrow } \chi )) \mathbin {\rightarrow } (\phi \mathbin {\rightarrow } \chi ))$ has the derivation

The sequent $\vdash \phi \mathbin {\rightarrow } (\psi \mathbin {\rightarrow } (\phi \mathbin {\wedge } \psi ))$ has the derivation

The sequents $\vdash (\phi \mathbin {\wedge } \psi ) \mathbin {\rightarrow } \phi $ and $\vdash (\phi \mathbin {\wedge } \psi ) \mathbin {\rightarrow } \psi $ have the derivations

By Lemma 2.3, the sequent $\vdash (\phi \mathbin {\rightarrow } \psi ) \mathbin {\rightarrow } ((\phi \mathbin {\rightarrow } \neg \psi ) \mathbin {\rightarrow } \neg \phi )$ has the derivation

By Lemma 2.2, the sequent $\vdash \neg \neg \phi \mathbin {\rightarrow } \phi $ has the derivation

Therefore, for every logical axiom $\alpha $ in the derivation of $(\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi _0$ , the sequent $\vdash \alpha $ is derivable in $SOM+E$ .

Furthermore, by Proposition 2.1, the inference rule

is also derivable in $SOM+E$ . Therefore, we may transform a derivation of $(\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi _0$ in H into a derivation of $\vdash (\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi _0$ in $SOM+E$ essentially by placing the symbol $\vdash $ in front of each formula. Formally, this is a straightforward inductive argument. We conclude that the sequent $\vdash (\phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n) \mathbin {\rightarrow } \psi _0$ is derivable in $SOM+E$ .

By Proposition 3.1 and the $\mathbin {\rightarrow }$ -elimination rule, the sequent $\phi _1, \ldots , \phi _n, \phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n \vdash \psi _0$ is also derivable in $SOM+E$ . Certainly, so is the sequent $\phi _1, \ldots , \phi _n \vdash \phi _1 \mathbin {\wedge } \cdots \mathbin {\wedge } \phi _n$ . Appealing to the cut rule, we conclude that $\phi _1, \dots , \phi _n \vdash \psi _0$ is derivable in $SOM+E$ , proving the implication $(3) \Rightarrow (1)$ .

In any orthomodular lattice ${\mathcal Q}$ , the binary operations $\mathbin {\&}$ and $\mathbin {\rightarrow }$ are defined by $a \mathbin {\&} b = (a \mathbin {\vee } \neg b) \mathbin {\wedge } b$ and $a \mathbin {\rightarrow } b = \neg a \mathbin {\vee } (a \mathbin {\wedge } b)$ for all $a, b \in {\mathcal Q}$ . Our convention is that $\mathbin {\&}$ associates with the left and $\mathbin {\rightarrow }$ associates with the right. Furthermore, $a_1 \mathbin {\&} \cdots \mathbin {\&} a_n$ denotes $\top $ when $n=0$ .

Definition 3.3. Let $L_1$ be the set of formulas of $SOM$ . We define an interpretation to be a function such that ${\mathcal Q}$ is an orthomodular lattice. Thus, a valuation of orthomodular logic is an interpretation such that

1. (1) ,

2. (2) ,

3. (3)

for all formulas $\phi $ and $\psi $ . We define a sequent $\phi _1, \ldots , \phi _n \vdash \psi $ to be true in an interpretation if . We define a rule of inference to be sound in an interpretation if its conclusion is true whenever its premises are all true.

The definition of a true sequent is motivated by Theorem A.3. The definition of a valuation is then motivated by the following proposition:

Proposition 3.4. Let be a surjective interpretation. If the rules of inference of $SOM$ are all sound in this interpretation, then is a valuation of orthomodular logic.

Proof. Let ${\mathcal Q}$ be the orthomodular lattice that is the codomain of the interpretation . Assume that the rules of inference of $SOM$ are all sound.

Let $\phi $ be a formula. Let $\alpha $ be a formula such that

, and let $\beta $ be a formula such that

. By assumption, the following derivations both yield sound rules of inference:

The soundness of the first rule implies that , and thus, . We certainly have that and , so the soundness of the second rule implies that . Altogether, we have that is a complement of that is orthogonal to . Therefore, for all formulas $\phi $ .

Let $\phi $ and $\psi $ be formulas. Let $\gamma $ be a formula such that

. By assumption, the following derivations all yield sound rules of inference:

The soundness of the first two rules implies that and ; thus, is a lower bound of and . We certainly have that and , so the soundness of the third rule implies that . Altogether, we have that is a lower bound of and that is at least as large as their greatest lower bound . Therefore, for all formulas $\phi $ and $\psi $ .

Let $\phi $ and $\psi $ be formulas. By Theorem 2.9, the following derivations yield sound rules of inference:

The soundness of the first rule implies that

, and the soundness of the second rule implies the opposite inequality. Altogether, we have that

Therefore,

for all formulas $\phi $ and $\psi $ .

Theorem 3.5. The rules of inference of $SOM$ are sound in every valuation of orthomodular logic.

Proof. For brevity, we use the notation , where $\Gamma $ is the sequence $\gamma _1, \ldots , \gamma _n$ .

First, we prove the soundness of the conjunction and implication rules. Let $\Gamma \vdash \phi $ and $\Gamma \vdash \psi $ be sequents, and assume that they are true. Then, we have that and , and hence . In other words, $\Gamma \vdash \phi \mathbin {\wedge } \psi $ is true. Therefore, the $\mathbin {\wedge }$ -introduction rule is sound. We may similarly conclude that the $\mathbin {\wedge }$ -elimination rules are sound.

The $\mathbin {\rightarrow }$ -introduction and $\mathbin {\rightarrow }$ -elimination rules are both sound if and only if the inequality is equivalent to the inequality for all $\Gamma $ , $\phi $ , and $\psi $ . These inequalities certainly are equivalent because the inequalities $a \mathbin {\&} b \leq c$ and $a \leq b \mathbin {\rightarrow } c$ are equivalent in every orthomodular lattice [15]. Therefore, the $\mathbin {\rightarrow }$ -introduction rule and the $\mathbin {\rightarrow }$ -elimination rule are sound.

Of the six remaining rules of inference, we may prove the soundness of all but the compatible exchange rule by appealing to the soundness of the rules for conjunction and implication and to the theorem that the orthomodular lattice $2^4 \times MO2$ is the free orthomodular lattice on two generators [40, theorem 2.1]. This theorem implies that an inequality in two variables holds universally in all orthomodular lattices if it holds in $2$ and in $MO2$ , making the verification of such inequalities a matter of routine computation.

For illustration, we prove the soundness of the excluded middle rule. Let $\Gamma , \phi \vdash \psi $ and $\Gamma , \neg \phi \vdash \psi $ be sequents, and assume that they are true. By the soundness of the conjunction and implication rules, we find that $\Gamma \vdash (\phi \mathbin {\rightarrow } \psi ) \mathbin {\wedge } (\neg \phi \mathbin {\rightarrow } \psi )$ is also true. By routine computation, we find that the inequality $(a \mathbin {\rightarrow } b) \mathbin {\wedge } (\neg a \mathbin {\rightarrow } b) \leq b$ holds universally in any orthomodular lattice. We infer that

Thus, the sequent $\Gamma \vdash \psi $ is true. Therefore, the excluded middle rule is sound. We may similarly conclude that the deductive explosion rule, the assumption rule, the cut rule, and the paste rule are all sound.

That leaves the compatible exchange rule, which is not directly amenable to the same approach. However, we can use the same approach to prove the soundness of the rule

We can then prove the soundness of the compatible exchange rule by deriving it from the rules whose soundness we have already established:

We have now established the soundness of all 11 inference rules of $SOM$ .

Lemma 3.6. The deductive system $SOM$ has the following properties:

1. (1) If $\phi \vdash \psi $ and $\psi \vdash \chi $ are both derivable, then $\phi \vdash \chi $ is derivable.

2. (2) If $\phi \vdash \psi $ is derivable, then $\neg \psi \vdash \neg \phi $ is derivable.

Proof. Assume that $\phi \vdash \psi $ and $\psi \vdash \chi $ are both derivable. By Proposition 3.1, the sequent $\phi , \psi \vdash \chi $ is also derivable, and therefore, so is the sequent $\phi \vdash \chi $ :

Assume that $\phi \vdash \psi $ is derivable. By Proposition 3.1, the sequent $\neg \psi , \phi \vdash \psi $ is also derivable, and therefore, so is the sequent $\neg \psi \vdash \neg \phi $ :

Refer to Proposition 2.3 and Theorem 2.5.

Definition 3.7. For all formulas $\phi $ and $\psi $ of $SOM$ , we define $\phi \leq \psi $ if $\phi \vdash \psi $ is derivable in $SOM$ . This relation is reflexive by Definition 1.1 and transitive by Lemma 3.6(1). In other words, $(L_1, \leq )$ is a preordered set. We define $(\mathcal L_1,\leq )$ to be the partially ordered set that is obtained by identifying formulas that are equivalent in $(L_1, \leq )$ .

Let $[\,\cdot \,]\colon L_1 \to \mathcal L_1$ be the quotient map. The function $\phi \mapsto \neg \phi $ on $L_1$ is order-reversing by Lemma 3.6(2), so the function $[\phi ] \mapsto [\neg \phi ]$ on $\mathcal L_1$ is well-defined and order-reversing. We define $\neg [\phi ] = [\neg \phi ]$ for all formulas $\phi $ of $L_1$ .

Theorem 3.8. The structure $(\mathcal L_1, \leq , \neg )$ is an orthomodular lattice. Furthermore, the quotient map $[\,\cdot \,]\colon L_1 \to \mathcal L_1$ is a valuation of orthomodular logic.

Proof. First, we observe that the quotient map $[\,\cdot \,]\colon L_1 \to \mathcal L_1$ satisfies conditions (1)–(3) of Definition 3.3. It satisfies condition (1) because $[\phi \mathbin {\wedge } \psi ]$ is the meet of $[\phi ]$ and $[\psi ]$ due to the logical rules for conjunction. It satisfies condition (3) by Definition 3.7. Finally, it satisfies condition (2) by Theorem 2.9, which implies that $[\phi \mathbin {\rightarrow } \psi ] = [\neg (\phi \mathbin {\wedge } \neg (\phi \mathbin {\wedge } \psi ))]$ . Therefore, the quotient map $[\,\cdot \,]\colon L_1 \to \mathcal L_1$ satisfies conditions (1)–(3) of Definition 3.3, and it is a valuation if $(\mathcal L_1, \leq , \neg )$ is an orthomodular lattice.

The function $\neg \colon [\phi ] \mapsto [\neg \phi ]$ is an involution of $(\mathcal L_1, \leq )$ by Lemma 2.2. We have already observed that $(\mathcal L_1, \leq )$ has binary meets with $[\phi ] \mathbin {\wedge } [\psi ] = [\phi \mathbin {\wedge } \psi ]$ . Since $\neg $ is an order-reversing involution, $(\mathcal L_1, \leq )$ also has binary joins with $[\phi ] \mathbin {\vee } [\psi ] = [\neg (\neg \phi \mathbin {\wedge } \neg \psi )]$ . For all formulas $\phi $ and $\psi $ , the sequent $\phi \mathbin {\wedge } \neg \phi \vdash \psi $ is derivable:

we have appealed to Proposition 2.1. Thus, $(\mathcal L_1, \leq )$ has a least element, and moreover, $[\phi ] \mathbin {\wedge } \neg [\phi ]$ is equal to that least element for every formula $\phi $ . Applying the order-reversing involution $\neg $ , we find that $(\mathcal L_1, \leq )$ also has a greatest element, and moreover, $\neg [\phi ] \mathbin {\vee } [\phi ]$ is equal to that greatest element for every formula $\phi $ . Therefore, $(\mathcal L_1, \leq , \neg )$ is an ortholattice.

Let $\phi $ and $\psi $ be formulas such that $[\phi ] \leq [\psi ]$ , that is, such that the sequent $\phi \vdash \psi $ is derivable. By Proposition 3.1, the sequent $\neg \phi , \psi , \phi \vdash \psi $ is also derivable. We apply Proposition 2.3 and Theorems 2.5 and 2.9 to derive $\psi \vdash \neg (\neg \phi \mathbin {\wedge } \neg (\neg \phi \mathbin {\wedge } \psi ))$ :

Therefore, $[\psi ] \leq [\neg (\neg \phi \mathbin {\wedge } \neg (\neg \phi \mathbin {\wedge } \psi ))] = \neg (\neg [\phi ] \mathbin {\wedge } \neg (\neg [\phi ] \mathbin {\wedge } [\psi ])) = [\phi ] \vee (\neg [\phi ] \mathbin {\wedge } [\psi ])$ .

For the opposite inequality, we reason that $\neg \phi \mathbin {\rightarrow } \psi , \phi \vdash \psi $ is derivable by Proposition 3.1, and hence the sequent $\neg \phi \mathbin {\rightarrow } \psi \vdash \psi $ is derivable:

Thus, $[\neg \phi \mathbin {\rightarrow } \psi ] \leq [\psi ]$ . By Theorem 2.9, we also have that $[\neg (\neg \phi \mathbin {\wedge } \neg (\neg \phi \mathbin {\wedge } \psi ))] \leq [\neg \phi \mathbin {\rightarrow } \psi ]$ , and therefore

$$ \begin{align*}[\phi] \vee (\neg [\phi] \mathbin{\wedge} [\psi]) = \neg(\neg [\phi] \mathbin{\wedge} \neg (\neg [\phi] \mathbin{\wedge} [\psi])) = [\neg(\neg \phi \mathbin{\wedge} \neg (\neg \phi \mathbin{\wedge} \psi))] \leq [\neg \phi \mathbin{\rightarrow} \psi] \leq [\psi].\end{align*} $$

Altogether, we have that $[\phi ] \vee (\neg [\phi ] \mathbin {\wedge } [\psi ])= [\psi ]$ for all formulas $\phi $ and $\psi $ such that $[\phi ] \leq [\psi ]$ . We conclude that $(\mathcal L_1, \leq , \neg )$ is an orthomodular lattice, as claimed.

Corollary 3.9. If a sequent is true in every valuation of orthomodular logic, then that sequent is derivable in $SOM$ .

Proof. Let $\phi _1, \ldots , \phi _n \vdash \psi $ be a sequent that it is true in every valuation. By Theorem 3.8, the quotient map $[\,\cdot \,]\colon L_1 \to \mathcal L_1$ is a valuation; hence $[\phi _1] \mathbin {\&} \cdots \mathbin {\&} [\phi _n] \leq [\psi ]$ . Repeatedly applying the adjunction between $\mathbin {\&}$ and $\mathbin {\rightarrow }$ [15], we conclude that $[\phi _1] \mathbin {\rightarrow } \cdots \mathbin {\rightarrow } [\phi _n] \mathbin {\rightarrow } [\psi ]$ is the greatest element of $\mathcal L_1$ . Thus, $[\phi _1 \mathbin {\rightarrow } \cdots \mathbin {\rightarrow } \phi _n \mathbin {\rightarrow } \psi ]$ is the greatest element of $\mathcal L_1$ . In particular, the sequents $\psi \vdash \phi _1 \mathbin {\rightarrow } \cdots \mathbin {\rightarrow } \phi _n \mathbin {\rightarrow } \psi $ and $\neg \psi \vdash \phi _1 \mathbin {\rightarrow } \cdots \mathbin {\rightarrow } \phi _n \mathbin {\rightarrow } \psi $ are both derivable. Applying the excluded middle rule, we infer that $\vdash \phi _1 \mathbin {\rightarrow } \cdots \mathbin {\rightarrow } \phi _n \mathbin {\rightarrow } \psi $ is derivable. Repeatedly applying the $\mathbin {\rightarrow }$ -elimination rule, we conclude that $\phi _1, \ldots , \phi _n \vdash \psi $ is derivable.

4 Disjunction and compatibility

Definition 4.1. We introduce two abbreviations:

1. (1) Let $\phi \mathbin {\vee } \psi $ be an abbreviation for $\neg (\neg \phi \mathbin {\wedge } \neg \psi )$ .

2. (2) Let $\phi \mathbin {\bot \!\!\!\bot } \psi $ be an abbreviation for $(\phi \mathbin {\rightarrow } (\psi \mathbin {\rightarrow } \phi )) \mathbin {\wedge } (\psi \mathbin {\rightarrow } (\phi \mathbin {\rightarrow } \psi ))$ .

In this section, we derive the primitive inference rules for these two connectives. We also derive the equivalence between the given expression for $\phi \mathbin {\bot \!\!\!\bot } \psi $ and the standard expression for it. Along the way, we derive a number of other rules of inference that express intelligible logical principles. We do not appeal to the results of Section 3 in any way. This section exhibits the derivations whose existence it claims, continuing the development that was initiated in Section 2.

Proposition 4.2. The following inference rule is derivable:

Proof. Refer to Proposition 2.3 and Theorem 2.5.

Lemma 4.3. The following inference rule is derivable:

Proof. Refer to Propositions 2.3 and 4.2 and Theorem 2.5.

Theorem 4.4. The following inference rule is derivable:

Proof. Refer to Theorems 2.5 and 2.9, Propositions 2.7 and 2.8, and Lemma 4.3.

Corollary 4.5. The following inference rules are derivable:

Proof. Refer to Proposition 2.3 and Theorems 2.5 and 4.4.

Corollary 4.6. The following inference rules are derivable:

Proof. The two introduction rules are derivable by Proposition 2.8. For the derivation of the elimination rule, refer to Proposition 2.3, Theorems 2.5 and 4.4, and Lemma 4.3.

Proposition 4.7. The following inference rules are derivable:

Proof. Refer to Theorem 2.5.

The derivation of the third rule is entirely similar to that of the second.

Proposition 4.8. The following inference rules are derivable:

Proof. Refer to Propositions 2.3 and 4.7, Theorem 2.5, and Corollary 4.5.

The derivations of the two remaining rules for negation are entirely similar.

The derivation of the remaining rule for conjunction is entirely similar.

Proposition 4.9. The following inference rule is derivable:

Proof. Refer to Theorem 2.5 and Proposition 4.8.

Lemma 4.10. The following inference rules are derivable:

Proof. Refer to Proposition 4.8.

Proposition 4.11. The following inference rules are derivable:

Proof. Refer to Corollary 4.6, Proposition 4.8, and Lemma 4.10.

Let $\chi _0$ be the formula $((\phi \mathbin {\wedge } \psi ) \mathbin {\vee } (\phi \mathbin {\wedge } \neg \psi )) \mathbin {\vee } ((\neg \phi \mathbin {\wedge } \psi ) \mathbin {\vee } (\neg \phi \mathbin {\wedge } \neg \psi ))$ .

Lemma 4.12. The following inference rules are derivable:

Consequently, the following sequents are derivable:

1. (1) $\Gamma , \phi \mathbin {\wedge } \psi \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $ ,

2. (2) $\Gamma , \phi \mathbin {\wedge } \neg \psi \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $ ,

3. (3) $\Gamma , \neg \phi \mathbin {\wedge } \psi \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $ ,

4. (4) $\Gamma , \neg \phi \mathbin {\wedge } \neg \psi \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $ .

Proof. Refer to Propositions 4.7 and 4.8.

The derivation of the rule

is entirely similar.

Lemma 4.13. The following inference rule is derivable:

Consequently, the following sequents are derivable:

1. (1) $\Gamma , (\phi \mathbin {\wedge } \psi ) \mathbin {\vee } (\phi \mathbin {\wedge } \neg \psi ) \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $ ,

2. (2) $\Gamma , (\neg \phi \mathbin {\wedge } \psi ) \mathbin {\vee } (\neg \phi \mathbin {\wedge } \neg \psi ) \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $ .

Proof. Refer to Corollary 4.6, Proposition 4.8, and Lemma 4.12. Let $\xi _1$ be the formula $\phi \mathbin {\wedge } \psi $ , and let $\xi _2$ be the formula $\phi \mathbin {\wedge } \neg \psi $ .

It follows that sequent (1) is derivable. So is sequent (2):

Proposition 4.14. The following inference rule is derivable:

Proof. Refer to Corollary 4.6 and Lemma 4.13. Let $\zeta _1$ be the formula $(\phi \mathbin {\wedge } \psi ) \mathbin {\vee } (\phi \mathbin {\wedge } \neg \psi )$ , and let $\zeta _2$ be the formula $(\neg \phi \mathbin {\wedge } \psi ) \mathbin {\vee } (\neg \phi \mathbin {\wedge } \neg \psi )$ .

5 Universal and existential quantification

This section extends the propositional deductive system $SOM$ to two predicate deductive systems. The first is shown to be sound for Takeuti’s semantics [82], and the second is shown to be sound for a variant of Weaver’s semantics [87]. For simplicity, we identify formulas that differ only in the symbols used for their bound variables so that any term is substitutable for any variable in any formula.

Throughout this section, let ${\mathcal Q}$ be a complete orthomodular lattice, and let $V^{({\mathcal Q})}$ be the ${\mathcal Q}$ -valued universe [82], [70, sec. 4.1].

Definition 5.1. We define the single-sorted predicate deductive system $SOM_{{\mathcal Q}}$ :

1. (1) Its formulas are the first-order formulas whose

   1. (a) connectives are $\mathbin {\wedge }$ , $\mathbin {\rightarrow }$ , and $\neg $ ;

   2. (b) quantifiers are $\forall $ ;

   3. (c) relation symbols are $=$ and $\in $ ;

   4. (d) constant symbols are the elements of $V^{({\mathcal Q})}$ , with no other function symbols.

2. (2) Its rules of inference are those in Figure 1 together with

   
   where the former rule is subject to the standard constraint that the variable x must not appear freely in $\Gamma $ .

Corollary 5.2. Let be a ${\mathcal Q}$ -valued interpretation of the formulas of $SOM_{{\mathcal Q}}$ whose quantized implication is the Sasaki arrow [70, sec. 4.2], e.g., Takeuti’s interpretation [82]. Let $\phi $ be a closed formula of $SOM_{{\mathcal Q}}$ . If $\vdash \phi $ is derivable in $SOM_{{\mathcal Q}}$ , then .

Proof. We define a sequent $\phi _1(x_1, \ldots , x_m), \ldots , \phi _n(x_1, \ldots , x_m) \vdash \psi (x_1, \ldots , x_m)$ to be ${{\mathcal Q}}$ -true if for all $u_1, \ldots , u_m \in V^{({\mathcal Q})}$ . We prove by induction that every derivable sequent of $SOM_{{\mathcal Q}}$ is ${\mathcal Q}$ -true. It is evidently sufficient to verify that each rule is ${\mathcal Q}$ -sound: if its premises are ${\mathcal Q}$ -true, then its conclusion is also ${\mathcal Q}$ -true. For those rules that appear in Figure 1, this follows by Theorem 3.5.

Let $\phi _1(x_1, \ldots , x_m), \ldots , \phi _n(x_1, \ldots , x_m) \vdash \psi (x_0, x_1, \ldots , x_m)$ be a ${\mathcal Q}$ -true sequent. Then,

for all $u_1, \ldots , u_m \in V^{({\mathcal Q})}$ . Therefore, the sequent $\phi _1(x_1, \ldots , x_m), \ldots , \phi _n(x_1, \ldots , x_m) \vdash (\forall x_0) \psi (x_0, x_1, \ldots , x_m)$ is ${\mathcal Q}$ -true, and more generally, the $\forall $ -introduction rule is ${\mathcal Q}$ -sound.

Let $\phi _1(x_1, \ldots , x_m), \ldots , \phi _n(x_1, \ldots , x_m) \vdash (\forall x_0) \psi (x_0, x_1, \ldots , x_m)$ be a ${\mathcal Q}$ -true sequent, and let t be a term. We calculate that

for all $u_1, \ldots , u_m \in V^{({\mathcal Q})}$ . If t is a variable, then $\phi _1(x_1, \ldots , x_m), \ldots , \phi _n(x_1, \ldots , x_m) \vdash \psi (t, x_1, \ldots , x_m)$ is ${\mathcal Q}$ -true because

for all $u_0 \in V^{({\mathcal Q})}$ , and if t is a constant, then $\phi _1(x_1, \ldots , x_m), \ldots , \phi _n(x_1, \ldots , x_m) \vdash \psi (t, x_1, \ldots , x_m)$ is ${\mathcal Q}$ -true for the same reason. Therefore, the $\forall $ -elimination rule is ${\mathcal Q}$ -sound.

Altogether, we find that all of the inference rules of $SOM_{{\mathcal Q}}$ are ${\mathcal Q}$ -sound. In particular, if $\phi $ is a closed formula such that $\vdash \phi $ is derivable in $SOM_{{\mathcal Q}}$ , then $\vdash \phi $ is ${\mathcal Q}$ -true, and thus as desired.

The quantum sets that are the discrete quantum spaces of noncommutative geometry [43, definition 2.1], [76] form a category in two inequivalent natural ways. The category $\mathbf {qSet}$ of quantum sets and functions generalizes the category $\mathbf {Set}$ of sets and functions, and it is dual to the category of hereditarily atomic von Neumann algebras and unital normal $*$ -homomorphisms [43, definition 5.3 and theorem 7.4]. The category $\mathbf {qRel}$ of quantum sets and binary relations generalizes the category $\mathbf {Rel}$ of sets and binary relations, and it is dual to the category of hereditarily atomic von Neumann algebras and quantum relations in the sense of Weaver [44, Appendix A.2], [88].

A function between quantum sets is formally a kind of binary relation between quantum sets [43, definition 4.1]; $\mathbf {qSet}$ is a subcategory of $\mathbf {qRel}$ . The two categories share the same symmetric monoidal structure, whose product is notated $\times $ because it generalizes the Cartesian product of sets in a suitable way [43, definitions 2.2 and 3.3]. The unit of the monoidal structure is notated $\mathbf {1}$ . For a quantum set $\mathcal X$ , there exist suitable projection functions $\mathcal X \times \mathcal X \to \mathcal X$ , but in general, there does not exist a suitable diagonal function $\mathcal X \to \mathcal X \times \mathcal X$ [43, definition 10.3]. This is not a defect in the definition but rather a basic feature of quantum spaces in noncommutative geometry [89].

In this setting, we work with a class of formulas that does not presume the existence of diagonal functions. A nonduplicating formula is a formula such that no variable, bound or free, appears more than once in any atomic subformula. For illustration, $P(x,y) \mathbin {\wedge } Q(x,y)$ is a nonduplicating formula, and $P(x,x) \mathbin {\wedge } Q(y,y)$ is not a nonduplicating formula.

Definition 5.3. We define the many-sorted predicate deductive system $SOM_{\mathbf q}$ :

1. (1) Its formulas are the nonduplicating first-order formulas whose

   1. (a) connectives are $\mathbin {\wedge }$ , $\mathbin {\rightarrow }$ , and $\neg $ ;

   2. (b) quantifiers are $\forall $ ;

   3. (c) sorts are quantum sets;

   4. (d) relation symbols of each arity $(\mathcal X_1, \ldots , \mathcal X_n)$ are binary relations $\mathcal X_1 \times \cdots \times \mathcal X_n \to \mathbf 1;$

   5. (e) function symbols of each arity $(\mathcal X_1, \ldots , \mathcal X_m; \mathcal Y)$ are functions $\mathcal X_1 \times \cdots \times \mathcal X_m \to \mathcal Y.$

2. (2) Its rules of inference are those in Figure 1 together with

   
   where the first rule is subject to the constraint that x must not appear freely in $\Gamma $ , the second rule is subject to the constraint that $\phi $ and t must not have any free variables in common, and the third rule is subject to the constraint that $\phi $ and $\psi $ must not have any free variables in common.

Corollary 5.4. Let be Weaver’s interpretation of the formulas of $SOM_{\mathbf q}$ [44, sec. 2], [87] with implication being interpreted as the Sasaki arrow. Let $\phi $ be a closed formula of $SOM_{\mathbf q}$ . If $\vdash \phi $ is derivable in $SOM_{\mathbf q}$ , then .

Proof. We define a sequent $\phi _1, \ldots , \phi _n \vdash \psi $ to be ${\mathbf q}$ -true if for all tuples of distinct variables $\bar x = (x_1, \ldots , x_m)$ that include the free variables of the sequent. We prove by induction that every derivable sequent in $SOM_{\mathbf q}$ is ${\mathbf q}$ -true. It is evidently sufficient to verify that each rule is ${\mathbf q}$ -sound: if its premises are ${\mathbf q}$ -true, then its conclusion is ${\mathbf q}$ -true. For those rules that appear in Figure 1, this follows by Theorem 3.5; the binary relations between any two quantum sets form an orthomodular lattice [43, definition 3.8].

Let $\phi _1, \ldots , \phi _n \vdash \psi $ be a ${\mathbf q}$ -true sequent, and let $x_0$ be a variable that does not appear freely in the antecedent. Let $\overline x = (x_1, \ldots , x_m)$ be a tuple of distinct variables that includes the free variables of the sequent $\phi _1, \ldots , \phi _n \vdash (\forall x_0)\psi $ . Without loss of generality, we may assume that $x_0$ does not appear in $\overline x$ . Because the sequent $\phi _1, \ldots , \phi _n \vdash \psi $ is ${\mathbf q}$ -true, we have that

. By [44, proposition 2.3.3],

for each index $i \in \{1, \ldots , n\}$ , where $\mathcal X_0$ is the sort of $x_0$ . We calculate that

which implies that

by [44, definition 2.3.2]. Therefore, $\phi _1, \ldots , \phi _n \vdash (\forall x_0) \psi $ is ${\mathbf q}$ -true, and more generally, the $\forall $ -introduction rule is ${\mathbf q}$ -sound.

Let $\phi _1, \ldots , \phi _n \vdash (\forall x_0)\psi $ be a ${\mathbf q}$ -true sequent, and let t be a term of the same sort as $x_0$ . Assume that $\psi $ and t have no free variables in common. Let $\overline x = (x_1, \ldots , x_m)$ be a tuple of distinct variables that includes the free variables of $\phi _1, \ldots , \phi _n \vdash \psi [x_0/t]$ . Without loss of generality, we may assume that $x_0$ does not appear in $\overline x$ . Let $\overline y = (y_1, \ldots , y_k)$ and $\overline z = (z_1, \ldots , z_{\ell })$ be tuples of distinct variables such that the variables of t appear in $\overline y$ , the free variables of $\psi $ appear in $\overline z$ , and the concatenation of $\overline y$ and $\overline z$ is a permutation of $\overline x$ . In particular $\overline y$ and $\overline z$ have no variables in common, and neither include $x_0$ .

Let $\mathcal X_0$ be the sort of $x_0$ , let $\mathcal Y_1, \ldots , \mathcal Y_k$ be the sorts of $y_1, \ldots , y_k$ , respectively, and let $\mathcal Z_1, \ldots , \mathcal Z_{\ell }$ be the sorts of $z_1, \ldots , z_{\ell }$ , respectively. Let $\mathcal Y = \mathcal Y_1 \times \cdots \times \mathcal Y_k$ , and let $\mathcal Z = \mathcal Z_1 \times \cdots \times \mathcal Z_{\ell }$ . We calculate that

where

because

is a function by [44, lemma 3.5.3] and

by Proposition C.2. Indeed, any function F from a quantum set $\mathcal Y$ to a quantum set $\mathcal X_0$ satisfies $\top _{\mathcal Y} = \top _{\mathcal X_0} \circ F$ because $\top _{\mathcal Y} = \top _{\mathcal Y} \circ I_{\mathcal Y} \leq \top _{\mathcal Y} \circ F^{\dagger } \circ F \leq \top _{\mathcal X_0} \circ F $ . We conclude that

. It follows by [44, definition 2.2.4 and proposition 2.3.3] that

. Therefore, the sequent $\phi _1, \ldots , \phi _n \vdash \psi [x_0/t]$ is ${\mathbf q}$ -true, and more generally, the $\forall $ -elimination is ${\mathbf q}$ -sound.

Let $\phi _1, \ldots , \phi _n, \phi , \psi \vdash \chi $ be a ${\mathbf q}$ -true sequent, and assume that $\phi $ and $\psi $ have no variables in common. Let $\overline x$ be a tuple of distinct variables that includes the free variables of $\phi _1, \ldots , \phi _n, \psi , \phi \vdash \chi $ . Let $\overline y = (y_1, \ldots , y_k)$ and $\overline z = (z_1, \ldots , z_{\ell })$ be tuples of distinct variables such that the free variables of $\phi $ appear in $\overline y$ , the free variables of $\psi $ appear in $\overline z$ , and the concatenation of $\overline y$ and $\overline z$ is a permutation of $\overline x$ . Let $\mathcal Y_1, \ldots , \mathcal Y_k$ be the sorts of $y_1, \ldots , y_k$ , and let $\mathcal Z_1, \ldots , \mathcal Z_{\ell }$ be the sorts of $z_1, \ldots , z_{\ell }$ . Let $\mathcal Y = \mathcal Y_1 \times \cdots \times \mathcal Y_k$ , and let $\mathcal Z = \mathcal Z_1 \times \cdots \times \mathcal Z_{\ell }$ . Applying [44, proposition 2.3.3], we calculate that

where the first and fourth equalities follow by [44, proposition 2.3.3] and the second and third equalities follow by linear algebra [43, definition 3.8]. It follows by [44, definition 2.2.4 and proposition 2.3.3] that

. Therefore, the sequent $\phi _1, \ldots , \phi _n, \psi , \phi \vdash \chi $ is ${\mathbf q}$ -true, and more generally, the third rule of inference in Definition 5.3 is ${\mathbf q}$ -sound.

Altogether, we have that all of the inference rules of $SOM_{\mathbf q}$ are ${\mathbf q}$ -sound. In particular, if $\phi $ is a closed formula such that $\vdash \phi $ is derivable in $SOM_{\mathbf q}$ , then $\vdash \phi $ is ${\mathbf q}$ -true.

Definition 5.5. Let $(\exists x) \phi $ be an abbreviation for $\neg (\forall x) \neg \phi $ .

Lemma 5.6. The sequent $\Gamma \vdash (\forall x) \phi \mathbin {\bot \!\!\!\bot } \phi [x/t]$ is derivable in $SOM_{{\mathcal Q}}$ . It is also derivable in $SOM_{\mathbf q}$ if $\phi $ and t have no free variables in common.

Proof. Refer to Proposition 4.7.

Proposition 5.7. The following inference rules are derivable in $SOM_{{\mathcal Q}}$ :

where the latter rule is subject to the standard constraint that the variable x must not appear freely in $\Gamma $ or in $\psi $ . Both rules are also derivable in $SOM_{\mathbf q}$ if the former rule is subject to the additional constraint that $\phi $ and t have no free variables in common.

Proof. Refer to Propositions 2.3, 4.2, and 4.7–4.9, Theorem 2.5, and Lemma 5.6.