2.1 Gentzen systems and Gentzen algebraisability

The notion of a Gentzen calculus we consider here is more general than the one developed in [Reference Font16, Definition 1.18 and Sec. 5.6], while it is somewhat closer to the one in [Reference Raftery31]. The same holds for the relation of Gentzen algebraisability, which we view as an instance of the relation of equivalence between (abstract) consequence relations investigated by Blok and Jónsson [Reference Blok and Jónsson5] and Galatos and Tsinakis [Reference Galatos and Ono19]. We will refrain from giving all the formal details, referring the reader to these papers for any undefined concept. This will involve a certain amount of handwaving, in the interests of brevity.

Generally speaking, a (sentential) Gentzen calculus $\mathtt {G}$ (or sequent calculus) is a formal deductive system composed of a collection of inference rules, applying which it is possible to derive sequents from other sequents. A sequent is a pair $(X,Y)$ , often evocatively written with a separator , e.g., , where the structures $X,Y$ are of some specified data-type (e.g., sets, multisets, etc.) of formulas over some fixed sentential language $\mathcal {L}$ . Inference rules are usually distinguished into three kinds:

• • Axiom: a rule with no premises, whose consequent is called an initial sequent.

• • Structural: a rule which acts solely on the form of the structures involved in the sequents (i.e., ignoring the shape of the formulas).

• • Logical: a rule that acts on the shape of formulas (usually by introducing a symbol from $\mathcal {L}$ in the conclusion).

An inference rule is typically presented schematically via a meta-inference rule, where it is understood that each substitution-instance of that scheme is an inference rule in the system $\mathtt {G}$ .

Given a set of sequents $S\cup \{s\}$ , a proof of s from S in $\mathtt {G}$ is a finite rooted labelled tree $\mathcal {D}$ whose nodes are labelled by sequents, such that the root of $\mathcal {D}$ is labelled by s, the sequents labelling each internal node and its children-nodes form an instance of some (meta-)inference rule from $\mathtt {G}$ , and each leaf is labelled by an initial sequent or a member of S. For a Gentzen system $\mathtt {G}$ , there is an associated action-invariant consequence relation $\vdash _{\mathtt {G}}$ in the sense of the general theory by Blok and Jónsson [Reference Blok and Jónsson5] and Galatos and Tsinakis [Reference Galatos and Ono19], often called the derivability relation for $\mathtt {G}$ , such that $S \vdash _{\mathtt {G}} s$ if and only if there is a proof of s from S in $\mathtt {G}$ . A sequent is said to be provable in $\mathtt {G}$ if $\vdash _{\mathtt {G}} s$ , i.e., there is a proof of s from the empty set in $\mathtt {G}$ .

Let $\mathbb {K}$ be a class of algebras in the same language $\mathcal {L}$ . The equational consequence relation for $\mathbb {K}$ is the relation $\models _{\mathbb {K}}$ such that for every set of $\mathcal {L}$ -equations $E\cup \{ \varphi \approx \psi \}$ , $E\models _{\mathbb {K}} \varphi \approx \psi $ if and only if for every algebra $\mathbf {A}\in \mathbb {K}$ and every valuation h on $\mathbf {A}$ , i.e., any homomorphism from the algebra of $\mathcal {L}$ -formulas to $\mathbf {A}$ , if $h(\gamma )=h(\delta )$ for every $ \gamma \approx \delta \in E$ then $h(\varphi )=h(\psi )$ .

In essence, a Gentzen system $\mathtt {G}$ is said to be algebraisable if there exists a class of algebras $\mathbb {K}$ for which the derivability relation of $\mathtt {G}$ and the equational consequence relation for $\mathbb {K}$ are Blok–Jónsson equivalent, in which case $\mathbb {K}$ is called an equivalent algebraic semantics for $\mathtt {G}$ (an equivalent variety semantics, if $\mathbb {K}$ is a variety). More precisely, and following the conventions of Raftery [Reference Raftery31] (as opposed to [Reference Font16]), $\mathtt {G}$ is algebraisable, with an equivalent algebraic semantics $\mathbb {K}$ , if there exists a pair of transformers $(\tau,\rho)$ , both commuting with substitutions, such that for any set of sequents $S\cup \{s\}$ and for all $\mathcal {L}$ -formulas $\varphi ,\psi $ :

2.2 Non-associative substructural logics

As explained in the introduction, in this paper we want to recast orthomodular quantum logic as a non-associative substructural logic. The study of these logics is not unprecedented. Less deviant forms of non-associative substructural logics—with two residuals and a monotonic order—have been considered in the literature. An exhaustive list would be long, but let us mention at least [Reference Cintula, Horčík and Noguera11, Reference Galatos, Jipsen, Kowalski and Ono18] and papers in the tradition of Lambek calculus [Reference Buszkowski8, Reference Metcalfe, Paoli, Tsinakis, Hosni and Montagna27]. Further information on substructural logics and residuated structures can be found in [Reference Fazio, Ledda and Paoli17, Reference Kornell26].

The sequent calculus $\mathtt {GL}$ , as developed by Galatos and Ono [Reference Galatos, Jipsen, Kowalski and Ono18], can be seen as the basis for substructural logics lacking associativity of the fusion connective and of its structural counterpart, comma. The system $\mathtt {GL}$ is essentially obtained by relaxing from the full Lambek calculus $\mathtt {FL}$ the data-type of the structures within the sequents from lists to binary trees.

We recall that a pointed residuated unital -groupoid is an algebra $(G,\land ,\vee ,\cdot ,\backslash ,/,0,1)$ that has a lattice reduct $(G,\land ,\vee )$ , a unital groupoid reduct $(G,\cdot ,1)$ , and further satisfies the residuation law: for all $a,b,c\in G$ ,

$$ \begin{align*} b\leq a \backslash c \iff a\cdot b\leq c \iff a\leq c/b, \end{align*} $$

where $\leq $ is the induced lattice-order, with no assumptions placed upon the constant $0$ . The residuation quasiequations can be replaced by appropriate equations, hence pointed residuated unital -groupoids form a variety $\mathbb {PRG}$ . Just as axiomatic extensions of $\mathtt {FL}$ correspond to subvarieties of pointed residuated lattices, axiomatic extensions of $\mathtt {GL}$ correspond to subvarieties of residuated lattice-ordered groupoids; more precisely, the variety of pointed residuated unital -groupoids is an equivalent algebraic semantics for $\mathtt {GL}$ .

2.3 Orthomodular lattices and orthomodular quantum logic

Orthomodular lattices are the algebras at the centre of the standard Birkhoff–von Neumann approach to quantum logic (for a readable survey of their algebraic theory, see [Reference Bruns, Harding, Coecke, Moore and Wilce7]). In this framework, quantum events (or properties) are mathematically represented by projection operators on a complex separable Hilbert space. If $\mathcal {H}$ is a Hilbert space and $\Pi (\mathcal {H})$ is the set of all projection operators on $\mathcal {H}$ , the structure

$$ \begin{align*} (\Pi(\mathcal{H}),{\land},{\vee},{'},0,1), \end{align*} $$

where $0$ (respectively, $1$ ) is the projection onto the one-element (respectively, total) subspace, $(P_X)'$ is the projection onto the subspace $X^\bot $ orthogonal to X, $P_X\land P_Y = P_{X\cap Y}$ , and $P_X\vee P_Y = P_{(X\cup Y)^{\bot \bot }}$ , is a canonical example of an orthomodular lattice, a structure defined below.

An ortholattice is an algebra $\mathbf {L}=(L,\land ,\vee ,{'},0,1)$ , where the reduct $(L,\land ,\vee ,0,1)$ is a bounded lattice, with $0$ ( $1$ ) the least (greatest) element, and for which the unary operation $'$ is an ortho-complementation, namely an antitone involution such that the identity $x\land x'\approx 0$ holds in $\mathbf {L}$ . An ortholattice $\mathbf {L}$ is an orthomodular lattice if it satisfies the orthomodular law:

$$ \begin{align*} x\leq y \implies y \approx(y\land x')\vee x, \end{align*} $$

where $\leq $ is the induced lattice-order, or equivalently the identity $x\vee ((x\vee y)\land x')\approx x\vee y$ . The class of orthomodular lattices thus forms a variety, denoted by $\mathbb {OML}$ . Of particular interest for this work are the following term operations which may be defined in any ortholattice:

$$ \begin{align*} \begin{array}{r c l l} x \cdot y &:=& (x\vee y')\land y & \mbox{(Sasaki product),}\\ y/x &:=& (y \land x) \vee x' & \mbox{(Sasaki hook),}\\ x + y &:=& (x \land y') \vee y & \mbox{(Sasaki sum)}. \end{array} \end{align*} $$

We note that, in general, the Sasaki product and sum are neither associative nor commutative in ortho(modular) lattices.

A certain relation on orthomodular lattices, the commuting relation, is of crucial importance for this paper. Given an orthomodular lattice $\mathbf {L}$ and $a,b\in L$ , a is said to commute with b in case $(a\wedge b)\vee (a^{\prime }\wedge b)=b$ . We flag some known facts about the commuting relation that will be put to good use hereafter (items (3) and (4) are known as Kröger’s Lemma [Reference Beran3, Theorem 6.1] and the Gudder–Schelp Theorem [Reference Beran2, Reference Goldblatt21], respectively).

The next celebrated result is one of the most useful tools for practitioners of the field:

Two different logics can be, and have indeed been, associated with $\mathbb {OML}$ : its $1$ -assertional logic $\mathrm {L}_{\mathbb {OML}}^{1}$ (see e.g., [Reference Czelakowski14, Reference Humberstone24]) and its logic of order $\mathrm {L}_{\mathbb {OML}}^{\leq }$ (see e.g., [Reference Dalla Chiara, Giuntini and Greechie15, Reference Galatos and Tsinakis20, Reference Hardegree23]).

In full, $\mathrm {L}_{\mathbb {OML}}^{1}$ is the logic in the language of $\mathbb {OML}$ whose consequence relation is defined as follows for any set of formulas $\Gamma \cup \left \{ \varphi \right \}$ :

$$ \begin{align*} \Gamma\vdash_{\mathrm{L}_{\mathbb{OML}}^{1}}\varphi \text{ iff }\left\{ \gamma \approx1:\gamma \in\Gamma\right\} \models_{\mathbb{OML}} \varphi \approx1. \end{align*} $$

This logic is regularly algebraisable with $\mathbb {OML}$ as equivalent algebraic semantics. The logic $\mathrm {L}_{\mathbb {OML}}^{\leq }$ has the same language but its consequence relation is defined as follows for any finite set of formulas $\Gamma \cup \left \{ \varphi \right \}$ :

$$ \begin{align*} \Gamma\vdash_{\mathrm{L}_{\mathbb{OML}}^{\leq}}\varphi \text{ iff } & \text{for any }\mathbf{A}\in\mathbb{OML}\text{, any } b\in A \text{ and any valuation } h \text{ to } \mathbf{A} \text{,}\\ & \text{if }b\leq h(\gamma) \text{ for all } \gamma\in\Gamma\text{, then }b\leq h(\varphi) \text{.} \end{align*} $$

This logic is slightly less well-behaved from the point of view of AAL, although it fits in a number of frameworks that have been intensively studied (logics of order, selfextensional logics with conjunction, semilattice-based logics with an algebraisable assertional companion: see [Reference Font16, Sec. 7.2]). From general facts in these theories we can deduce that it is protoalgebraic but not even equivalential, let alone algebraisable, and yet that the class of algebra reducts of its reduced matrix models is again $\mathbb {OML}$ .

The existing calculi for “orthomodular quantum logic”(Nishimura [Reference Moot, Retoré, Moot and Retoré28] or Cutland and Gibbins [Reference Cutland and Gibbins13]) can be considered, in a weak sense, as proof systems for either of these logics. Indeed, a sequent $\Gamma \Rightarrow \varphi $ , where $\Gamma $ is a finite set of formulas, is a theorem of Nishimura’s calculus just in case $\Gamma \vdash _{\mathrm {L}_{\mathbb {OML}}^{\leq }}\varphi $ ; on the other hand $\Rightarrow \varphi $ is derivable from the set $\{ \Rightarrow \gamma : \gamma \in \Gamma \}$ just in case $\Gamma \vdash _{\mathrm {L}_{\mathbb {OML}}^{1}}\varphi $ (and similar reflections hold for the calculus by Cutland and Gibbins). In a stronger sense, however, they might just as well be proof systems for neither, since none of such calculi has been proved to be Gentzen algebraisable with $\mathbb {OML}$ as equivalent algebraic semantics.

2.4 Pointed left-residuated -groupoids

In light of the left residuation property observed in orthomodular groupoids, a theory of left-residuated lattice-ordered groupoids has been developed [Reference Paoli30] with the aim of placing the theory of substructural logics and quantum logics within a common framework. A pointed left-residuated -groupoid is an algebra $\mathbf {L} = (L,\land ,\vee ,\cdot ,/,0,1)$ that has a lattice reduct $(L,\land ,\vee )$ , a groupoid reduct $(L,\cdot ,1)$ with a left-unit $1$ , and furthermore satsifies the left-residuation law Footnote ¹ : for all $a,b,c\in L$ ,

$$ \begin{align*} a\cdot b \leq c \iff a\leq c/b, \end{align*} $$

where $\leq $ is the induced lattice-order.

In [Reference Paoli30] it is shown that the class of all pointed left-residuated -groupoids forms a variety, denoted by $\mathbb {PLRG}$ . As with pointed residuated -groupoids, $0$ is an arbitrary constant for which no assumptions are placed. However, we will make use of the term-defined operation $\varphi ':=0/\varphi $ , where $\varphi $ is any formula in the language of pointed left-residuated -groupoids.Footnote ² We caution the reader that, in general, this operation is neither involutive nor antitone in $\mathbb {PLRG}$ .

An orthomodular groupoid is a pointed left-residuated -groupoid that satisfies the following identities:

$$ \begin{align*} \begin{array}{r l} x''\approx x &\mbox{(involutive)}, \\ (x\vee y)'\leq x' & \mbox{(antitone)},\\ x\cdot(x\vee y)\approx x& \mbox{(strongly idempotent)},\\ x\cdot y \approx (x \vee y')\land y&\mbox{(Sasakian)}, \\ x/y\approx(x\land y)\vee y' &(/\mbox{-Sasakian}). \\ \end{array} \end{align*} $$

As is such, the class of orthomodular groupoids forms a variety, denoted by $\mathbb {OG}$ . In [Reference Chajda and Länger9], it is shown that orthomodular groupoids are term equivalent to orthomodular lattices. The proposition below shows that many of the above identities can be equivalently replaced by the identity (strongly involutive): $y/x \approx (y'\cdot x)' $ .

Remark 4. The following quasi-identities do not generally hold in $\mathbb {OG}$ :

$$ \begin{align*} \begin{array}{r c l} x\leq w ~\&~ y\leq z &\implies& x\cdot y \leq w\cdot z,\\ x\leq w ~\&~y\leq z& \implies& (y/w)\cdot x\leq z. \end{array} \end{align*} $$

The above remark draws a stark contrast in $\mathbb {PLRG}$ with $\mathbb {PRG}$ , whose groupoid operation $\cdot $ is isotone in both its coordinates, and therefore the two quasi-identities above are satisfied.

3.1 The morphology of the calculus

Essentially following [Reference Galatos, Jipsen, Kowalski and Ono18], we first specify in detail the morphological structure of the calculus we are going to present.

Let $\mathcal {L}$ be the language $(2,2,2,2,0,0)$ with connectives $\land ,\lor ,\cdot ,/,0,1$ , and let $\mathbf {Fm}_{\mathcal {L}}$ be the formula $\mathcal {L}$ -algebra with countably many generators in ${Var}_{\mathcal {L}}$ . Let us denote by $\textit {Fm}_{\mathcal {L}}^{\sim }$ the set $\{\varphi ^{\sim }:\varphi \in {\textit {Fm}_{\mathcal {L}}}\}$ and consider $\textit {Fm}_{\mathcal {L}}^{\delta }={\textit {Fm}_{\mathcal {L}}}\cup \textit {Fm}_{\mathcal {L}}^{\sim }$ . We refer by $\mathbf {G}(\textit {Fm}_{\mathcal {L}}^{\delta })=(G(\textit {Fm}_{\mathcal {L}}^{\delta }),\circ ,\epsilon )$ to the unital groupoid freely generated by $\textit {Fm}_{\mathcal {L}}^{\delta }\cup \{\epsilon \}$ , where $\epsilon $ is a new constant.

Now, consider a new symbol $\_$ . The set $G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }$ is defined inductively as follows:

• • $\_\in G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }$ and

• • $a\in G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }$ and $x\in G(\textit {Fm}_{\mathcal {L}}^{\delta })$ entail that $a\circ x,x\circ a\in G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }$ .

Given $u\in G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }$ and $x\in G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }\cup G(\textit {Fm}_{\mathcal {L}}^{\delta })$ , we will denote by $u[x]$ the word obtained by replacing the (unique!) occurrence of $\_$ in u by x. For example, if $u=(a\circ (b\circ \_))$ , $v=(a\circ \_)$ , and $x=(a\circ b)$ , then $u[v]=(a\circ (b\circ (a\circ \_)))$ and $u[x]=(a\circ (b\circ (a\circ b)))$ . To make the operation more explicit we allow ourselves to denote $u[x]$ by $u\star x$ . The elements of $G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }$ are called G-contexts or simply contexts.

A sequent is any pair in $G(\textit {Fm}_{\mathcal {L}}^{\delta })\times G(\textit {Fm}_{\mathcal {L}}^{\delta })$ . Following the customary conventions, we will denote any sequent $(X,Y)$ by . The set of all such sequents is denoted by $\mathrm {Seq}(\mathcal {L})$ .

The calculi that follow will have infinitely many rules of inference organized in meta-inference rules, or (metarules). In order to formally define metarules, we need three pairwise disjoint sets of meta-variables: A (of sort $S_{A}$ ), G (of sort $S_{G}$ with $S_{A}\subseteq S_{G}$ ) and U (of sort $S_{U}$ ). In our system, we will have $A={\textit {Fm}_{\mathcal {L}}}(F)$ , where F is a set of propositional variables distinct from ${Var}_{\mathcal {L}}$ above. A meta-Sasaki word will be any term of type $S_{G}$ built up by means of the following operations: $^{\sim }:S_{A}\rightarrow S_{G}$ , $\circ :S_{G}\times S_{G}\rightarrow S_{G}$ , $\star :S_{U}\times S_{G}\rightarrow S_{G}$ , and the constant $\epsilon $ of sort $S_{G}$ . For any $u,X$ of type $S_{U}$ resp. $S_{G}$ , we set $u\star X=u[X]$ . A meta-sequent $(X,Y)$ is any pair such that X and Y are meta-Sasaki words. Meta-rules are pairs $(S,s)$ such that $S\cup \{s\}$ is a set of meta-sequents. An inference rule is said to be an instance of a metarule, if all metavariables from A, G and U are instantiated to elements of ${\textit {Fm}_{\mathcal {L}}}$ , $G(\textit {Fm}_{\mathcal {L}}^{\delta })$ and $G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }$ , respectively, metasequent operators $\epsilon $ , $\circ $ and $\star $ are replaced by the corresponding sequent operators, and for any instance $\varphi $ of a metavariable $\alpha \in A$ , $\alpha ^{\sim }$ is mapped to $\varphi ^{\sim }\in \textit {Fm}_{\mathcal {L}}^{\sim }$ .

For each formula $\varphi \in \textit {Fm}_{\mathcal {L}}$ , by $\varphi '$ we abbreviate the formula $0/\varphi $ . We define inductively the following maps $\left(\cdot\right)^{\delta }:G\left(\textit {Fm}_{\mathcal {L}}^{\delta }\right)\rightarrow G\left(\textit {Fm}_{\mathcal {L}}^{\delta }\right)$ , $\left(\cdot \right)^{\Pi }:G\left(\textit {Fm}_{\mathcal {L}}^{\delta }\right)\rightarrow {\textit {Fm}_{\mathcal {L}}}$ and $\left(\cdot \right)^{\Sigma }:G\left(\textit {Fm}_{\mathcal {L}}^{\delta }\right)\rightarrow {\textit {Fm}_{\mathcal {L}}}$ :

$$ \begin{align*} \begin{array}{c|c|c|c} \epsilon^{\delta}=\epsilon & \varphi^{\delta}=\varphi^{\sim} & \left( \varphi^{\sim }\right) ^{\delta}=\varphi & \left( X\circ Y\right) ^{\delta}=X^{\delta }\circ Y^{\delta} ,\\ \epsilon^{\Pi}=1 & \varphi^{\Pi}=\varphi & \left( \varphi^{\sim}\right) ^{\Pi}=\varphi^{\prime} & \left( X\circ Y\right) ^{\Pi}=X^{\Pi}\cdot Y^{\Pi} ,\\ \epsilon^{\Sigma}=0 & \varphi^{\Sigma}=\varphi & \left( \varphi^{\sim}\right) ^{\Sigma}=\varphi^{\prime} & \left( X\circ Y\right) ^{\Sigma}=\left( \left( X^{\Sigma}\right) ^{\prime}\cdot\left( Y^{\Sigma}\right) ^{\prime}\right) ^{\prime}. \\ \end{array} \end{align*} $$

3.2 The calculus and its heuristic explanation

The inference rules for the calculus $\mathtt {OGC}$ are given in Figure 1, where we use $X\Leftrightarrow Y$ as an abbreviation for the conjunction of sequents and , respectively called the $\Rightarrow $ - and $\Leftarrow $ -sequent,Footnote ³ and the double horizontal lines in $\delta $ to indicate that it is a bidirectional rule. While the letters $\alpha , \beta , \ldots $ can be instantiated only by members of $\textit {Fm}_{\mathcal {L}}$ , the letters $a,b, \ldots $ can be instantiated by any members of $\textit {Fm}_{\mathcal {L}}^\delta $ .

Fig. 1 The calculus $\mathtt {OGC}$ .

In the interest of allowing the reader to intuitively digest the inference rules presented, a discussion about the intended (algebraic) interpretation is in order. As will be seen in Section 4, the intended interpretation of a sequent will be the inequality $X^\Pi \leq Y^\Sigma $ , i.e., the intended meaning of is $\leq $ , structures X to the left of represent (Sasaki) products while structures Y on the right are (Sasaki) sums. With this interpretation in mind, we can now elucidate and motivate our choice of presentation.

On the one hand, this interpretation makes the genesis of the rule $\delta $ clear: in an orthomodular lattice $\mathbf {A}$ we have the following residuation law(s) relating the Sasaki operations with the lattice order:

$$ \begin{align*}x\cdot z \leq y \iff x\leq y/z \approx y + z' \end{align*} $$

for all $x,y,z \in A$ . Similarly, the conditional exchange rules and , where active structures in the right-hand premiss can be swapped if the left-hand premiss is also available, corresponds to the demand that the algebraic interpretations of a and X commute (see Lemma 1(5)); i.e., for all $a,x\in A$

$$ \begin{align*}a\cdot x \leq a \iff a \mbox{ commutes with }x \iff x \mbox{ commutes with }a \iff x\cdot a \leq x,\end{align*} $$

or in other words, a commutes with x if and only if $a\cdot x = a\land x = x\cdot a$ .

On the other hand, the interpretation also illuminates the peculiarities of the remaining structural and operational rules based mainly around Remark 4; namely the failure of the Sasaki operations to preserve (or in the case of hook, reverse) order in the right-coordinate. This immediately explains, for example, the particular left-associated versions of familiar inferences rules like the weakening rule $(\mathrm{w}) $ as well as those rules for the lattice connectives $\land $ and $\vee $ . Furthermore, this motivates the appearance of $\Leftrightarrow $ , whose intended interpretation corresponds to $\approx $ , in the rules $(\cdot{\mathrm{r}}) $ , , and , which mirror the fact that in $\mathbb {OG}$ (or even $\mathbb {PLRG}$ ) only the following quasi-identities generally hold:

(1) $$ \begin{align} \begin{array}{r c l} x\leq a ~\&~ y\approx b &\implies& x\cdot y \leq a\cdot b,\\ x\approx a ~\&~b\leq z& \implies& (b/a)\cdot x\leq z. \end{array} \end{align} $$

Clearly, the $3$ -premiss rules $(\cdot{\mathrm{r}}) $ and violate the subformula property, since e.g., the formula $Y^{\Pi }$ disappears in the conclusion of $(\cdot{\mathrm{r}}) $ . However, the search space of all possible premisses of applications of both rules is always finite.

It is worth noting that need for $\Leftrightarrow $ in the cut-rule, for example, can be alleviated with a related, but syntactically different, version of this calculus. Namely, let $\mathtt {OGC}^\prime $ be the calculus obtained from: replacing the binary operation $/$ with a unary operation ${}^\prime $ in $\mathcal {L}$ ; replacing the rule by [see Lemma 13]; and replacing and $(/{\mathrm{r}}) $ by $(\prime{\mathrm{l}}) $ and [see below Lemma 7]. Due to the generic nature of $(\prime{\mathrm{l}}) $ and , it is not difficult to prove the following claims [see Section 4.2]:

• • $\mathtt {OGC}^\prime $ satisfies .

• • $\mathtt {OGC}^\prime $ satisfies the rules and $(/{\mathrm{r}}) $ , where $\varphi / \psi := (\varphi ' \cdot \psi )'$ .

In fact, following an almost identical argument as seen in Section 4, one can show that $\mathtt {OGC}^\prime $ is algebraisable with a variety of algebras in the signature $\langle \land , \vee , \cdot , {}^\prime , 0 ,1\rangle $ that is term-equivalent to $\mathbb {OG}$ .

However, ridding entirely the appearance of $\Leftrightarrow $ does not seem possible, as it is necessary for proving completeness [see Lemma 17], for instance, with the (Sasaki) product operation. It is for this reason, as well as our intention of providing a syntactic calculus for orthomodular groupoids, that we use this particular presentation.

3.3 Elementary properties of $\mathtt {OGC}$

For the sake of readability, in what follows we will write $x^{uv}$ as an abbreviation for $(x^u)^v$ , where $u,v\in \{\prime ,\sim ,\delta ,\Pi ,\Sigma \}$ and x is a (meta-) variable of the proper sort. Also, given a G-context u, we inductively define the G-context $u^\delta $ as follows: $\_^\delta =\_$ ; $(v\circ w)^\delta = v^\delta \circ w^\delta $ for $v,w\in G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }\cup G(\textit {Fm}_{\mathcal {L}}^{\delta })$ . Hence, $u[X]^\delta = u^\delta [X^\delta ]$ for any structure X.

Also, for the sake of readability, some $\mathtt {OGC}$ -derivations contain informal uses of rules not proper to the calculus; e.g.,

where $[=]$ means syntactically equal, while $[\star ]$ is shorthand for the sub-derivation in $\mathtt {OGC}$ resulting from some lemma, derived rule, or assumption $\star $ .

In light of the above lemma, we will freely use the fact that $X^{\delta \delta }=X$ without reference, and we will abuse notation and write $\delta $ to represent .

Proof. Observe:

The second claim follows from $(\mathrm{id}) $ for $a\in \textit {Fm}_{\mathcal {L}}$ , and also the above for $a\in \textit {Fm}_{\mathcal {L}}^\sim $ .

Lemma 7. $\vdash _{\mathtt {OGC}} \varphi ^\sim \Leftrightarrow \varphi '$ and $\vdash _{\mathtt {OGC}} \varphi \Leftrightarrow \varphi ''$ . Furthermore,

Proof. Recall $\varphi ':=0/\varphi $ . First, we observe [ $\star $ ]:

and [ $\star '$ ]:

Hence [ $\star _1$ ]: $\vdash _{\mathtt {OGC}} \varphi ^\sim \Leftrightarrow \varphi '$ by [ $\star $ ] and that fact that

is an instance of $(\mathrm{id}) $ since $\varphi ^{\sim \Pi }=\varphi '$ by definition of the operator $\Pi $ . For [ $\star _2$ ]: $\vdash _{\mathtt {OGC}} \varphi \Leftrightarrow \varphi ''$ , observe:

Thus, for either $\{a,b \}=\{\varphi ',\varphi ^\sim \}$ or $\{a,b \}=\{\varphi ,\varphi ''\}$ , we have $[\star _3]:\vdash _{\mathtt {OGC}} a\Leftrightarrow b$ and hence:

Whence

and

. Lastly, we observe:

As a consequence of the lemma above, the following rules are derivable in $\mathtt {OGC}$ , for any $\varphi \in \textit {Fm}_{\mathcal {L}}$ , $X,Y\in G(\textit {Fm}_{\mathcal {L}}^{\delta })$ , and $u\in G(\textit {Fm}_{\mathcal {L}}^{\delta })^{\alpha }$ :

Proof. We proceed by induction on the construction of X. For $X=\epsilon $ , then the $\vdash $ -direction is the rule

, while the $\dashv $ -direction is derived below:

For $X=\varphi $ , then $X=X^\Pi $ and there is nothing to prove. For $X=\varphi ^\sim $ , then $X^\Pi =\varphi '$ , and the result follows from Lemma 7.

For the inductive step, assume the claim (IH) holds for words of complexity strictly less than that of X, and suppose $X=Z\circ V$ . For the $\vdash $ -direction, observe:

And for the $\dashv $ -direction:

Proof. For fixed $X\in G(\textit {Fm}_{\mathcal {L}}^{\delta })$ , call the second claim $(\star _X)$ . Clearly, if the first claim holds for X then $(\star _X)$ follows by the derivations below:

We now prove the first claim by induction on the complexity of X. Let $X=\epsilon $ . By the definitions of the operators, clearly ${\epsilon ^{\delta \Pi \sim }}={\epsilon ^{\Pi \sim }}=1^\sim $ , while $\epsilon ^\Sigma =0$ . Below we observe the derivation for the

-sequent on the left and the $\Leftarrow $ -sequent on the right:

For $X=\varphi $ , observe ${\varphi ^{\delta \Pi \sim }}={(\varphi ^\sim )^{\Pi \sim }}=(\varphi ')^\sim $ and $\varphi ^\Sigma =\varphi $ . Hence the claim follows by Lemma 7. Similarly for $X=\varphi ^\sim $ , we have ${(\varphi ^\sim )^{\delta \Pi \sim }}={\varphi ^{\Pi \sim }}=\varphi ^{\sim }$ while $(\varphi ^\sim )^\Sigma =\varphi '$ , and again the claim follows from Lemma 7.

For the inductive step, assume the claim holds for structures of complexity strictly less than that of X, and suppose $X=Z\circ V$ . In particular, the inductive hypothesis implies that both $(\star _Z)$ and $(\star _V)$ hold. By definition, we have

$$ \begin{align*} {(Z\circ V)^{\delta\Pi\sim}} = {(Z^\delta\circ V^\delta)^{\Pi\sim}} = (Z^{\delta\Pi}\cdot V^{\delta\Pi})^\sim \quad\mbox{and}\quad (Z\circ V)^\Sigma = ({Z^\Sigma}'\cdot {V^{\Sigma}}')' .\end{align*} $$

Below we derive the

-sequent on the left and the $\Leftarrow $ -sequent on the right:

Proof. Below we derive the $\vdash $ -direction on the top and the $\dashv $ -direction on the bottom:

By Lemmas 8 and 10, we obtain the following.

The derivable structural rules in the next lemma express, against the backdrop of the informal reading suggested for sequents of the form $a \circ b \Rightarrow a$ (Section 3.2), some of the algebraic properties of the commuting relations pinned down in Lemma 1(1) and (2).

Lemma 12. The following inference rules are derivable in $\mathtt {OGC}:$

Proof. Below, we establish

on the left and

on the right:

Now, the rules

and

are proven similarly to

. Lastly, below we derive

on the left and using it with

we derive

on the right:

Lemma 13. The following inference rules are derivable in $\mathtt {OGC}:$

Proof. For

, let $\alpha =a^\Pi $ . Observe:

where $(R)=(R')=[=]$ if $a\in \textit {Fm}_{\mathcal {L}}$ , otherwise

and $(R')=(\prime{\mathrm{l}}) $ when ${a\in \textit {Fm}_{\mathcal {L}}^\delta}$ . As for

, observe:

Lemma 14. The following rules are derivable in $\mathtt {OGC}:$

Proof. For

, we observe:

Now,

is derived by applying $(\mathrm{w}) $ on its right premise and then applying

.

4.1 $\mathtt {OGC}$ and $\mathbb {OG}$

Recall, to show that $\mathtt {OGC}$ is algebraisable with equivalent variety semantics given by $\mathbb {OG}$ , it is enough to find transformers $\tau :\mathrm {Seq}(\mathcal {L})\to \wp (\textit {Fm}_{\mathcal {L}}^2)$ and $\rho :\textit {Fm}_{\mathcal {L}}^2\to \wp (\mathrm {Seq}(\mathcal {L}))$ both commuting with substitutions, such that, for all $S\cup \{s\}\subseteq \mathrm {Seq}(\mathcal {L})$ and for all $\mathcal {L}$ -formulas $\varphi ,\psi $ :

• • $S \vdash _{\mathtt {OGC}} s$ iff $\tau [S]\models _{\mathbb {OG}} \tau (s)$ and

• • .

We will see that the appropriate transformers are defined as follows, for all $X,Y\in G(\textit {Fm}_{\mathcal {L}}^\delta )$ and $\varphi ,\psi \in \textit {Fm}_{\mathcal {L}}$ :

Clearly, $\tau $ and $\rho $ commute with substitutions.

Proof. We observe,

However, this is obvious given the reflexivity and antisymmetry of the induced order of the lattice reduct in $\mathbb {OG}$ .

Proof. Let s denote the sequent . That is, we must prove

$$ \begin{align*} S \vdash_{\mathtt{OGC}} s \quad\mbox{implies} \quad \tau[S] \models_{\mathbb{OG}} X^\Pi\leq Y^\Sigma. \end{align*} $$

A customary induction on the length of the $\mathtt {OGC}$ -proof of from S will suffice. If is an axiom, then it is either $(\mathrm{id}) $ , , or ; and it is immediate to observe that the translations of these axioms make instances of the identity $x\leq x$ , valid in all $\mathbf {A}\in \mathbb {OG}$ . If $s\in S$ , our claim is trivial. The other rules can be checked with some occasional help from Lemma 1 and Theorem 2. For the sake of illustration, we exemplify the inductive step through the rule $(\cdot{\mathrm{r}}) $ . Suppose has been derived from S in $\mathtt {OGC}$ via a final application of $(\cdot{\mathrm{r}}) $ to the premises , , and . By the inductive hypothesis, we have that

$$ \begin{align*} \begin{array}{rcl} \tau[S] &\models_{\mathbb{OG}}& X^\Pi \leq \alpha, \\ \tau[S] &\models_{\mathbb{OG}}& Y^\Pi\leq \beta, \\ \tau[S] &\models_{\mathbb{OG}}& \beta\leq Y^\Pi. \end{array} \end{align*} $$

Note that, by the last two consequences, we obtain $\tau [S]\models _{\mathbb {OG}} Y^\Pi \approx \beta $ . Now, let $\mathbf {A}\in \mathbb {OG}$ and h be a valuation to $\mathbf {A}$ , and suppose that $\tau [S]\subseteq \ker (h)$ . Hence $h(Y^\Pi )=h(\beta )$ , and so by Equation (1),

$$ \begin{align*} h\left((X\circ Y)^\Pi \right) =h(X^\Pi)\cdot h(Y^\Pi) =h(X^\Pi)\cdot h(\beta)\leq h(\alpha)\cdot h(\beta) =h\left((\alpha\cdot \beta)^\Sigma \right), \end{align*} $$

whence our conclusion follows.

Proof. Suppose contrapositively that $S \not \vdash _{\mathtt {OGC}} s$ , where s is the sequent . We require the Lindenbaum algebra construction, so let ${T}$ be the $\xi $ -theory generated by S, where $\xi $ is the closure operator associated with $\vdash _{\mathtt {OGC}}$ . Define, for all $\varphi ,\psi \in \textit {Fm}_{\mathcal {L}}$ :

$$ \begin{align*} \langle\varphi,\psi\rangle \in \operatorname{\mathrm{\Theta}}_{T} \iff \rho(\varphi\approx \psi)\subseteq {T}. \end{align*} $$

We need an algebra $\mathbf {A}\in \mathbb {OG}$ and a valuation h to $\mathbf {A}$ such that $\tau [S]\subseteq \ker (h)$ , while . Unsurprisingly enough, we choose $\mathbf {A}=\mathbf {Fm}_{\mathcal {L}}/\operatorname {\mathrm {\Theta }}_{T}$ , and h as the valuation uniquely determined by the condition $h(x)=x/\operatorname {\mathrm {\Theta }}_{T}$ . For our choice to be viable, we must verify the following two assertions:

1. (1) $\operatorname {\mathrm {\Theta }}_{T}$ is a congruence on $\mathbf {Fm}_{\mathcal {L}}$ and

2. (2) The quotient $\mathbf {Fm}_{\mathcal {L}}/\operatorname {\mathrm {\Theta }}_{T}$ belongs to $\mathbb {OG}$ .

For (1), $\operatorname {\mathrm {\Theta }}_{T}$ is clearly reflexive, symmetric, and transitive by $(\mathrm{id}) $ and

. Thus we need only show compatibility with product, implication, meet, and join, i.e., $\varphi \operatorname {\mathrm {\Theta }}_{T} \psi $ and $\chi \operatorname {\mathrm {\Theta }}_{T} \upsilon $ implies $(\varphi \star \chi )\operatorname {\mathrm {\Theta }}_{T} (\psi \star \upsilon )$ for each $\star \in \{\cdot ,/,\land ,\vee \}$ . By definition of $\operatorname {\mathrm {\Theta }}_{T}$ and $\rho $ , we must therefore show $\varphi \Leftrightarrow \psi , \chi \Leftrightarrow \upsilon \in {T}$ implies $(\varphi \star \chi )\Leftrightarrow (\psi \star \upsilon )\in {T}$ , where we abuse the notation $x\Leftrightarrow y\in {T}$ to mean $\rho (x\approx y)\subseteq {T}$ . It suffices to show

, since the $\Leftarrow $ -sequent is obtained by a symmetric derivation. Below we catalogue the derivations for each $\star \in \{\cdot ,/,\land ,\vee \}$ :

The derivation for $\vee $ is similar to that for $\land $ . Hence $\operatorname {\mathrm {\Theta }}_{T}$ is a congruence.

For (2), observe that $\varphi /\operatorname {\mathrm {\Theta }}_{T} \leq ^{\mathbf {A}} \psi /\operatorname {\mathrm {\Theta }}_{T}$ iff $\varphi \Leftrightarrow \varphi \land \psi \in {T}$ iff . We base on this observation the verification that $\mathbf {A}$ belongs to $\mathbb {OG}$ .

First we show that $\mathbf {A}\in \mathbb {PLRG}$ . As the derivations for verifying $\mathbf {A}$ has a lattice reduct as well as a multiplicative (left-)unit are standard, we only show the defining inequations for residuation (see [Reference Paoli30]):

So $\mathbf {A}\in \mathbb {PLRG}$ . Hence, by Proposition 3, it is enough to show that $\mathbf {A}$ is strongly idempotent and strongly involutive. For strong idempotency, observe:

For strong involutivity, observe:

Hence $\operatorname {\mathrm {\Theta }}_{T}$ and $\mathbf {A}$ are as claimed, and so we need only verify $\tau [S]\subseteq \ker (h)$ but

, written in full:

Now, by Corollary 11,

iff

. Since ${T}=\xi (S)$ , it follows that $\tau [S]\subseteq \ker (h)$ , while

since $S\not \vdash _{\mathtt {OGC}} s$ . Therefore

.

Therefore, by Lemmas 15–17 we conclude:

4.2 The alternative calculus $\mathtt {OGC}'$

As it has been already mentioned above, in $\mathbb {OG}$ the identity $x/y\approx (x'\cdot y)'$ holds. Therefore, orthomodular groupoids can be equivalently regarded as algebras in the signature $\{\land ,\lor ,\cdot ,',0,1\}$ , which are unital lattice-ordered groupoids with an antitone involution satisfying further conditions. Indeed, it can be shown that once $\mathtt {OGC}$ is formulated into the alternative calculus $\mathtt {OGC}'$ [see Section 3.2] by assuming as a primitive connective $'$ , and replacing and $(/{\mathrm{r}}) $ by

then the resulting calculus can be still shown to be algebraisable with respect to orthomodular groupoids in the new signature (by means of the same $\tau $ and $\rho $ ). Moreover, $\mathtt {OGC}^\prime $ seems to behave better proof-theoretically. First of all, it can be shown that and $(/{\mathrm{r}}) $ can be derived without making use of . In fact we have

as well as

Secondly, it can be shown that can be replaced by . To see this, we first prove the following lemmas.

Proof. We proceed by induction on X. If $X=\epsilon $ , then follows by means of a simple application of $(\mathrm{id}) $ . If $X=\varphi ^{\sim }$ , one has:

Finally, if $X=Y\circ Z$ , then one has by induction hypothesis that as well as . Therefore one has:

Proof. Assuming we derive by Lemma 13. Conversely, by Lemma 20, we have . Therefore, we have:

Indeed, the above results show that, in presence of and $(\prime{\mathrm{l}}) $ , we do not need to assume in its full generality. In fact the same results follows by replacing by the simple cut: