An alternative proof of the Hilbert-style axiomatization for the $\{\wedge ,\vee \}$-fragment of classical propositional logic

Abstract

Dyrda and Prucnal gave a Hilbert-style axiomatization for the $\{\wedge ,\vee \}$-fragment of classical propositional logic. Their proof of completeness follows a different approach to the standard one proving the completeness of classical propositional logic. In this note, we present an alternative proof of Dyrda and Prucnal’s result following the standard arguments which prove the completeness of classical propositional logic.

1 Introduction

It is well-known that classical propositional logic $\mathcal {CL}$ can be presented syntactically in several ways, among them a Hilbert-style calculus. Let us denote the resulting syntactic consequence by $\vdash _{\mathcal {CL}}$. The standard completeness theorem for classical logic is the statement that for all $\varGamma \cup \{\varphi \}\subseteq \mathbf{Fm}$,

$$\begin{aligned} \varGamma \vdash _{\mathcal {CL}}\varphi \iff \varGamma \vDash _{{\mathbf {2}}}\varphi , \end{aligned}$$

where ${\mathbf {2}}$ is the two-element Boolean algebra. The standard completeness proof is as follows. The implication $\Rightarrow$, the soundness theorem, is proved by what is normally qualified as routine checking. On the other hand, the implication $\Leftarrow$ is proved by contraposition. One assumes that $\varGamma \nvdash _{\mathcal {CL}}\varphi$. Then, by the Lindenbaum’s Lemma there exists a maximally consistent theory $\varDelta$ such that $\varGamma \subseteq \varDelta$ and $\varphi \notin \varDelta$. Now, one defines the function $h:\mathbf{Fm} \rightarrow {\mathbf {2}}$ by putting, for any $\alpha \in \mathbf{Fm}$, $h\alpha =1$ if and only if $\alpha \in \varDelta$. Next, using several properties of maximally consistent theories, one shows that h is actually a homomorphism. Thus, this homomorphism is such that $h(\varGamma )\subseteq \{1\}$ and $h\varphi \ne 1$. Hence, it follows that $\varGamma \nvDash _{{\mathbf {2}}}\varphi$.

The $\{\wedge ,\vee \}$-fragment of classical propositional logic is defined by the matrix $\langle {\mathbf {2}},\{1\}\rangle$, where ${\mathbf {2}}=\langle \{0,1\},\wedge ,\vee \rangle$ is the two-element distributive lattice. This fragment was studied by different authors, for instance [2, 4, 5, 7]. In [2] Dyrda and Prucnal presented a Hilbert-style axiomatization for the $\{\wedge ,\vee \}$-fragment of classical logic. The argument used to prove this completeness result does not follow the classical arguments used in the standard completeness theorem of classical logic with respect to some of its equivalent Hilbert-style axiomatizations.

We will try to explain shortly the arguments given in [2] by Dyrda and Prucnal to prove the completeness theorem. Let $\vdash _{\mathrm {DP}}$ be the syntactic consequence defined by the Hilbert-style calculus proposed in [2]. The implication $\varGamma \vDash _{{\mathbf {2}}}\varphi \implies \varGamma \vdash _{\mathrm {DP}}\varphi$ is proved by contraposition. It is assumed that $\varGamma \nvdash _{\mathrm {DP}}\varphi$. Thus, they show that there is a finite set U of formulas built from the variables appearing in $\varphi$ and the connective $\vee$ such that $\varphi \vdash _{\mathrm {DP}}\chi \iff U\vdash _{\mathrm {DP}}\chi$, for all $\chi \in \mathbf{Fm}$. So, there is $\alpha \in U$ such that $\varGamma \nvdash _{\mathrm {DP}}\alpha$. It is also proved that there is a set $U_1$ of formulas built from variables and $\vee$ such that $\varGamma \vdash _{\mathrm {DP}}\chi \iff U_1\vdash _{\mathrm {DP}}\chi$, for all formula $\chi$. Then, there exists a set $Y_1$ of variables such that $Y_1\nvdash _{\mathrm {DP}}\alpha$ and $Y_1\vdash _{\mathrm {DP}}\gamma$, for all $\gamma \in \varGamma$. Now they define the map $v:\mathrm {Var}\rightarrow \{0,1\}$ as follows: $v(p)=1\iff p\in Y_1$. Let ${\widehat{v}}:\mathbf{Fm} \rightarrow {\mathbf {2}}$ be the homomorphism extending the map v. Then, it is verified that ${\widehat{v}}(\varGamma )\subseteq \{1\}$ and ${\widehat{v}}(\varphi )\ne 1$. Hence, $\varGamma \nvDash _{{\mathbf {2}}}\varphi$. We refer the reader to [2] for the details missing.

Our aim is to present a proof of the completeness between the $\{\wedge ,\vee \}$-fragment of classical logic and the Hilbert-style presentation given in [2] following the usual arguments which prove the standard completeness of classical logic defined by the matrix $\langle {\mathbf {2}},\{1\}\rangle$ and some of its Hilbert-style axiomatizations.

2 The Hilbert-style axiomatization and completeness for the $\{\wedge ,\vee \}$-fragment of classical logic

In this note we follow the usual concepts and notations of algebraic logic. Our main reference for algebraic logic is [3].

Let ${\mathcal {L}}=\{\wedge ,\vee \}$ be an algebraic language of type (2, 2), and $\mathbf{Fm}$ the algebra of formulas over this language and a denumerable set of variables. The $\{\wedge ,\vee \}$-fragment of classical propositional logic, denoted by ${\mathcal {S}}_{\wedge ,\vee }=\langle \mathbf{Fm} ,\vDash _{{\mathbf {2}}}\rangle$, is defined by: for all $\varGamma ,\{\varphi \}\subseteq \mathbf{Fm}$,

$$\begin{aligned} \varGamma \vDash _{{\mathbf {2}}}\varphi \iff \forall h\in \mathrm {Hom}(\mathbf{Fm} ,{\mathbf {2}}), \ h(\varGamma )\subseteq \{1\} \ \text { implies } \ h(\varphi )=1. \end{aligned}$$

Now we introduce the Hilbert-style presentation given by Dyrda and Prucnal in [2]. Let ${\mathcal {S}}_{\mathrm {DP}}=\langle \mathbf{Fm} ,\vdash _{\mathrm {DP}}\rangle$ be the propositional logic defined in the usual “Hilbert-style” with no axioms and with the following rules of inference:

• (R1) $\varphi \wedge \psi \vdash \varphi$

• (R2) $\varphi \wedge \psi \vdash \psi \wedge \varphi$

• (R3) $\varphi ,\psi \vdash \varphi \wedge \psi$

• (R4) $\varphi \vdash \varphi \vee \psi$

• (R5) $\varphi \vee \psi \vdash \psi \vee \varphi$

• (R6) $\varphi \vee (\varphi \vee \psi )\vdash \varphi \vee \psi$

• (R7) $\varphi \vee (\psi \vee \chi )\vdash (\varphi \vee \psi )\vee \chi$

• (R8) $(\varphi \vee \psi )\vee \chi \vdash \varphi \vee (\psi \vee \chi )$

• (R9) $\varphi \vee (\psi \wedge \chi )\vdash (\varphi \vee \psi )\wedge (\varphi \vee \chi )$

• (R10) $(\varphi \vee \psi )\wedge (\varphi \vee \chi )\vdash \varphi \vee (\psi \wedge \chi )$

• (R11) $\varphi \wedge (\psi \vee \chi )\vdash (\varphi \wedge \psi )\vee (\varphi \wedge \chi )$

• (R12) $\varphi \vee \varphi \vdash \varphi$

It is known that rules (R6), (R8) and (R11) are derivable from the others, see [1, 4].

Our aim is to show that the logics ${\mathcal {S}}_{\wedge ,\vee }$ and ${\mathcal {S}}_{\mathrm {DP}}$ coincide following the standard arguments proving that the classical logic, defined by some Hilbert-style presentation, is complete with respect to the matrix $\langle {\mathbf {2}},\{1\}\rangle$ (see for instance [3, pp. 72–73]). To this end, we need to prove that the logic ${\mathcal {S}}_{\mathrm {DP}}$ satisfies the Proof by Cases Principle (see Proposition 2.3). First we need the following property of the logic ${\mathcal {S}}_{\mathrm {DP}}=\langle \mathbf{Fm} ,\vdash _{\mathrm {DP}}\rangle$.

Proposition 2.1

Let $\varphi ,\psi ,\chi \in \mathbf{Fm}$. If $\varphi \vdash _{\mathrm {DP}}\psi$, then $\varphi \vee \chi \vdash _{\mathrm {DP}}\psi \vee \chi$.

Proof

Assume $\varphi \vdash _{\mathrm {DP}}\psi$. In order to prove that $\psi \vee \chi$ is derivable from $\varphi \vee \chi$, it is sufficient to show that $\{\gamma \vee \chi : \gamma \in \varGamma \}\vdash _{\mathrm {DP}}\alpha \vee \chi$ for each rule of inference $\varGamma \vdash \alpha$ defining ${\mathcal {S}}_{\mathrm {DP}}$.

(R1’) $(\alpha \wedge \beta )\vee \chi \vdash _{\mathrm {DP}}\alpha \vee \chi$:

$\begin{array}{lll} 1. &{} (\alpha \wedge \beta )\vee \chi &{} (Hyp)\\ 2. &{} (\chi \vee \alpha )\wedge (\chi \vee \beta ) &{} 1., (R5), (R9)\\ 3. &{} \alpha \vee \chi &{} 2., (R1), (R5) \end{array}$

(R2’) $(\alpha \wedge \beta )\vee \chi \vdash _{\mathrm {DP}}(\beta \wedge \alpha )\vee \chi$:

$\begin{array}{lll} 1. &{} (\alpha \wedge \beta )\vee \chi &{} (Hyp)\\ 2. &{} (\chi \vee \alpha )\wedge (\chi \vee \beta ) &{} 1., (R5), (R9)\\ 3. &{} \chi \vee \alpha &{} 2., (R1)\\ 4. &{} \chi \vee \beta &{} 2., (R2), (R1)\\ 5. &{} (\chi \vee \beta )\wedge (\chi \vee \alpha ) &{} 4., 3., (R3)\\ 6. &{} (\beta \wedge \alpha )\vee \chi &{} 5., (R10), (R5) \end{array}$

(R3’) $\alpha \vee \chi ,\beta \vee \chi \vdash _{\mathrm {DP}}(\alpha \wedge \beta )\vee \chi$:

$\begin{array}{lll} 1. &{} \alpha \vee \chi , \beta \vee \chi &{} (Hyp)\\ 2. &{} \chi \vee \alpha , \chi \vee \beta &{} 1., (R5)\\ 3. &{} (\chi \vee \alpha )\wedge (\chi \vee \beta ) &{} 2., (R3)\\ 4. &{} (\alpha \wedge \beta )\vee \chi &{} 3., (R10), (R5) \end{array}$

(R4’) $\alpha \vee \chi \vdash _{\mathrm {DP}}(\alpha \vee \beta )\vee \chi$:

$\begin{array}{lll} 1. &{} \alpha \vee \chi &{} (Hyp)\\ 2. &{} (\chi \vee \alpha )\vee \beta &{} 1., (R5), (R4)\\ 3. &{} (\alpha \vee \beta )\vee \chi &{} 2., (R8), (R5) \end{array}$

(Aux1) $\alpha \vee (\beta \vee \alpha )\vdash _{\mathrm {DP}}\beta \vee \alpha$:

$\begin{array}{lll} 1. &{} \alpha \vee (\beta \vee \alpha ) &{} (Hyp)\\ 2. &{} \alpha \vee (\alpha \vee \beta ) &{} 1., (R7), (R5)\\ 3. &{} \beta \vee \alpha &{}2., (R6), (R5) \end{array}$

(R5’) $(\alpha \vee \beta )\vee \chi \vdash _{\mathrm {DP}}(\beta \vee \alpha )\vee \chi$:

$\begin{array}{lll} 1. &{} (\alpha \vee \beta )\vee \chi &{} (Hyp)\\ 2. &{} ((\alpha \vee \beta )\vee \alpha )\vee \chi &{} 1., {(R4')}\\ 3. &{} \alpha \vee (\beta \vee (\alpha \vee \chi )) &{} 2., (R8), (R8)\\ 4. &{} (\alpha \vee \chi )\vee (\beta \vee (\alpha \vee \chi )) &{} 3. (R4')\\ 5. &{} \beta \vee (\alpha \vee \chi ) &{} 4., (Aux1)\\ 6. &{} (\beta \vee \alpha )\vee \chi &{} 5., (R7) \end{array}$

(R7’) $(\alpha \vee (\beta \vee \gamma ))\vee \chi \vdash _{\mathrm {DP}}((\alpha \vee \beta )\vee \gamma )\vee \chi$:

$\begin{array}{lll} 1. &{} (\alpha \vee (\beta \vee \gamma ))\vee \chi &{} (Hyp)\\ 2. &{} \alpha \vee ((\beta \vee \gamma )\vee \chi ) &{} 1.,(R8)\\ 3. &{} (\alpha \vee \beta )\vee ((\beta \vee \gamma )\vee \chi ) &{} 2., (R4')\\ 4. &{} \chi \vee ((\alpha \vee \beta )\vee (\beta \vee \gamma )) &{} 3., (R7), (R5)\\ 5. &{} (\chi \vee (\alpha \vee \beta ))\vee (\beta \vee \gamma ) &{} 4., (R7)\\ 6. &{} (\beta \vee \gamma )\vee (\chi \vee (\alpha \vee \beta )) &{} 5., (R5)\\ 7. &{} (\gamma \vee \beta )\vee (\chi \vee (\alpha \vee \beta )) &{} 6., (R5')\\ 8. &{} (\chi \vee (\alpha \vee \beta ))\vee (\gamma \vee \beta ) &{} 7., (R5)\\ 9. &{} \beta \vee ((\chi \vee (\alpha \vee \beta ))\vee \gamma ) &{} 8., (R7), (R5)\\ 10. &{} (\beta \vee \alpha )\vee ((\chi \vee (\alpha \vee \beta ))\vee \gamma ) &{} 9., (R4')\\ 11. &{} (\alpha \vee \beta )\vee ((\chi \vee (\alpha \vee \beta ))\vee \gamma ) &{} 10., (R5')\\ 12. &{} ((\alpha \vee \beta )\vee \chi )\vee ((\chi \vee (\alpha \vee \beta ))\vee \gamma ) &{} 11., (R4')\\ 13. &{} (\chi \vee (\alpha \vee \beta ))\vee ((\chi \vee (\alpha \vee \beta ))\vee \gamma ) &{} 12., (R5')\\ 14. &{} (\chi \vee (\alpha \vee \beta ))\vee \gamma &{} 13., (R6)\\ 15. &{} ((\alpha \vee \beta )\vee \gamma )\vee \chi &{} 14., (R8), (R5)\\ \end{array}$

(R9’) $(\alpha \vee (\beta \wedge \gamma ))\vee \chi \vdash _{\mathrm {DP}}((\alpha \vee \beta )\wedge (\alpha \vee \gamma ))\vee \chi$:

$\begin{array}{lll} 1. &{} (\alpha \vee (\beta \wedge \gamma ))\vee \chi &{} (Hyp)\\ 2. &{} (\chi \vee \alpha )\vee (\beta \wedge \gamma ) &{} 1., (R5), (R7)\\ 3. &{} ((\chi \vee \alpha )\vee \beta )\wedge ((\chi \vee \alpha )\vee \gamma ) &{} 2., (R9)\\ 4. &{} (\chi \vee \alpha )\vee \beta &{} 3., (R1)\\ 5. &{} (\chi \vee \alpha )\vee \gamma &{} 3., (R5), (R1)\\ 6. &{} \chi \vee (\alpha \vee \beta ) &{} 4., (R8)\\ 7. &{} \chi \vee (\alpha \vee \gamma ) &{} 5., (R8)\\ 8. &{} (\chi \vee (\alpha \vee \beta ))\wedge (\chi \vee (\alpha \vee \gamma )) &{} 6., 7., (R3)\\ 9. &{} \chi \vee ((\alpha \vee \beta )\wedge (\alpha \vee \gamma )) &{} 8., (R10)\\ 10. &{} ((\alpha \vee \beta )\wedge (\alpha \vee \gamma ))\vee \chi &{} 9., (R5) \end{array}$

(R10’) $((\alpha \vee \beta )\wedge (\alpha \vee \gamma ))\vee \chi \vdash _{\mathrm {DP}}(\alpha \vee (\beta \wedge \gamma ))\vee \chi$:

$\begin{array}{lll} 1. &{}((\alpha \vee \beta )\wedge (\alpha \vee \gamma ))\vee \chi &{} (Hyp)\\ 2. &{} (\chi \vee (\alpha \vee \beta ))\wedge (\chi \vee (\alpha \vee \gamma )) &{} 1., (R5), (R9)\\ 3. &{} \chi \vee (\alpha \vee \beta ) &{} 2., (R1)\\ 4. &{} \chi \vee (\alpha \vee \gamma ) &{} 2., (R2), (R1)\\ 5. &{} (\chi \vee \alpha )\vee \beta &{} 3., (R7)\\ 6. &{} (\chi \vee \alpha )\vee \gamma &{} 4., (R7)\\ 7. &{} ((\chi \vee \alpha )\vee \beta )\wedge ((\chi \vee \alpha )\vee \gamma ) &{} 5., 6., (R3)\\ 8. &{} (\chi \vee \alpha )\vee (\beta \wedge \gamma ) &{} 7., (R10)\\ 9. &{} (\alpha \vee (\beta \wedge \gamma ))\vee \chi &{} 8., (R8), (R5) \end{array}$

(R12’) $(\alpha \vee \alpha )\vee \chi \vdash _{\mathrm {DP}}\alpha \vee \chi$:

$\begin{array}{lll} 1. &{} (\alpha \vee \alpha )\vee \chi &{} (Hyp)\\ 2. &{} \alpha \vee (\alpha \vee \chi ) &{} 1., (R8)\\ 3. &{} \alpha \vee \chi &{} 2., (R6) \end{array}$ $\square$

Corollary 2.2

Let $\varGamma \cup \{\varphi ,\chi \}\subseteq \mathbf{Fm}$. If $\varGamma \vdash _{\mathrm {DP}}\varphi$, then $\varGamma \vee \chi \vdash _{\mathrm {DP}}\varphi \vee \chi$, where $\varGamma \vee \chi :=\{\gamma \vee \chi : \gamma \in \varGamma \}$.

Proof

It follows from the fact that the consequence relation $\vdash _{\mathrm {DP}}$ is finitary, Proposition 2.1, and by the rules of inferences. $\square$

Proposition 2.3

The logic ${\mathcal {S}}_{\mathrm {DP}}$ satisfies the Proof by Cases Principle. That is, for all $\varGamma \cup \{\varphi ,\psi ,\chi \}\subseteq \mathbf{Fm}$,

$$ \begin{aligned} \varGamma ,\varphi \vdash _{\mathrm {DP}}\chi \quad \& \quad \varGamma ,\psi \vdash _{\mathrm {DP}}\chi \implies \varGamma ,\varphi \vee \psi \vdash _{\mathrm {DP}}\chi . \end{aligned}$$

Proof

Since $\vdash _{\mathrm {DP}}$ is finitary, it is sufficient to prove a weaker version of the Proof by Cases Principle. We prove that

$$ \begin{aligned} \varphi \vdash _{\mathrm {DP}}\chi \quad \& \quad \psi \vdash _{\mathrm {DP}}\chi \implies \varphi \vee \psi \vdash _{\mathrm {DP}}\chi . \end{aligned}$$

Assume that $\varphi \vdash _{\mathrm {DP}}\chi$ and $\psi \vdash _{\mathrm {DP}}\chi$. By Proposition 2.1, we have that $\varphi \vee \psi \vdash _{\mathrm {DP}}\chi \vee \psi$ and $\psi \vee \chi \vdash _{\mathrm {DP}}\chi \vee \chi$. From rules (R5) and (R12), we obtain that $\chi \vee \psi \vdash _{\mathrm {DP}}\chi$. Hence, $\varphi \vee \psi \vdash _{\mathrm {DP}}\chi$. $\square$

Now we are ready to present a standard proof of the following result of completeness.

Theorem 2.4

The logics ${\mathcal {S}}_{\mathrm {DP}}$ and ${\mathcal {S}}_{\wedge ,\vee }$ coincide. That is, for all $\varGamma \cup \{\varphi \}\subseteq \mathbf{Fm}$,

$$\begin{aligned} \varGamma \vdash _{\mathrm {DP}}\varphi \iff \varGamma \vDash _{{\mathbf {2}}}\varphi . \end{aligned}$$

Proof

The implication from left to right (soundness), is a routine proof. Now we prove the other implication. First, without loss of generality we can assume that $\varGamma$ is a theory of the logic ${\mathcal {S}}_{\mathrm {DP}}$. Suppose that $\varGamma \nvdash _{\mathrm {DP}}\varphi$. Then, there exists a theory $\varDelta$ of ${\mathcal {S}}_{\mathrm {DP}}$ such that $\varGamma \subseteq \varDelta$, $\varphi \notin \varDelta$, and $\varDelta$ is maximal among all the theories of ${\mathcal {S}}_{\mathrm {DP}}$ not containing $\varphi$ (see for instance [3, Lemma 1.43]). Now we define the map $h:\mathbf{Fm} \rightarrow {\mathbf {2}}$ as follows: for every $\alpha \in \mathbf{Fm}$, $h(\alpha )=1 \iff \alpha \in \varDelta$. We need to show that h is a homomorphism. Let $\alpha ,\beta \in \mathbf{Fm}$. Since $\varDelta$ is a theory, it follows by rules (R1) and (R3) that $\alpha \wedge \beta \in \varDelta \iff \alpha ,\beta \in \varDelta$. Hence, $h(\alpha \wedge \beta )=h(\alpha )\wedge h(\beta )$. Now, by rules (R4) and (R5), we have that if $\alpha \in \varDelta$ or $\beta \in \varDelta$, then $\alpha \vee \beta \in \varDelta$. Then, $h(\alpha )=1$ or $h(\beta )=1$ implies $h(\alpha \vee \beta )=1$. Now assume that $h(\alpha \vee \beta )=1$. That is, $\alpha \vee \beta \in \varDelta$. Suppose that $h(\alpha )\ne 1$ and $h(\beta )\ne 1$. Thus $\alpha ,\beta \notin \varDelta$. Let $\varDelta _\alpha$ and $\varDelta _\beta$ be the theories of ${\mathcal {S}}_{\mathrm {DP}}$ generated by $\varDelta \cup \{\alpha \}$ and $\varDelta \cup \{\beta \}$, respectively. By the maximality of $\varDelta$, we obtain that $\varphi \in \varDelta _\alpha$ and $\varphi \in \varDelta _\beta$. Thus we have that $\varDelta ,\alpha \vdash _{\mathrm {DP}}\varphi$ and $\varDelta ,\beta \vdash _{\mathrm {DP}}\varphi$. Then, by Proposition 2.3, it follows that $\varDelta ,\alpha \vee \beta \vdash _{\mathrm {DP}}\varphi$. Since $\alpha \vee \beta \in \varDelta$, it follows that $\varDelta \vdash _{\mathrm {DP}}\varphi$, a contradiction. Hence, we prove that $h(\alpha \vee \beta )=1$ implies that $h(\alpha )=1$ or $h(\beta )=1$. Thus, we obtain that $h(\alpha \vee \beta )=1$ $\iff$ $h(\alpha )=1$ or $h(\beta )=1$. Then $h(\alpha \vee \beta )=h(\alpha )\vee h(\beta )$. We have proved that $h:\mathbf{Fm} \rightarrow {\mathbf {2}}$ is a homomorphism such $h(\varGamma )\subseteq \{1\}$ and $h(\varphi )\ne 1$. Hence $\varGamma \nvDash _{{\mathbf {2}}}\varphi$. $\square$

Another standard alternative proof of the completeness between the $\{\wedge ,\vee \}$-fragment of classical logic and the Hilbert-style axiomatization given in [2], following also usual arguments, is possible. This proof makes explicit the role of the Lindenbaum-Tarski algebra. We sketch the proof and left the details to the reader. Suppose that $\varGamma \nvdash _{\mathrm {DP}}\varphi$, and assume that $\varGamma$ is a theory. Then:

• 1. We consider the binary relation $\varLambda (\varGamma )$ on $\mathbf{Fm}$ defined as follows:

  $$\begin{aligned} (\alpha ,\beta )\in \varLambda (\varGamma ) \iff \varGamma ,\alpha \vdash _{\mathrm {DP}}\beta \ \text { and } \ \varGamma ,\beta \vdash _{\mathrm {DP}}\alpha . \end{aligned}$$

• 2. $\varLambda (\varGamma )$ is a congruence on $\mathbf{Fm}$. Apply the Proof by Cases Principle.

• 3. The quotient algebra $\mathbf{Fm} /\varLambda (\varGamma )$ is a distributive lattice. It is also necessary to apply the Proof by Cases Principle.

• 4. $[\alpha ]\in \varGamma /\varLambda (\varGamma )$ if and only if $\alpha \in \varGamma$.

• 5. $\varGamma /\varLambda (\varGamma )=\emptyset$ or $\varGamma /\varLambda (\varGamma )$ is a proper filter of $\mathbf{Fm} /\varLambda (\varGamma )$.

• 6. There exists a prime filter ${\mathcal {F}}$ of $\mathbf{Fm} /\varLambda (\varGamma )$ such that $\varGamma /\varLambda (\varGamma )\subseteq {\mathcal {F}}$ and $[\varphi ]\notin {\mathcal {F}}$.

• 7. The map $f:\mathbf{Fm} /\varLambda (\varGamma )\rightarrow {\mathbf {2}}$ defined by $f([\alpha ])=1\iff [\alpha ]\in {\mathcal {F}}$ is a homomorphism.

• 8. Let $v:\mathbf{Fm} \rightarrow {\mathbf {2}}$ be the homomorphism given by $v(\alpha )=f([\alpha ])$. Hence $v(\varGamma )\subseteq \{1\}$ and $v(\varphi )=0$. Therefore, $\varGamma \nvDash _{{\mathbf {2}}}\varphi$.

The relation $\varLambda (\varGamma )$ is known as the Frege relation of $\varGamma$ relative to ${\mathcal {S}}_{\mathrm {DP}}$ and the quotient algebra $\mathbf{Fm} /\varLambda (\varGamma )$ is named the Lindenbaum-Tarski algebra, see for instance [5, 6].