Metatheory

“[A] somewhat different extension of our subject matter occurs when we discuss the form of our metamathematical definitions and theorems in turn. If we chose to be meticulous in our way of doing this, it would constitute a metametamathematics.”
—Stephen Kleene

Now that we have formal (mathematically precise) definitions of WFFs, truth, and proof, we can think about proving facts about formulas and proofs. Proofs about logical systems are known as metaproofs and the study of metaproofs is called metatheory.

Soundness

How might we prove this theorem? The full details are beyond the scope of these notes, but here’s the basic idea:

• Proofs are finite sequences of steps, justified by the natural deduction rules.
• Since proofs are finite, if there is a property that all ND proofs have, we can try to prove that property by induction on the length of the ND proof.
• Specifically, we can prove that all ND proofs have the following property, by induction on the length of the ND proof:
  • Every line is either an assumption, or is a formula that is true (according to truth tables) whenever the assumptions it depends on are true.
• Intuitively, the reason the inductive step works (going from a proof of length $n$ with this property to a proof of length $n+1$) is that the last line of the proof will be justified by one of the dozen or so ND rules, and each of the ND rules “preserves truth.” If the premises of the rule are already true, then the conclusion is true.

Completeness

How might we show that Natural Deduction is sound for classical propositional logic? The full proof is beyond the scope of these notes, but the basic idea involves three steps.

Step 1: A Lemma

That is, if we explicitly assume the propositional variables involved in ${\cal A}$ are true or false, then ${\cal A}$ is provable if the truth tables tell us ${\cal A}$ should be true, and $\lnot {\cal A}$ is provable if the truth tables tell us ${\cal A}$ should be false.

How can we prove this lemma? Well, every WFF is a finite sequence of symbols, and the proof of this property proceeds by induction on the length of ${\cal A}$.

In the base case, ${\cal A}$ is a propositional variable (and we just use the corresponding assumption) or a constant (and we either proof $\top$ or $\lnot\bot$ as needed).

In the inductive case, we consider all the different kinds of WFF that ${\cal A}$ could be:

• If ${\cal A}$ is a conjunction of the form ${\cal C}\land {\cal D}$, then (since ${\cal C}$ and ${\cal D}$ are strictly smaller than ${\cal A}$) we can apply the inductive hypotheses to both ${\cal C}$ and ${\cal D}$. Then:
  • If $M$ makes ${\cal A}$ true, it must be because $M$ makes ${\cal C}$ true and $M$ makes ${\cal D}$ true. So by the inductive hypothesis, we can assume that $\ldots M\ldots \ \vdash \ {\cal C}$ and $\ldots M\ldots \ \vdash \ {\cal D}$. Putting these together (with the $\land I$ rule) guarantees we can prove $\ldots M\ldots \ \vdash {\cal C}\land {\cal D}$. That is, $\ldots M\ldots \ \vdash \ {\cal A}$.
  • If $M$ makes ${\cal A}$ false, it must be because $M$ makes ${\cal C}$ false or because $M$ makes ${\cal D}$ false (or both). In the first case, the inductive hypothesis tells us that $\ldots M\ldots \ \vdash \ \lnot {\cal C}$, and in the other cases, we can show that $\ldots M\ldots \ \vdash \ \lnot {\cal D}$. Either of these proofs can be extended (with a few more proof steps) to show that $\ldots M\ldots \ \vdash \ \lnot ({\cal C}\land {\cal D})$. That is, $\ldots M\ldots \ \vdash \ \lnot {\cal A}$.
• If ${\cal A}$ is a disjunction, implication, or negation, then we proceed similarly.

Step 2: Completeness for Tautologies

That is, tautologies (formulas true in every model) are provable in Natural Deduction from no assumptions.

The proof works as follows: Suppose the propositional variables in ${\cal B}$ are $p_1,\ldots,p_n$. Then we can apply LEM and $\lor E$ to consider all $2^n$ cases of those propositional variables being assumed true or false. For example, in the case where $n=2$, we set up a proof with the following form, where we have to prove ${\cal B}$ in $2^2 = 4$ sub-subcases:

Since ${\cal B}$ is a tautology, Lemma 1 guarantees that

and so the gaps in the above proof (lines 5, 7, 11, and 13) can be filled.

Step 3: Completeness

The argument goes as follows:

1. Assume ${\cal A}_1,\ldots,{\cal A}_n \vDash {\cal B}$ (i.e., that ${\cal B}$ is true in every model where the ${\cal A}$’s are true).
2. Then by the truth table for implication, $\vDash ({\cal A}_1\land\cdots\land {\cal A}_n) \to {\cal B}$.
3. By Lemma 2, $\vdash ({\cal A}_1\land\cdots\land {\cal A}_n) \to {\cal B}$.
4. Using that proof and the $\land I$ and $\to E$ rules, we can build a proof showing ${\cal A}_1,\ldots,{\cal A}_n \vdash {\cal B}$.