Alternative proof for soundness and completeness of standard semantics for conjunction-only fragment of classical propositional calculus

Question

I'm trying to prove the completeness and soundness of the standard inference rules (listed below) of the conjunction-only fragment of classical logic.

The conjunction-only fragment of classical logic is extremely simple. The introduction and elimination rules for $\land$ are also extremely simple. My proof, however, has ended up way more complicated than I would have liked.

My question is twofold.

• Is there an alternative way to prove this that's simpler and less verbose?
• On the flip side, did I gloss over anything that shouldn't be glossed over or use an invalid argument somewhere?

For example, I think my argument about building a proof tree and then hacking off part of it is valid but possibly too sketchy.

---

First a word on notation, I nonstandardly use $\psi \prec \varphi$ to mean that the well-formed formula $\psi$ occurs textually as a subexpression of $\varphi$. I also use $\psi \prec \Gamma$ to mean that there exists an element $\varphi$ of $\Gamma$ such that $\psi \prec \varphi$.

$A$, when used outside of an inference rule, is a primitive proposition (a well-formed formula consisting of a propositional constant only). $S$, $\varphi$, and $\psi$ are well-formed formulas. $\Gamma$ is a set of well-formed formulas. $\Delta$ is a set of well-formed formulas where each formula is constrained to be a primitive proposition. $M$ is a valuation, a map assigning truth values to primitive propositions.

For the standard semantics, my truth values are $\varnothing$ and $\{\varnothing\}$. Only $\{\varnothing\}$ is designated.

In addition, $[\varphi \land \psi]$ is equal to $[\varphi] \cap [\psi]$.

If $\Gamma$ is a set of well-formed formulas, then $[\Gamma]$ is $\bigcap_{\varphi \in \Gamma}[\varphi]$

Here are my inference rules:

$$ \frac{A \;\text{and}\; B}{A \land B} \;\; \text{is conjunction introduction} $$

$$ \frac{A \land B}{A} \;\; \text{and} \;\; \frac{A \land B}{B} \;\; \text{are conjunction elimination} $$

Let $S$ be an arbitrary proposition. I want to show

$$ \Gamma \vdash S \;\;\text{if and only if}\;\; \Gamma \models S $$

Lemma 101: $\Gamma \vdash S$ if and only if $\{A : A \prec \Gamma\} \vdash S$ where $A$ is a primitive proposition.

If $\Gamma \vdash S$, then, via repeated application of conjunction elimination, I can prove each primitive proposition $A \prec \Gamma$. I can also, via repeated application of conjunction introduction, prove $\Gamma$ given $\{A : A \prec \Gamma\}$. Thus I can show:

$$ \Gamma \implies \{ A : A \prec \Gamma \} \implies \Gamma \implies S $$

By cutting off the first part of the proof tree, giving the figure below, I can make a proof tree for $\{A : A \prec \Gamma\} \vdash S$.

$$ \require{cancel} \xcancel{\Gamma \implies} \{ A : A \prec \Gamma \} \implies \Gamma \implies S $$

If $\{ A : A \prec \Gamma \} \vdash S$, then I can prove $\Gamma$ by repeatedly using conjunction introduction and then get $\{A : A \prec \Gamma\}$ again using conjunction elimination.

$$ \{A : A \prec \Gamma \} \implies \Gamma \implies \{A : A \prec \Gamma\} \implies S $$

$$ \require{cancel} \xcancel{\{A : A \prec \Gamma \} \implies} \;\; \Gamma \implies \{A : A \prec \Gamma\} \implies S $$

Lemma 102: $\Gamma \models S$ if and only if $\{A : A \prec \Gamma\} \models S$ where $A$ is a primitive proposition.

Let $\varphi$ be a well-formed formula. $[\varphi]$ is equal to $\bigcap_{A \prec \varphi} [A]$ because the only connective is $\land$. Since there are only two possible values for each $A$, $[\varphi]$ is non-empty if and only if all, for all $A \prec \varphi$, $[A]$ is non-empty.

$[\Gamma]$ is non-empty if and only if all, for all $\varphi$ in $\Gamma$, $[\varphi]$ is non-empty.

Therefore $[\Gamma]$ is equal to $[\{A : A \prec \Gamma\}]$.

Therefore $\Gamma \models S$ if and only if $\{A : A \prec \Gamma\} \models S$ as desired.

Lemma 103: $\Delta \vdash S$ if and only if $\Delta \models S$ where all well-formed formulas in $\Delta$ are primitive propositions.

Suppose $S$ is a primitive proposition. $\Delta \vdash S$ if and only if $S \in \Delta$.

If $S$ is in $\Delta$, then $S$ holds in any valuation $M$ such that $M \models \Delta$. If $S$ is not in $\Delta$, then there exists a valuation $M_0$ that sends all primitive propositions in $\Delta$ to $\{\varnothing\}$ and everything else to $\varnothing$. Thus $\Delta \models S$ if and only if $S \in \Delta$ when $S$ is constrained to be a primitive proposition.

If $\Delta \vdash S_1$ holds and $\Delta \vdash S_2$ holds, then $\Delta \vdash S_1 \land S_2$ holds because I can freely reuse hypotheses in a proof tree and then use conjunction introduction.

If $\Delta \vdash S_1 \land S_2$ holds, then $\Delta \vdash S_1$ holds and $\Delta \vdash S_2$ holds by conjunction elimination.

If $\Delta \models S_1$ holds and $\Delta \models S_2$ holds, then $[S_1]$ and $[S_2]$ are both equal to $\{\varnothing\}$ and thus $[S_1\land S_2]$ is also equal to $\{\varnothing\}$.

If $\Delta \models S_1 \land S_2$, then $[S_1 \land S_2]$ is $\{\varnothing\}$. Thus, $[S_1]$ and $[S_2]$ are both equal to $\{\varnothing\}$.

Proof $\Gamma \vdash S$ if and only if $\Gamma \models S$

I have proven the following equivalences, thus we are done.

$$ \Gamma \vdash S \stackrel{101}{\iff} \{A : A \prec \Gamma \} \vdash S \stackrel{103}{\iff} \{A : A \prec \Gamma\} \models S \stackrel{102}{\iff} \Gamma \models S $$

Answer 1

Your proof essentially proceeds by completely understanding the relations $\vdash$ and $\models$. I think it can be summarized/streamlined like this: We have $\Gamma\vdash \varphi$ if and only if every proposition letter appearing in $\varphi$ appears in $\Gamma$ if and only if $\Gamma\models \varphi$.

This works, but only because the $\vdash$ and $\models$ relations have such simple descriptions for this logic.

Let me give another proof. I think it's simpler than yours, and it has the advantage of following a common approach for soundness and completeness proofs - so it will generalize more easily to more complex logics. Here's the outline:

(1) Prove soundness by induction on the proof tree. (2) For completeness, use the theory $\Gamma$ to build a special model/valuation $M$ from the syntax, such that truth in that model is tied to provability from $\Gamma$. For more complicated logics, we often need to argue by contrapositive: (a) assume $\Gamma\not\vdash \varphi$ (b) build $M$ so that $M\models \Gamma$ but $M\not\models \varphi$, (c) conclude $\Gamma\not\models \varphi$. But this logic is simple enough that we can build $M$ in a really canonical way, which allows us to argue directly: (a) assume $\Gamma\models \varphi$, (b) build $M\models \Gamma$ so that $M\models \psi$ if and only if $\Gamma\vdash \psi$, and (c) conclude that $M\models \varphi$, so $\Gamma\vdash \varphi$.

---

Soundness: Suppose $\Gamma \vdash \varphi$. We wish to show $\Gamma\models \varphi$. Let $M$ be a valuation with $M\models \Gamma$. We proceed by induction on the structure of the proof $\Gamma\vdash \varphi$.

Case 1: If the proof ends with an axiom $\psi\in \Gamma$, then since $M\models \Gamma$, $M\models \psi$, as desired.

Case 2: If the proof ends with the rule $\frac{A\quad B}{A\land B}$, then by induction $M\models A$ and $M\models B$, so $M\models A\land B$ by the semantics for $\land$, as desired.

Case 3: If the proof ends with the rule $\frac{A\land B}{A}$, then induction $M\models A\land B$, so $M\models A$ by the semantics for $\land$, as desired.

This completes the proof.

Completeness: Suppose $\Gamma\models \varphi$. We wish to show $\Gamma\vdash \varphi$. We define a valuation $M$ by setting, for each propositional variable $P$, $$P^M = \begin{cases}\top & \text{if }\Gamma\vdash P\\ \bot & \text{otherwise}.\end{cases}$$

I claim that for any sentence $\psi$, $M\models \psi$ if and only if $\Gamma\vdash \psi$. We proceed by induction on the structure of $\psi$.

Case 1: If $\psi$ is a propositional variable $P$, then $M\models \psi$ if and only if $P^M = \top$ if and only if $\Gamma\vdash \psi$, as desired.

Case 2: Suppose $\psi$ is $A\land B$. If $M\models \psi$, then $M\models A$ and $M\models B$, by the semantics for $\land$. By induction, $\Gamma\vdash A$ and $\Gamma\vdash B$. By an application of the conjunction introduction rule, $\Gamma\vdash \psi$. Conversely, if $\Gamma\vdash \psi$, then by an applciation of each of the conjunction elimination rules, $\Gamma\vdash A$ and $\Gamma\vdash B$. By induction, $M\models A$ and $M\models B$, so $M\models \psi$, by the semantics for $\land$.

This completes the proof of the claim. Now for each $\theta\in \Gamma$, $\Gamma\vdash \theta$, so $M\models \theta$ by the claim. Thus $M\models \Gamma$. By our assumption that $\Gamma\models \varphi$, $M\models \varphi$. By the claim again, $\Gamma\vdash \varphi$, as was to be shown.

Answer 2

I restrict $A \prec \Gamma$ and $A \prec \phi$ to when $A$ is primitive.

First, note that soundness is fairly trivial.

Thm. If $\Gamma \vdash \phi$ then $\Gamma \models \phi$.

Proof: We simply prove that all four of the rules of deduction used to construct proof trees are sound (that is, they hold when replacing $\Gamma \vdash \phi$ with $\Gamma \models \phi$), then apply induction on proof trees. The four rules are conjunction introduction, the two forms of conjunction elimination, and the rule which states that if $A \in \Gamma$ then $\Gamma \vdash A$. $\square$

The hard bit is proving completeness; that is, proving that if $\Gamma \models \phi$ then $\Gamma \vdash \phi$.

For completeness, we prove

Lemma: Let $M$ be a truth assignment, and let $\phi$ be a formula. Suppose for all $A \prec \phi$ that $M(A) = \top$. Then $M \models \phi$.

Proof: induction on $\phi$. If $\phi$ is primitive, then $M(\phi) = \top$ and thus $M \models \phi$. If $\phi = \psi_1 \land \psi_2$, then for all $A \prec \psi_i$, we have $M(A) = \top$, and therefore by the inductive hypothesis $M \models \psi_i$, so we can conclude by the definition of $\models$ that $M \models \phi$. $\square$

Thm. If $A$ is a primitive proposition and $\Gamma \models A$ then $A \prec \Gamma$.

Proof: define $M(B) = \{x \in \{\emptyset\} \mid B \prec \Gamma\}$. Note that for all $\phi \in \Gamma$, the above lemma shows that $M \models \phi$; therefore, $M \models \Gamma$. Since $\Gamma \models A$, we have that $M(A) = \top$, and therefore $A \prec \Gamma$. $\square$

Thm. Suppose $A$ is primitive and $A \prec \phi$. If $\Gamma \vdash \phi$ then $\Gamma \vdash A$.

Proof: induction on $\phi$. If $\phi$ is primitive, then $A = \phi$ and we're done. If $\phi = \psi_1 \land \psi_2$, take $\psi_i$ such that $A \prec \psi_i$. Then by conjunction intro, $\Gamma \vdash \psi_i$, and thus by the inductive hypothesis, $\Gamma \vdash A$. $\square$

Corollary: If $A \prec \Gamma$ then $\Gamma \vdash A$.

Proof: Take some $\phi \in \Gamma$ such that $A \prec \phi$. Since $\Gamma \vdash \phi$, $\Gamma \vdash A$. $\square$

Completeness Theorem: For all $\phi$, if $\Gamma \models \phi$ then $\Gamma \vdash \phi$.

Proof: induction on $\phi$. If $\phi$ is primitive, then $\phi \prec \Gamma$ and therefore $\Gamma \vdash \phi$. If $\phi$ is of the form $\theta \land \psi$, then $\Gamma \models \theta$ and also $\Gamma \models \psi$, so $\Gamma \vdash \theta$ and also $\Gamma \models \psi$, and by conjunction introduction, $\Gamma \models \phi$.

I started this answer and then forgot to post it before grabbing dinner, but I decided to finish it and post it since it is constructive in the case that the set of primitive variables has decidable equality and $\Gamma$ is finite (unlike Kruckman's proof, which is not constructive even under these circumstances but is nicer in that it is short).