1 Introduction
Quantum logic as it was first defined by Birkhoff and von Neumann [Reference Birkhoff and von Neumann5] 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 [Reference von Neumann86], and it may be that every physical system can be modeled in this way [Reference Jaffe and Witten38]. 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 [Reference Husimi37]:
$$ \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 [Reference Holland and Hooker36]. The first entailment that is valid in quantum logic but not in orthomodular lattices was discovered by Greechie [Reference Greechie, Beltrametti and Fraassen26]. A number of other examples were then found and investigated [Reference Godowski23, Reference Mayet55–Reference Megill and Pavičić60, Reference Pavičić, Megill, Gabbay and Lehmann73]. Recently, building on the work of Slofstra [Reference Slofstra80], Fritz showed that the first-order theory of the ortholattice of closed subspaces of a separable infinite-dimensional Hilbert space is undecidable [Reference Fritz17]. 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 [Reference Gross and Künzi28, Reference Keller and Ochsenius41]. An abundance of deductive systems for orthomodular logic has been proposed [Reference Cattaneo, Dalla Chiara, Giuntini, Paoli, Engesser, Gabbay and Lehmann6–Reference Dishkant10, Reference Goldblatt24, Reference Hardegree31, Reference Kalmbach40, Reference Mittelstaedt62, Reference Nishimura64, Reference Pavičić71, Reference Pavičić and Megill72, Reference Titani, Engesser, Gabbay and Lehmann83, Reference Zeman90]; most are glossed in [Reference Pavičić, Megill and Lehmann74] along with other systems of derivation. These deductive systems range from Hilbert-style systems such as [Reference Dalla Chiara8, Reference Kalmbach40] to Gentzen-style systems such as [Reference Delmas-Rigoutsos9, Reference Nishimura64]. 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” [Reference Abramsky and Coecke1], “no satisfactory implication operator has been found (so that there is no deductive system in quantum logic)” [Reference Heunen, Landsman and Spitters35]. 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” [Reference Maudlin and Ben-Menahem54], “quantum logic was a mistake a priori” [Reference Girard21]. 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” [Reference Maudlin and Ben-Menahem54], “it has proved to be mathematically sterile: it fails to link up in interesting ways with mainstream developments in mathematical physics” [Reference Halvorson and Halvorson29].
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) A formula is built up from propositional letters using the connectives
$\mathbin {\wedge }$
,
$\mathbin {\rightarrow }$
, and
$\neg $
. -
(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) 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 [Reference Herman, Marsden and Piziak34, Reference Sasaki79]. A number of authors have argued that the Sasaki arrow is the natural implication connective for quantum logic [Reference Finch15, Reference Hardegree30, Reference Hardegree32, Reference Kunsemüller46, Reference Mittelstaedt61, Reference Mittelstaedt62]. 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. [Reference Mittelstaedt63, 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) The sequent
$\phi _1, \ldots , \phi _n \vdash \psi $
is derivable in
$SOM$
with the exchange rule. -
(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 [Reference Restall77] 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 [Reference Griffiths27]. It is also the defining feature of quantum mathematics in the sense noncommutative geometry [Reference Gracia-Bondía, Várilly and Figueroa25]. 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 [Reference Malinowski51, theorem 2.7], though a “semiclassical” deductive theorem may be formulated [Reference Titani, Engesser, Gabbay and Lehmann83, 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 [Reference Mittelstaedt63]. 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 [Reference Mittelstaedt63, 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 [Reference Stachow81].
A noncommutative semantics for sequents was previously considered by Bell, and furthermore, his semantics satisfies the deduction theorem [Reference Bell4, eq. (4.5)]. However, the deductive system
$SOM$
is not sound for Bell’s semantics [Reference Bell4, p. 95], and Bell describes the specification of a deductive system for his semantics as an “open problem” [Reference Bell4, p. 97]. Instead,
$SOM$
is sound for an experimentally motivated semantics, as anticipated by Lehmann [Reference Lehmann49, 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 [Reference Sasaki79]. 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 [Reference Pelletier and Hazen75]. Second,
$SOM$
may also be presented as a natural deduction system in the style of Fitch [Reference Fitch16, Reference Jaśkowski39]. 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 [Reference Gentzen18]. 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 [Reference Cutland and Gibbins7, Reference Delmas-Rigoutsos9, Reference Nishimura64, Reference Nishimura65, Reference Titani, Engesser, Gabbay and Lehmann83]. 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 [Reference Marsden53]. This notation is due to Takeuti [Reference Takeuti, Beltrametti and Fraassen82, 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}$
[Reference Döring, Eva and Ozawa11, Reference Ozawa66, Reference Ozawa69, Reference Ozawa70, Reference Takeuti, Beltrametti and Fraassen82]. 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 [Reference Gleason22]. 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})}$
[Reference Podleś and Woronowicz76, Reference Takeuti, Beltrametti and Fraassen82]. 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$
[Reference Takeuti, Beltrametti and Fraassen82, p. 321], [Reference Ozawa66, theorem 6.1]. In this context, Ozawa has analyzed the compatibility of real-valued observables from the perspective of quantum logic [Reference Ozawa67, Reference Ozawa68]. We do not treat bounded quantifiers because they are not expressible within the language of set theory in quantum set theory [Reference Takeuti, Beltrametti and Fraassen82, 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 [Reference Kornell43, Reference Podleś and Woronowicz76]. 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 [Reference Weaver87, 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 [Reference Woronowicz89] and the impossibility of broadcasting quantum states [Reference Barnum, Caves, Fuchs, Jozsa and Schumacher3].
Result 7 (Weaver’s semantics)
Let
be the semantics that is defined in [Reference Kornell44]. 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)
where y does not appear freely in
$\Gamma \vdash (\forall x) \phi $
, -
(2)
where
$\phi $
and t have no free variables in common, -
(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 [Reference Kornell44, sec. 1.5] including discrete quantum graphs, discrete quantum groups, and discrete quantum isomorphisms [Reference Kornell45]. 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 [Reference Kustermans and Vaes48], and quantum graphs generalize measurable graphs [Reference Weaver88]. These discrete quantum structures all originate in mathematical physics. Quantum graphs were motivated by quantum error correction [Reference Duan, Severini and Winter12], quantum groups were motivated by the quantization of physical symmetry [Reference Podleś and Woronowicz76], and quantum graph isomorphisms were motivated by quantum nonlocality [Reference Atserias, Mančinska, Roberson, Šámal, Severini and Varvitsiotis2, Reference Mančinska and Roberson52]. The general notion of a discrete quantum structure also traces its origins to the problem of quantum error correction [Reference Kornell43, Reference Kornell44, Reference Kuperberg and Weaver47, Reference Weaver88]. 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 [Reference Harding, Huynh, Nakamori, Ono, Lawry, Kreinovich and Nguyen33, 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 [Reference Rump78] along the lines of [Reference Kornell43] 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 [Reference Dishkant10]. 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 [Reference Dunn13]. More recently, Titani has formulated a sequent calculus for quantum predicate logic [Reference Titani, Engesser, Gabbay and Lehmann83, 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 [Reference Tokuo84], the Sasaki projection is a primitive logical connective. Furthermore, in the Orthomodular Groupoid Calculus of Fazio, Ledda, Paoli and St. John [Reference Fazio, Ledda, Paoli and St. John14] and the Projective Linear Logic of Lehmann [Reference Lehmann50], 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$
[Reference Tokuo85]. 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)
$\Gamma , \neg \phi , \phi \vdash \psi $
, -
(2)
$\Gamma , \neg \neg \phi \vdash \phi $
, -
(3)
$\Gamma , \phi , \neg \phi \vdash \psi $
, -
(4)
$\Gamma , \phi \vdash \neg \neg \phi $
.
Proof.
Proposition 2.3. The following inference rules are derivable:
Lemma 2.4. The following inference rules are derivable:
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)
$\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)
$\Gamma , \neg \phi , \phi \mathbin {\wedge } \psi \vdash \neg \phi $
and
$\Gamma , \neg \psi , \phi \mathbin {\wedge } \psi \vdash \neg \psi $
, -
(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)
$\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:
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 [Reference Kleene42, sec. 19]. Let
$LK$
be the deductive system
$G1$
given in [Reference Kleene42, 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)
$\phi _1, \ldots , \phi _n \vdash \psi _0$
is derivable in
$SOM + E$
. -
(2)
$\phi _1, \ldots , \phi _n \vdash \psi _0$
is derivable in
$LK$
. -
(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 [Reference Kleene42, theorem 47] [Reference Gentzen19, 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 [Reference Kleene42, 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 $
[Reference Kleene42, 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)
, -
(2)
, -
(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 [Reference Finch15]. 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 [Reference Kalmbach40, 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) If
$\phi \vdash \psi $
and
$\psi \vdash \chi $
are both derivable, then
$\phi \vdash \chi $
is derivable. -
(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 $
:
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 }$
[Reference Finch15], 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) Let
$\phi \mathbin {\vee } \psi $
be an abbreviation for
$\neg (\neg \phi \mathbin {\wedge } \neg \psi )$
. -
(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:
Lemma 4.3. The following inference rule is derivable:
Theorem 4.4. The following inference rule is derivable:
Corollary 4.5. The following inference rules are derivable:
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:
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)
$\Gamma , \phi \mathbin {\wedge } \psi \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $
, -
(2)
$\Gamma , \phi \mathbin {\wedge } \neg \psi \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $
, -
(3)
$\Gamma , \neg \phi \mathbin {\wedge } \psi \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $
, -
(4)
$\Gamma , \neg \phi \mathbin {\wedge } \neg \psi \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $
.
Lemma 4.13. The following inference rule is derivable:
Consequently, the following sequents are derivable:
-
(1)
$\Gamma , (\phi \mathbin {\wedge } \psi ) \mathbin {\vee } (\phi \mathbin {\wedge } \neg \psi ) \vdash \phi \mathbin {\bot \!\!\!\bot } \psi $
, -
(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:
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 [Reference Takeuti, Beltrametti and Fraassen82], and the second is shown to be sound for a variant of Weaver’s semantics [Reference Weaver87]. 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 [Reference Takeuti, Beltrametti and Fraassen82], [Reference Ozawa70, sec. 4.1].
Definition 5.1. We define the single-sorted predicate deductive system
$SOM_{{\mathcal Q}}$
:
-
(1) Its formulas are the first-order formulas whose
-
(a) connectives are
$\mathbin {\wedge }$
,
$\mathbin {\rightarrow }$
, and
$\neg $
; -
(b) quantifiers are
$\forall $
; -
(c) relation symbols are
$=$
and
$\in $
; -
(d) constant symbols are the elements of
$V^{({\mathcal Q})}$
, with no other function symbols.
-
-
(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 [Reference Ozawa70, sec. 4.2], e.g., Takeuti’s interpretation [Reference Takeuti, Beltrametti and Fraassen82]. 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 [Reference Kornell43, definition 2.1], [Reference Podleś and Woronowicz76] 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 [Reference Kornell43, 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 [Reference Kornell44, Appendix A.2], [Reference Weaver88].
A function between quantum sets is formally a kind of binary relation between quantum sets [Reference Kornell43, 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 [Reference Kornell43, 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$
[Reference Kornell43, definition 10.3]. This is not a defect in the definition but rather a basic feature of quantum spaces in noncommutative geometry [Reference Woronowicz89].
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) Its formulas are the nonduplicating first-order formulas whose
-
(a) connectives are
$\mathbin {\wedge }$
,
$\mathbin {\rightarrow }$
, and
$\neg $
; -
(b) quantifiers are
$\forall $
; -
(c) sorts are quantum sets;
-
(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;$
-
(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) 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}$
[Reference Kornell44, sec. 2], [Reference Weaver87] 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 [Reference Kornell43, 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 [Reference Kornell44, 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 [Reference Kornell44, 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 [Reference Kornell44, 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 [Reference Kornell44, 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 [Reference Kornell44, proposition 2.3.3], we calculate that
where the first and fourth equalities follow by [Reference Kornell44, proposition 2.3.3] and the second and third equalities follow by linear algebra [Reference Kornell43, definition 3.8]. It follows by [Reference Kornell44, 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.
A Appendix
Let
$\mathcal H$
be a Hilbert space of any dimension. For each subspace A of
$\mathcal H$
, let
$\overline A$
be the closure of A. For each closed subspace A of
$\mathcal H$
, let
$[A]\colon \mathcal H \to \mathcal H$
be the corresponding orthogonal projection operator.
Proposition A.1. Let A and B be closed subspaces of
$\mathcal H$
. Then,
$A \mathbin {\&} B = \overline {[B]A}$
.
Proof. Let
$\xi \in A$
. We calculate that for all
$\eta \in A^{\perp } \wedge B$
,
$ \langle \eta | [B] \xi \rangle = \langle [B] \eta | \xi \rangle = \langle \eta | \xi \rangle = 0. $
Thus,
$[B]\xi \in (A^{\perp } \wedge B)^{\perp } = A \vee B^{\perp }$
, and moreover,
$[B]\xi \in (A \vee B^{\perp }) \wedge B = A \mathbin {\&} B$
. We conclude that
$[B]A$
is a subspace of
$A \mathbin {\&} B$
, and therefore
$\overline {[B]A} \subseteq A \mathbin {\&} B$
.
Let
$\zeta \in ([B]A)^{\perp }$
. We calculate that for all
$\xi \in A$
,
$ \langle \xi | [B] \zeta \rangle = \langle [B] \xi | \zeta \rangle = 0. $
Thus,
$[B] \zeta \in A^{\perp }$
, and moreover,
$[B]\zeta \in A^{\perp } \wedge B$
. Of course
$(1-[B])\zeta \in B^{\perp }$
, and hence
$\zeta = [B] \zeta + (1-[B]) \zeta \in (A^{\perp } \wedge B) \vee B^{\perp } = ((A \vee B^{\perp }) \wedge B)^{\perp } = (A \mathbin {\&} B)^{\perp }$
. We conclude that
$([B]A)^{\perp } \subseteq (A \mathbin {\&} B)^{\perp }$
, and therefore
$A \mathbin {\&} B = (A\mathbin {\&} B)^{\perp \perp }\subseteq ([B]A)^{\perp \perp } = \overline {[B]A}$
. Altogether, we have that
$A \mathbin {\&} B = \overline {[B]A}$
.
Lemma A.2. For all closed subspaces
$A_1, \ldots , A_n$
, and B of
$\mathcal H$
, we have that
$A_1 \mathbin {\&} \cdots \mathbin {\&} A_n \leq B$
is equivalent to
$[A_n]\cdots [A_1]\mathcal H \subseteq B$
.
Proof. In the case
$n = 0$
, the equivalence holds as a consequence of the convention that
$A_1 \mathbin {\&} \cdots \mathbin {\&} A_n = \mathcal H$
. In the case
$n =1$
, the equivalence holds because
$[A_1]\mathcal H = A_1$
. For the remaining cases, we argue by induction. Let
$n \geq 1$
, and assume that for all closed subspaces
$A_1, \ldots , A_n$
, and B of
$\mathcal H$
, we have that
$A_1 \mathbin {\&} \cdots \mathbin {\&} A_n \leq B$
is equivalent to
$[A_n]\cdots [A_1]\mathcal H \subseteq B$
. Then, for all closed subspaces
$A_1, \ldots , A_n, A_{n+1}$
, and B of
$\mathcal H$
, we reason that
$$ \begin{align*} &A_1 \mathbin{\&} \cdots \mathbin{\&} A_n \mathbin{\&} A_{n+1} \leq B\quad\Longleftrightarrow\quad A_1 \mathbin{\&} \cdots \mathbin{\&} A_n \leq A_{n+1} \mathbin{\rightarrow} B\\ & \quad\Longleftrightarrow\quad[A_n] \cdots [A_1] \mathcal H \subseteq A_{n+1} \mathbin{\rightarrow} B\quad\Longleftrightarrow\quad\overline{[A_n] \cdots [A_1] \mathcal H} \leq A_{n+1} \mathbin{\rightarrow} B\\ & \quad\Longleftrightarrow\quad\overline{[A_n] \cdots [A_1] \mathcal H} \mathbin{\&} A_{n+1} \leq B\quad\Longleftrightarrow\quad\overline{[A_{n+1}] \overline{[A_n] \cdots [A_1] \mathcal H}} \leq B\\ & \quad\Longleftrightarrow\quad\overline{[A_{n+1}] [A_n] \cdots [A_1] \mathcal H} \leq B\quad\Longleftrightarrow\quad[A_{n+1}] [A_n] \cdots [A_1] \mathcal H \subseteq B, \end{align*} $$
where the first and fourth equivalences follow by the adjunction between the Sasaki projection and the Sasaki arrow [Reference Finch15] and the fifth equivalence follows by Proposition A.1. Therefore, by induction on n,
$A_1 \mathbin {\&} \cdots \mathbin {\&} A_n \leq B$
if and only if
$[A_n]\cdots [A_1]\mathcal H \subseteq B$
for all closed subspaces
$A_1, \ldots , A_n$
, and B of
$\mathcal H$
.
Theorem A.3. Let
$A_1, \ldots , A_n$
, and B be closed subspaces of
$\mathcal H$
. Then, the following are equivalent:
-
(1) If a physical system that is modeled by
$\mathcal H$
is prepared in any initial state and the propositions that are modeled by
$A_1, \ldots , A_n$
are measured to be true in that order, then the proposition that is modeled by B is true with probability one. -
(2)
$A_1 \mathbin {\&} \cdots \mathbin {\&} A_n \leq B$
.
Proof. If the physical system is in vector state
$\xi $
and the proposition modeled by A is verified to be true, then after this measurement, the physical system is in vector state
$\xi ' = (\|[A]\xi \|)^{-1} [A] \xi $
. The scalar
$\|[A]\xi \|$
is the square-root of the probability that the proposition modeled by A true in vector state
$\xi $
, and thus it is necessarily nonzero if that proposition can be verified.
Let
$\xi _0$
be the initial vector state of the system. For each
$i \in \{1, \ldots , n\}$
, let
$p_i$
be the probability that the propositions modeled by
$A_1, \ldots , A_i$
can be verified in that order, and let
$\xi _i$
be the vector state of the system after such a verification. By a straightforward inductive argument,
$p_i = \|[A_i] \cdots [A_1] \xi _0\|^2$
and
$\xi _i = p_i^{-1/2}[A_i] \cdots [A_1] \xi _0$
if
$p_i \neq 0$
. In particular,
$p_n = \|[A_n] \cdots [A_1] \xi _0\|^2$
and
$\xi _n = p_n^{-1/2}[A_n] \cdots [A_1] \xi _0$
if
$p_n \neq 0$
. Thus, condition (1) is equivalent to the condition that for each vector state
$\xi _0$
, if
$\|[A_n] \cdots [A_1]\xi _0\|^2 \neq 0$
, then
$\|[A_n] \cdots [A_1]\xi _0\|^{-1} [A_n] \cdots [A_1]\xi _0 \in B$
.
We obtain a sequence of equivalent conditions:
-
• condition (1);
-
• for each unit vector
$\xi _0 \in \mathcal H$
, if
$\|[A_n] \cdots [A_1]\xi _0\|^2 \neq 0$
, then
$$ \begin{align*}\|[A_n] \cdots [A_1]\xi_0\|^{-1} [A_n] \cdots [A_1]\xi_0 \in B;\end{align*} $$
-
• for each unit vector
$\xi _0 \in \mathcal H$
, if
$\|[A_n] \cdots [A_1]\xi _0\|^2 \neq 0$
, then
$[A_n] \cdots [A_1]\xi _0 \in B;$
-
• for each unit vector
$\xi _0 \in \mathcal H$
,
$[A_n] \cdots [A_1]\xi _0 \in B;$
-
•
$[A_n] \cdots [A_1]\mathcal H \subseteq B$
; -
• condition (2).
The last equivalence follows by Lemma A.2. Thus, the theorem is proved.
B Appendix
This appendix addresses readers who are skeptical of the claim that
$SOM$
is a system of natural deduction. Before reading this appendix, such a reader is encouraged to make their own assessment of the essential features of natural deduction and to compare this assessment to the discussion in [Reference Pelletier and Hazen75].
“A fundamental part of natural deduction, and what (according to most writers on the topic) sets it apart from other proof methods, is the notion of a ‘subproof’” [Reference Pelletier and Hazen75, abs.]. A subproof begins with an assumption and has the form of a stand-alone proof in which this assumption plays the same role as other asserted formulas. Previously derived subproofs serve to justify assertions just as previously asserted formulas do. For example, a subproof of
$\psi $
from assumption
$\phi $
justifies the assertion of
$\phi \mathbin {\rightarrow } \psi $
. Similarly, a subproof of
$\psi $
from assumption
$\phi $
and a subproof of
$\psi $
from assumption
$\neg \phi $
together justify the assertion of
$\psi $
; this is the principle of excluded middle.
Natural deduction can be presented in a number of ways, including as a sequent calculus [Reference Pelletier and Hazen75, sec. 4]. Gentzen’s presentation of natural deduction as a sequent calculus [Reference Gentzen20] is much like
$SOM$
. Each assertion in a natural deduction is recorded as a sequent whose consequent is the asserted formula and whose antecedent is the sequence of assumptions that have been made but not discharged. The significance of the weakening rule, which is a rule of Gentzen’s system and which is admissible in
$SOM$
by Proposition 3.1, is that any proof may be a part of any subproof because every valid inference is valid with additional assumptions.
A restrictive conception of natural deduction might exclude sequent calculuses, but even the most restrictive conception must include deductive systems in the style of Fitch [Reference Fitch16]. Fitch modified the notation of Jaśkowski’s natural deduction system [Reference Jaśkowski39], which is contemporary with Gentzen’s first natural deductive systems [Reference Gentzen18] and which is clearly more faithful to deduction as it is practiced by mathematicians. The deductive system
$SOM$
may be presented in the style of Fitch without difficulty. For illustration, the cut rule and the paste rule would be presented as follows:
The greatest departure of
$SOM$
, in this presentation, from the standard system of Fitch is that the reiteration rule is more restricted. Recall that in Fitch’s system a previously asserted formula may be reiterated after any number of additional assumptions have been made. Such a reiteration rule is not sound for orthomodular logic. The paste rule is nothing but a restricted reiteration rule that is sound for orthomodular logic. However, properly considered, the reiteration rule in Fitch’s system is not unrestricted either: no formula can be reiterated after one of its assumptions has been discharged.
Another apparent departure of
$SOM$
from Fitch’s system is that some primitive rules allow an assertion after one or more additional assumptions, e.g., the
$\mathbin {\rightarrow }$
-elimination rule:
This is only an apparent departure from Fitch’s system because the reiteration rule is such a rule. Furthermore, such rules are fully compatible with the author’s conception of natural deduction. Nevertheless, it is possible to adjust the primitive rules of
$SOM$
in such a way as to leave special cases of reiteration as the only primitive rules with this property. It is a short exercise to show that
$SOM$
is equivalent to the sequent calculus given in Figure 4. It too may be presented in the style of Fitch.
Fig. 4 A minor reformulation of
$SOM$
.
In natural language, the primitive rules of this natural deduction system are as follows: After assuming
$\phi $
, you may reiterate any formula of the form
$\phi \mathbin {\wedge } \psi $
,
$\neg \phi $
, or
$\phi \mathbin {\rightarrow } \psi $
. If you have proved
$\phi $
after assuming
$\phi $
and then
$\psi $
and you have proved
$\psi $
after assuming
$\psi $
and then
$\phi $
, then you may infer
$\psi \mathbin {\rightarrow } (\phi \mathbin {\rightarrow } \chi )$
from
$\phi \mathbin {\rightarrow } (\psi \mathbin {\rightarrow } \chi )$
. The other primitive rules are entirely familiar.
C Appendix
In this appendix, as in [Reference Kornell44], we write
$\mathrm {Rel}(\mathcal X_1, \ldots , \mathcal X_n)$
for the complete orthomodular lattice of all binary relations
$\mathcal X_1 \times \cdots \times \mathcal X_n \to \mathbf 1$
, where
$\mathcal X_1, \ldots , \mathcal X_n$
are quantum sets and
$(\mathbf {qRel}, \times , \mathbf 1)$
is the symmetric monoidal category of quantum sets and binary relations. We also write
for the interpretation of nonduplicating formulas and terms as it is defined in [Reference Kornell44].
Lemma C.1. Let
$\mathcal X$
,
$\mathcal Y$
, and
$\mathcal Z$
be quantum sets, let F be a function
$\mathcal X \to \mathcal Y$
, and let R be a binary relation
$\mathcal Y \times \mathcal Z \to \mathbf 1$
. Then,
$$ \begin{align*}& \sup\{P \in \mathrm{Rel} (\mathcal X) \,|\, P \times \top_{\mathcal Z} \leq R \circ (F \times I_{\mathcal Z}) \} = \sup\{Q \in \mathrm{Rel}(\mathcal Y) \,|\, Q \times \top_{\mathcal Z} \leq R\} \circ F. \end{align*} $$
Proof. Let
$S_1 = \sup \{P \in \mathrm {Rel} (\mathcal X) \,|\, P \times \top _{\mathcal Z} \leq R \circ (F \times I_{\mathcal Z}) \}$
, and let
$S_2 = \sup \{Q \in \mathrm {Rel}(\mathcal Y) \,|\, Q \times \top _{\mathcal Z} \leq R\}$
. We are to prove that
$S_1 = S_2 \circ F$
. By the definition of
$S_2$
, we have that
$S_2 \times \top _{\mathcal Z} \leq R$
, and thus we also have that
$(S_2 \circ F) \times \top _{\mathcal Z} = (S_2 \times \top _{\mathcal Z}) \circ (F \times I_{\mathcal Z}) \leq R \circ (F \times I_{\mathcal Z})$
. Therefore,
$S_2 \circ F \leq S_1$
by the definition of
$S_1$
. Similarly, by the definition of
$S_1$
, we have that
$S_1 \times \top _{\mathcal Z} \leq R \circ (F \times I_{\mathcal Z})$
, and thus we also have that
$(S_1 \circ F^{\dagger }) \times \top _{\mathcal Z} = (S_1 \times \top _{\mathcal Z}) \circ (F^{\dagger } \times I_{\mathcal Z}) \leq R \circ (F \times I_{\mathcal Z}) \circ (F^{\dagger } \times I_{\mathcal Z}) = R \circ ((F \circ F^{\dagger }) \times I_{\mathcal Z}) \leq R \circ (I_{\mathcal Y} \times I_{\mathcal Z}) = R$
because
$F \circ F^{\dagger } \leq I_{\mathcal Y}$
by the definition of a function between quantum sets. Hence
$S_1 \circ F^{\dagger } \leq S_2$
by the definition of
$S_2$
. Therefore,
$S_1 = S_1 \circ I_{\mathcal X} \leq S_1 \circ F^{\dagger } \circ F \leq S_2 \circ F$
because
$I_{\mathcal X} \leq F^{\dagger } \circ F$
by the definition of a function between quantum sets. Altogether, we have that
$S_1 = S_2 \circ F$
, as desired.
We make two observations for the next proof: First, [Reference Kornell44, proposition 2.3.3], which relates
to
when the variables of
$\overline x$
all appear in
$\overline x'$
, applies to nonduplicating formulas as well as to primitive formulas. Indeed, a nonduplicating formula is interpreted by first translating it into a primitive formula [Reference Kornell44, sec. 2.7]. Second,
is a function for any term
$t(\overline x)$
by a simple inductive argument that applies [Reference Kornell44, lemma 3.5.3] at each step.
Proposition C.2. Let
$t(x_1, \ldots , x_n)$
be a nonduplicating term, and let
$\phi (y, z_1, \ldots , z_m)$
be a nonduplicating formula. Let
$\mathcal X_1, \ldots , \mathcal X_n$
be the sorts of
$x_1, \ldots , x_n$
, respectively, let
$\mathcal Y$
be the sort of y, and let
$\mathcal Z_1, \ldots , \mathcal Z_m$
be the sorts of
$z_1, \ldots , z_m$
, respectively. Let
$\overline x = (x_1, \ldots , x_n)$
, and let
$\overline z = (z_1, \ldots , z_m)$
; let
$\mathcal X = \mathcal X_1 \times \cdots \times \mathcal X_n$
, and let
$\mathcal Z = \mathcal Z_1 \times \cdots \times \mathcal Z_m$
. Assume that the sort of
$t(x_1, \ldots , x_n)$
is
$\mathcal Y$
and that
$\overline x$
and
$\overline z$
have no variables in common. Then,
Proof. We prove the proposition by induction on the formula
$\phi (y, \overline z)$
for a fixed term
$t(\overline x)$
. The base case, when
$\phi (y, \overline z)$
is an atomic formula, follows from Lemmas 3.5.2 and 3.5.3 of [Reference Kornell44] with Propositions 2.3.3 and 3.1.1 of [Reference Kornell44] serving to handle the expansion and permutation of contexts. The proof consists of tedious bookkeeping that differs only superficially from the bookkeeping for classical predicate logic, and it is omitted.
If
$\phi (y, \overline z)$
is of the form
$\neg \psi (y, \overline z)$
, then we argue that
where the second equality follows by the induction hypothesis and the third equality follows by [Reference Kornell43, theorem B.8]. We argue likewise if
$\phi (y,\overline z)$
is of the form
$\psi _1(y, \overline z) \mathbin {\wedge } \psi _2(y, \overline z)$
, if it is of the form
$\psi _1(y, \overline z) \mathbin {\vee } \psi _2(y, \overline z)$
, or if it is of the form
$\psi _1(y, \overline z) \mathbin {\rightarrow } \psi _2(y, \overline z)$
.
If
$\phi (y, \overline z)$
is of the form
$(\forall z_{m+1})\psi (y, \overline z, z_{m+1})$
for some variable
$z_{m+1}$
of some sort
$\mathcal Z_{m+1}$
, then we argue that
where the second equality follows by the induction hypothesis and the third equality follows by Lemma C.1, which is applied to the function
and the binary relation
. We argue likewise if
$\phi (y, \overline z)$
is of the form
$(\exists z_{m+1})\psi (y, \overline z, z_{m+1})$
.
By induction over the class of all nonduplicating formulas
$\phi (y,\overline z)$
for arbitrary tuples
$\overline z$
, we conclude that the claimed equality holds universally.
Acknowledgements
I thank John Harding for his comments on orthomodular lattices. I also thank Davide Fazio, Antonio Ledda, Francesco Paoli, and Gavin St. John for sharing a preprint of their article with me [Reference Fazio, Ledda, Paoli and St. John14]. I also thank an anonymous referee for a careful reading of the manuscript.
Funding
This work was supported by the AFOSR under MURI grant FA9550-16-1-0082.
Open access
