Absolute proof of consistency of FSN

In section IV of their great little book, Nagel and Newman discuss efforts by Gottlob Frege and then Bertrand Russell to reduce arithmetic to logic. This is clearly another attempt at a relative proof of consistency: if this reduction were successful, then arithmetic would be consistent provided logic is consistent.

Whether this latter statement is true or not, Whitehead and Russell's Principia Mathematica was a landmark achievement: it almost completed the first step in an absolute proof of consistency of arithmetic, since it led to the formalization of an axiomatic system for arithmetic.

In section V, Nagel and Newman describe a formalization of propositional (or sentential) logic, that is, a subset of the logic system in Principia Mathematica (but not a large enough subset to represent arithmetic). The bulk of this section first describes the formalization process, which yields the standard syntax and inference rules of propositional logic (including modus ponens) and then outlines an absolute proof of consistency of this formalized axiomatic system.

This absolute proof of consistency is a proof by contrapositive, which relies on the following true conditional statement:

"If the formal system is not consistent, then it can prove ALL of the syntactically legal formulas in the formal system."

[Here is a quick proof of this statement, which is classically called "ex falso quodlibet."]

Now, the contrapositive of this statement, which must then also be true, is:

"If the formal system cannot prove ALL of the syntactically legal formulas in the formal system, then it is consistent."

[Aside: In logic, a conditional statement and its contrapositive are logically equivalent, which means that they are either both true or both false. In this case, they are both true.]

Finally, if we can prove that "the formal system cannot prove ALL of the syntactically legal formulas", then we can use modus ponens and the contrapositive statement above to infer that the formal system is consistent.

Therefore, Nagel and Newman wrap up section V by proving that all theorems of 'their' formal system are tautologies (they are always true under all possible substitutions of propositions for propositional variables) and that some syntactically legal formulas, such as p ∨ q, are not tautologies and are therefore not theorems of the formal system.

In the rest of this post, instead of going over their proof in detail, I will provide a different and simpler, absolute consistency proof, namely the consistency of our simple formal system called FSN.  Recall the axiom and inference rules of FSN:

Axiom 1 [A1]:

E0

Inference rule 1 [IR1]:

Eα (where α is any non-empty finite sequence of 0's and 1's) E0α

Inference rule 2 [IR2]:

Eα (where α is any non-empty finite sequence of 0's and 1's) E1α

Inference rule 3 [IR3]:

Eβ0 (where β is any finite sequence of 0's and 1's) ¬Eβ1

Here is a really short sketch of the absolute proof of consistency of FSN that fills up the rest of this post: FSN cannot derive both a theorem and its negation because all of the theorems that start with a negation symbol end with the symbol '1' but all of the theorems that do not start with a negation symbol end with the symbol '0'.

Nevertheless, it is interesting to try and write a rigorous proof. Notice how the proof sketch above is a clear example of meta-reasoning, that is, reasoning about (and outside of) the formal system itself.

So, before we give an absolute proof of consistency of FSN, let's start with a simple example of meta-reasoning about FSN.

Let T be any theorem of FSN. Let's prove the following meta-theorem:

[MT1]  Every theorem of FSN has the form 'Eγ' or the form '¬Eγ' where γ is a non-empty sequence of 0's and 1's. 

To prove this meta-theorem about the set of theorems of FSN, we must reason outside of the system. More specifically, we can write a proof by structural induction. In other words, we can analyze the structure of the axiom and inference rules to prove that all theorems generated by any one of them has the property stated in MT1.

---

Proof of MT1 by structural induction: Let T be any theorem of FSN.

• If T is produced by A1, then T is 'E0' which has the form 'Eγ'; therefore T has one of the forms required by the theorem.
• If T is produced by IR1, then T has the form 'E0α' which has the form 'Eγ', that is, one of the forms required by the theorem.
• If T is produced by IR2, then T has the form 'E1α' which has the form 'Eγ', that is, one of the forms required by the theorem.
• If T is produced by IR3, then T has the form '¬Eβ1' which has the form '¬Eγ', that is, one of the forms required by the theorem.

Since T has the desired property in all cases, MT1 holds.
□

---

Notice that we did not need an inductive hypothesis in this proof because the conclusion of each inference rule clearly satisfies the needed property regardless of whether its premise does.

Now, let's define three properties P, Q and R of T. We say that:

• P(T) is true if T starts with the symbol 'E' and ends with the symbol '0'.
• Q(T) is true if T starts with the symbol '¬' and ends with the symbol '1'.
• R(T) is true if and only if exactly one of P(T) and Q(T) is true.

We can easily prove the following meta-theorem about FSN:

[MT2]  For every theorem T of FSN, R(T) is true.

---

Proof of MT2 by structural induction: Let T be any theorem of FSN.

• Basis step: T is produced by A1
• T is 'E0' which starts with the symbol 'E' and ends with the symbol '0'; therefore R(T) is true in this case.
• First inductive step: T is produced by IR1
• Inductive hypothesis: Assume that R(Eα) is true
• Q(Eα) must be false since 'Eα' does not start with '¬'. Thus P(Eα) must be true and α must end with the symbol '0'. Therefore,  T  has the form 'E0α' which starts with the symbol 'E' and ends with the symbol '0'; therefore R(T) is true in this case.
• Second inductive step: T is produced by IR2
• Inductive hypothesis: Assume that R(Eα) is true
• Q(Eα) must be false since 'Eα' does not start with '¬'. Thus P(Eα) must be true and α must end with the symbol '0'. Therefore,  T  has the form 'E1α' which starts with the symbol 'E' and ends with the symbol '0'; therefore R(T) is true in this case.
• Third inductive step: T is produced by IR3
• Inductive hypothesis: Not needed here
• T  must have the form ¬Eβ1. Thus Q(T) is true and, therefore, R(T) is also true in this case.

Since R(T) is true for all theorems T of FSN, MT2 holds.
 □

---

Finally, it is only one short step from MT2 to ...

[MT3] FSN is consistent.

---

Proof of MT3 by contradiction:

Assume that FSN is not consistent.

By definition of (in)consistency, there must exist two theorems of FSN of the form T and ¬T. Since ¬T starts with a negation symbol, this theorem must, by MT1, have the form  '¬Eγ' where γ is a non-empty sequence of 0's and 1's. According to MT2, γ must end with the symbol '1' (to satisfy property Q). Therefore, ¬T must have the form ¬Eβ1. But then T must have the form Eβ1, which contradicts MT2 (since neither P(Eβ1) nor Q(Eβ1) is true). 

In conclusion, FSN is consistent.

 □

---