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 2


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.

  • 1
    $\begingroup$ 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.) $\endgroup$ Nov 30, 2021 at 1:31
  • 3
    $\begingroup$ @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. $\endgroup$ 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).


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .