Proof verification: classical propositional logic is Post-complete.
I'm trying to prove the Post-completeness of classical propositional logic. In order to do this, I will be proving a theorem about Boolean rings and then later adding the glue in prose to connect it to the original statement.
The problem I'm running into is that the Post-completeness of classical propositional logic is so intuitively obvious that I'm not sure whether I've proven it or not. My idea was to paraphrase statements about classical propositional logic into statements about Boolean rings, and then show that adding any new open equation as an axiom would rule out every ring except the trivial one and hence lead to trivial, one-valued logic.
I'm interested in:
- Whether the argument works
- Whether I'm using an assumption somewhere that I'm not listing up front.
- Whether there's a simpler argument for the Post-completeness of classical propositional logic.
I assume the following without proof:
- Every vector space has a basis.
- An open term in the language of Boolean rings can be rewritten into arithmetic normal form.
- The deduction theorem for classical propositional logic.
- We can map back and forth between the language of classical propositional logic and the language of Boolean rings.
In the equational theory of Boolean rings, let the signature be $1, +, \times$. Let $0$ be an abbreviation for $1+1$. Let $ab$ be an abbreviation for $a \times b$.
The following axioms define a Boolean ring. Enumerating these axioms is perhaps not necessary, but this is what I mean by a Boolean ring.
- $a+0 \approx a$
- $a+a \approx 0$
- $a+b \approx b+a$
- $a+(b+c) \approx (a+b)+c$
- $a \times b \approx b \times a$
- $a \times a \approx a$
- $a \times (b \times c) \approx (a \times b) \times c$
- $a \times 1 \approx a$
- $a \times 0 \approx 0$
- $(a+b) \times (c+d) \approx ac + bc + ad + bd$
I do not insist that $0$ and $1$ be distinct elements.
Let $M_1$ refer to the trivial Boolean ring on one element.
Let $M_2$ refer to the unique Boolean ring on two elements.
Lemma 101: $M, \vec{v} \models \delta(\vec{v}) \not\approx 0$ for some $M$ and $\vec{v}$ implies $M_2, \vec{u} \models \delta(\vec{u}) \not\approx 0$ for some $\vec{u}$.
$\delta(\vec{v})$ can be expressed in normal form in the following way, where $\vec{a}$ is a sequence of integers and $\vec{g}$ is a sequence of elements of $M$.
$$ \delta(\vec{v}) = \sum_{i=1}^{n} \prod_{j=1}^{\vec{a}_n} \vec{g}_{ij} $$
$M$ is a vector space over the field with two elements, therefore, by the fact that every vector space has a basis, $M$ has a basis. Note, however, that $\times$ need not be componentwise with respect to this basis $B$.
Since $\delta(\vec{v})$ is, by hypothesis, not equal to zero, there exists a basis element $b$ such that $\langle g, b \rangle = 1$. Note that since $b$ is a basis element, we can treat $\langle g, b \rangle$ as well-defined even when $B$ is countably infinite or uncountably infinite.
We then note that the Boolean product $\times$ operates componentwise with respect to our basis.
$$ \left\langle \sum_{i=1}^{n} \prod_{j=1}^{\vec{a}_n} \vec{g}_{ij}, b \right\rangle = \sum_{i=1}^{n} \left\langle \prod_{j=1}^{\vec{a}_n} \vec{g}_{ij} ,b \right\rangle = \sum_{i=1}^n \prod_{j=1}^{\vec{a}_n} \left\langle \vec{g}_{ij}, b \right\rangle $$
Since the RHS of the above chain of equalities consists only of $0$ and $1$.
Therefore, we can construct a variable mapping $\vec{u}$ where $\vec{u}(x) = \langle g_{ij}, b \rangle$ when $\vec{v}(x) = g_{ij}$.
Thus we are done.
Lemma 102: $\mathcal{M} \models \delta(\vec{v}) \approx 0$ if and only if $\{M_1, M_2\} \models \delta(\vec{v}) \approx 0$.
For the $\Rightarrow$ case, suppose by way of contrapositive that $\{M_1, M_2\} \not\models \delta(\vec{v}) \approx 0$.
In $M_1$, all elements are zero, thus $M_2 \not\models \delta(\vec{v}) \approx 0$.
$M_2$ is in $\mathcal{M}$, so $\mathcal{M} \not\models \delta(\vec{v}) \approx 0$ as desired.
For the $\Leftarrow$ case, suppose by way of contrapositive that $\mathcal{M} \not\models \delta(\vec{v}) \approx 0$.
Thus there exists an $M$ and a $\vec{v}$ such that $M, \vec{v} \not\models \delta(\vec{v}) \approx 0$.
By invoking Lemma 101, it follows that there exists a $\vec{u}$ so that $M, \vec{u} \not\models \delta(\vec{u}) \approx 0$.
Thus $M \not\models \delta(\vec{u}) \approx 0$ as desired.
Lemma 103: $\mathcal{M} \models \delta(\vec{v}) \approx \eta(\vec{v})$ if and only if $\{M_1, M_2\} \models \delta(\vec{v}) \approx \eta(\vec{v})$.
This lemma follows from the straightfoward observation that $\delta(\vec{v}) \approx \eta(\vec{v})$ holds in a model if and only if $\delta(\vec{v}) + \eta(\vec{v}) \approx 0$ holds.
Proof: classical propositional logic is Post-complete.
Suppose we have an axiomatization for classical propositional logic with the inference rule modus ponens.
Suppose we have a new contraclassical inference rule $\Gamma \vdash \varphi$ that we are considering adding to classical propositional logic.
By the deduction theorem and the validity of modus ponens, we can rewrite $\Gamma \vdash \varphi$ into $\gamma$, which is $\Gamma_1 \to \Gamma_2 \to \cdots \to \Gamma_n \to \varphi$, giving us a new axiom $\gamma$. The logic formed by adding the new inference rule $\Gamma \vdash \varphi$ is the same as the logic formed by adding the new axiom $\gamma$.
Our axiom $\gamma$, can be translated into an equation in the language of Boolean rings with the RHS equal to $1$, thus we also have:
$$ 1 + \gamma' \approx 0 \;\;\text{where $\gamma'$ is the translation of $\gamma$} $$
Since $\gamma$ is a new axiom, that means that $1 + \gamma' \approx 0$ does not hold in every model of $\mathcal{M}$.
Therefore, by lemma 103, $1 + \gamma' \approx 0$ does not hold in both $\{M_1, M_2\}$.
$1 + \gamma' \approx 0$ does not hold in $M_2$ because it is contraclassical by hypothesis.
Therefore $M_1$ is the sole remaining model.
Every equation holds in $M_1$.
Therefore classical propositional logic extended with $\gamma$ is trivial.
Therefore classical propositional logic is Post-complete.