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 $$
Best Answer
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.