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