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

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$$

## 2 Answers

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.

• Oh that's cool! I think $M$ is also the meet/minimum of all the valuations $N$ such that $N \models \Gamma$. Does that trick work whenever the meet of all the valuations $N \models \Gamma$ exists and also satisfies $\Gamma$? (I'm defining the meet as the elementwise conjunction of valuations.) Nov 30, 2021 at 1:31
• @GregoryNisbet Right! This logic admits, for every theory $\Gamma$, a "minimal" model which satisfies fewer sentences than any other model. If you have a logic that admits minimal models in this sense, completeness theorems are particularly easy, because the minimal model should satisfy exactly the sentences provable from $\Gamma$ and no others. Nov 30, 2021 at 1:34

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).