The logic induced by effect algebras

Effect algebras were introduced by D. Foulis and M. K. Bennett (Foulis and Bennett 1994; see also Bennett and Foulis 1995 and Botur and Halaš 2009) as an algebraic axiomatization of the logic of quantum mechanics. For enabling deductions and derivations in this logic, it is necessary to introduce the connective implication. It is worth noticing that for lattice effect algebras this task was solved in a different way in Chajda et al. (2017). The problem is that though the binary operation of an effect algebra is only partial, implication should be defined everywhere. If the considered effect algebra is lattice-ordered, then implication is usually defined by \(x\rightarrow y:=x'+(x\wedge y)\) and called Sasaki implication, see e.g., Borzooei et al. (2018), Chajda and Länger (2019), Foulis and Pulmannová (2012) and Rad et al. (2019). Properties of this implication were described in these papers, and a certain axiomatization of the corresponding logic in Gentzen style (see e.g., Blok and Pigozzi 1989) was derived in Rad et al. (2019). However, non-lattice-ordered effect algebras are more important than lattice-ordered ones. As shown in Chajda et al. (2009), any effect algebra can be completed to a basic algebra which is total. For commutative basic algebras, a Gentzen system was presented in Botur and Halaš (2009) and for basic algebras in Chajda (2015). This motivates us to find such an axiomatization also for not necessarily lattice-ordered effect algebras.

Another reason for introducing implication in effect algebras is to show that this connective is related to conjunction via (left) adjointness, and hence effect algebras can be considered as left residuated structures; see Chajda and Länger (2019), Chajda and Länger (submitted).

We should not direct the attention of the reader to the quantum logic aspect only but also to psychology, etc. (see Aerts 2009). The reason is that the logic of finite effect algebras cannot completely cover quantum mechanics, but it can help in other areas.

For concepts and results concerning effect algebras, the reader is referred to the monograph by Dvurečenskij and Pulmannová (2000). The following definition and lemma are taken from Dvurečenskij and Pulmannová (2000).

For lattice effect algebras \((E,+,{}',0,1)\), the Sasaki implication (called also material implication in Blok and Pigozzi (1989)) was introduced as follows:for all \(x,y\in E\). For our sake, we will consider this in the following way:for all \(x,y\in E\) and call this kind of implication natural implication. Note that the natural implication of x and y coincides with the Sasaki implication of \(y'\) and \(x'\). The reason for this choice is that it turns out that some computations become more feasible with this natural implication than with the Sasaki one.

In the rest of our paper, the implication investigated in lattice effect algebras will be the natural one.

Concerning the reduct restricted to \(\rightarrow \) and \(\vee \), we can prove the following.

Summarizing the above properties, we can introduce an alter ego of a lattice effect algebra, i.e., its implication version.

In order to show the correspondence between a lattice effect algebra and the implication version, we state and prove the following three theorems.

By a propositional language, we understand some set \({\mathcal {L}}\) of propositional connectives. The arity of a propositional connective \(c\in {\mathcal {L}}\) is called the rank of c. The \({\mathcal {L}}\)-formulas are built in the usual way from the propositional variables using the connectives of \({\mathcal {L}}\). We denote the set of all \({\mathcal {L}}\)-formulas by \({\mathcal {F}}m_{{\mathcal {L}}}\) or \({\mathcal {F}}m\) in brief when the language \({\mathcal {L}}\) is clear from the context.

By a logic in \({\mathcal {L}}\), we mean a standard deductive system over \({\mathcal {L}}\) or, equivalently, its consequence relation \(\vdash _{{\mathcal {L}}}\) (see Blok and Pigozzi 1989 for details). We shall use the notation \(\vdash \) whenever there is no danger of confusion.

Let us mention that a system of axioms and rules for the propositional logic induced by lattice effect algebras was already presented in Rad et al. (2019). However, that system is rather complicated because it consists of five axioms and ten derivation rules. In what follows, we present another system having only three axioms and five rules. Moreover, three of these rules, namely Modus Ponens, Suffixing and Weak Prefixing, are common in many propositional calculi.

By the propositional logic \(L_{\mathrm{LEA}}\) in a language \({\mathcal {L}}=\{\rightarrow ,0\}\) (\(\rightarrow \) is of rank 2, 0 is of rank 0), we understand a consequence relation \(\vdash _{\mathrm{LEA}}\) (or \(\vdash \), in brief) satisfying the axioms and the rules where \(\lnot \varphi :=\varphi \rightarrow 0\) and \(1:=\lnot 0=0\rightarrow 0\).

The axiom system (A1)–(A3) with the derivation rules (MP)–(R2) will be referred to as axiom system \({\mathbf {A}}\).

As usual, for \(\Gamma \cup \{\varphi ,\psi \}\subseteq {\mathcal {F}}m\), the biconditional \(\Gamma \vdash \varphi \leftrightarrow \psi \) is an abbreviation for \(\Gamma \vdash \varphi \rightarrow \psi \) and \(\Gamma \vdash \psi \rightarrow \varphi \).

In order to show that the system \({\mathbf {A}}\) is really an axiom system in Gentzen style for lattice effect algebras, we prove the following important properties.

For a class \({\mathcal {K}}\) of \({\mathcal {L}}\)-algebras over a language \({\mathcal {L}}\), consider the relation \(\models _{\mathcal {K}}\) that holds between a set \(\Sigma \) of identities and a single identity \(\varphi \approx \psi \) if every interpretation of \(\varphi \approx \psi \) in a member of \({\mathcal {K}}\) holds provided each identity in \(\Sigma \) holds under the same interpretation. In this case, we say that \(\varphi \approx \psi \) is a \({\mathcal {K}}\)-consequence of \(\Sigma \). The relation \(\models _{\mathcal {K}}\) is called the semantic equational consequence relation determined by \({\mathcal {K}}\).

Given a deductive system \(({\mathcal {L}},\vdash _L)\) over a language \({\mathcal {L}}\), a class \({\mathcal {K}}\) of \({\mathcal {L}}\)-algebras is called an algebraic semantics for \(({\mathcal {L}},\vdash _L)\) if \(\vdash _L\) can be interpreted in \(\models _{\mathcal {K}}\) in the following sense: There exists a finite system \(\delta _i(p)\approx \varepsilon _i(p)\), (\(\delta (\varphi )\approx \varepsilon (\varphi )\), in brief) of identities with a single variable p such that for all \(\Gamma \cup \{\varphi \}\subseteq {\mathcal {F}}m\),Then, \(\delta _i\approx \varepsilon _i\) are called defining identities for \(({\mathcal {L}},\vdash _L)\) and \({\mathcal {K}}\).

\({\mathcal {K}}\) is said to be equivalent to \(({\mathcal {L}},\vdash _L)\) if there exists a finite system \(\Delta (p,q)\) of formulas with two variables p, q such that for every identity \(\varphi \approx \psi \),where \(\varphi \Delta \psi \) means just \(\Delta (\varphi ,\psi )\) and is an abbreviation for the conjunction \(\Gamma \models _{\mathcal {K}}\Delta \) and \(\Delta \models _{\mathcal {K}}\Gamma \).

According to Rasiowa (1974) and Rasiowa and Sikorski (1970), a standard system of implicative extensional propositional calculus (SIC, for short) is a deductive system \(({\mathcal {L}},\vdash _L)\) satisfying the following conditions:As one can immediately see, the system \(({\mathcal {L}},\vdash _{\mathrm{LEA}})\) fulfils all the properties of SIC. Indeed, there is no unary connective in our language, and we have the only binary connective \(\rightarrow \). Now, the first property is (c) of Theorem 3.1, the second is (MP) and the third is (a) from Theorem 3.1. To show the fifth property, we have \(\varphi \rightarrow \psi \vdash (\psi \rightarrow \chi )\rightarrow (\phi \rightarrow \chi )\) by (Sf), and \(\chi \rightarrow \lambda ,\lambda \rightarrow \chi \vdash (\psi \rightarrow \chi )\rightarrow (\psi \rightarrow \lambda )\) by (WPf). The rest then follows again by (a) of Theorem 3.1.

Moreover, taking \(\varepsilon (p)=p\), \(\delta (p)=p\rightarrow p\) and \(\Delta (p,q)=\{p\rightarrow q,q\rightarrow p\}\), it is known (see Blok and Pigozzi 1989) that every SIC has an equivalent algebraic semantics with the defining identity \(\delta \approx \varepsilon \) and with the set \(\Delta \) as an equivalence system. As a consequence, we obtain

In order to show that LEA is an equivalent algebraic semantics for \(({\mathcal {L}},\vdash _{\mathrm{LEA}})\), we use the following statement (see Blok and Pigozzi 1989, Theorem 2.17).

Taking into account that \(\vdash \varphi \rightarrow \varphi \) in \(({\mathcal {L}},\vdash _{\mathrm{LEA}})\), we have \(p\rightarrow p\approx 1\), i.e., \(\varepsilon (p)=1\). Applying the previous proposition, we are going to prove the following.

We conclude that, using the equivalence between lattice effect algebras and lattice effect implication algebras and Theorem 4.3, system \({\mathbf {A}}\) is an algebraic axiomatization of the logic of lattice effect algebras.

Although lattice effect algebras are more feasible for some kinds of algebraic investigation, effect algebras which need not be lattice-ordered play a more important role in algebraic axiomatization of the logic of quantum mechanics. Hence, it is a question if also in this case we are able to derive some semantics, axioms and rules for a Gentzen-type axiomatization in a way similar to that for lattice-ordered effect algebras.

The first question is how to define the connective implication in not lattice-ordered effect algebras. In this section, we show that this can be done successfully in the case when the effect algebra \((E,+,{}',0)\) in question is finite, or, more generally, if for every \(x,y\in E\) there exist maximal elements in the lower cone \(L(x',y')\).

In the following, let \({\mathbf {E}}=(E,+,{}',0,1)\) be an effect algebra with induced order \(\le \) such that \((E,\le )\) satisfies the ascending chain condition (shortly, ACC). This condition says that in \((E,\le )\) there do not exist infinite ascending chains. Hence, if \((E,\le )\) satisfies the ACC, then every non-empty subset of E has at least one maximal element. In particular, this is true in case of finite E.

Now, let \(a,b\in E\) and \(A,B\subseteq E\). Here and in the following,Moreover, we defineSince \((E,\le )\) satisfies the ACC, we have \(x\rightarrow y\ne \emptyset \) for all \(x,y\in E\). Moreover, if \({\mathbf {E}}\) is a lattice effect algebra, then the definition of \(\rightarrow \) coincides with the original natural implication \(\rightarrow \) since thenfor all \(x,y\in E\).

Since every element of \(\text {Max}L(x',y')\) is less than or equal to \(y'\), \(y+\text {Max}L(x',y')\) is defined for each \(x,y\in E\). It is worth noticing that now \(x\rightarrow y\) need not be a single element of E, but a non-void subset of E. Hence, one cannot expect that such an implication will satisfy the same properties as the implication in lattice effect algebras. On the other hand, it was already successfully used by the first and third author in Chajda and Länger (submitted) in order to show that for the implication defined in this way the effect algebra in question can be organized in an operator residuated structure.

Although not all the conditions of Theorems 2.1 and 2.2 are valid for effect algebras which need not be lattice-ordered, we still can prove several characteristic properties.

Summarizing all what was stated for implication in effect algebras, we can introduce the following concept.

Of course, every finite effect implication algebra satisfies trivially the last condition of Definition 5.2.

We are going to show that every effect algebra satisfying the ACC induces an effect implication algebra and vice versa.

Although \(x\rightarrow y\) need not be a single element of the corresponding effect algebra \({\mathbf {E}}\), we are able to prove that an effect implication algebra can be converted into an effect algebra where the partial operation \(+\) is defined in the standard way.

The following theorem shows that the correspondence between an effect algebra satisfying the ACC and its corresponding effect implication algebra is almost one-to-one.

Theorem 5.5 (i) says that every effect algebra satisfying the ACC is fully determined by its derived effect implication algebra. This enables us to set up the semantics and axiomatization for finite effect algebras which need not be lattice-ordered in a way similar to that for lattice effect algebras.

In this section, we use the same general theory taken from Blok and Pigozzi (1989) as in Sects. 3 and 4. Hence, we need not repeat all what was said in the beginning of these two sections. All what was described in Propositions 4.1 and 4.2 remains valid also here with the same equivalence system.

By the propositional logic \(L_{\mathrm{EA}}\) in a language \({\mathcal {L}}=\{\rightarrow ,0\}\) (\(\rightarrow \) is of rank 2, 0 is of rank 0), we understand a consequence relation \(\vdash _{\mathrm{EA}}\) (or \(\vdash \), in brief) satisfying the axioms and the rules where \(\lnot \varphi :=\varphi \rightarrow 0\) and \(1:=\lnot 0=0\rightarrow 0\).

This axiom system will be referred to as system \({\mathbf {B}}\). We can prove the following consequences of \({\mathbf {B}}\).

In what follows, we show that this algebraic semantics is just that for algebras satisfying conditions (i)–(viii) of Definition 5.2, i.e., for finite effect implication algebras. Similar to the lattice case, the system \(({\mathcal {L}},\vdash _{\mathrm{EA}})\) fulfills the properties of SIC. Again, applying Proposition 4.2, we are going to show the following theorem:

Due to the correspondence described in Theorem 5.5, our propositional logic \(L_{\mathrm{EA}}\), i.e., system \({\mathbf {B}}\), is an algebraic axiomatization in Gentzen style of the logic of finite effect algebras which need not be lattice-ordered. A possible extension to effect algebras satisfying ACC could make problems since the last condition of Definition 5.2 (mentioned after condition (viii)) equivalent to ACC cannot be easily described in our logic \(L_{\mathrm{EA}}\).