Prerequisites for consistency proofs of propositional calculus

Question

I've looked at some sketches how to "prove" the consistency of propositional calculus. It goes something like this: Show that the axioms

$\begin{align}1. \quad & (A \rightarrow (B \rightarrow A)) \\ 2. \quad &((A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))) \\ 3.\quad & ((\neg A \rightarrow \neg B) → (B \rightarrow A))\end{align}$

are tautologies (in the truth table sense), show that modus ponens carries tautologies to tautologies, so all theorems are tautologies. We can easily convince ourselves, that the negation of a tautology is not a tautology. But we can just deduce tautologies, so we can't deduce a theorem and it's negation.

Now, in this informal reasoning, aren't we just presupposing at least modus ponens, the third axiom and even some kind of induction? What do we actually gain by such proofs?

Answer 1

The third axiom is a formal statement... a well-formed formula. You don't presuppose a formal statement in that way when you reason metalogically. I don't see that you've necessarily presupposed axiom 3.

Any formal proof results in a tautology, as you outlined. All theorems are tautologies. Now, suppose the consistency meta-theorem false. Then, we could deduce something which is not a theorem. Since anything deducible is a theorem, we could then deduce some formal theorem which is not a formal theorem. Consequently, the supposition that consistency theorem is false has resulted in a contradiction, and thus by proof by contradiction, the consistency meta-theorem holds.

Now, I suppose someone might argue that proof by contradiction (in it's strongest form when stated formally) has as much effect as axiom 3. Thus, we must have presupposed axiom 3, in Polish notation CCNpNqCqp, along the way. Maybe we presupposed an informal statement which would have similar meaning to CpCCNqNpq were it the case that well-formed formulas had meaning. That is like saying that two distinct formal axioms are equivalent, but it has something to it, because of the consequences of CCNpqCCNpNqp or CCNpNqCCNpqp or CCNpNqCqp or CpCCNqNpq in the presence of the other 2 axioms all end up the same.

So, let's try another sort of reasoning.

Suppose that the consistency meta-theorem is false. Make a second assumption that we can deduce some formula F which is not a theorem. Consequently, by the definition of a formal proof, F qualifies as a theorem. Now we discharge the second assumption into a conditional meaning that the assumption of some deducible formula F as not a theorem implies that it is a theorem. It follows by the informal law of Clavius that this F is a theorem. So, by the soundness meta-theorem this F is a tautology. It is not the case that for any tautology that it is not a tautology. So, since F is a tautology it can't hold that F is not a theorem, since any formula which is not a tautology is not a theorem. Since F was arbitrary, for no formula F does it hold that F is both a theorem and not a theorem. But, that is what the consistency meta-theorem says. Thus, we discharge the first assumption above into a conditional which says that the negation of the consistency meta-theorem implies the consistency meta-theorem. Therefore, by the informal law of Clavius, the consistency meta-theorem holds true.

I do agree that you've presupposed modus ponens.

I don't see any presupposition of induction anywhere in the above. But, that no last theorem exists can get seen as present due to the recursive definition of well-formed formulas and axiom 1, or the rule of uniform substitution.