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:

Absolute proofs of consistency and meta-mathematics

In earlier posts, we explained why consistency is an important property of axiomatic systems and discussed relative proofs of consistency, in which the proof of consistency of a system is based on the assumption that another axiomatic system is consistent. In this post, we introduce absolute proofs of consistency that do not make any assumptions about any other axiomatic system. Apparently, David Hilbert was the first to study and propose such proofs, according to Nagel and Newman's book (Section III, page 26).

Recall that an axiomatic system is consistent if it cannot derive both a theorem and its negation. What do we mean by the negation of a theorem? Let's take, as a simple example, the theorem: "6 is divisible by 3." Its negation is simply the following statement: "6 is not divisible by 3" or equivalently "It is not the case that 6 is divisible by 3." This second formulation of the negation, although less elegant in English, is preferable because the negation is added to the front of the original theorem. In a formal system, negation is handled by simply adding a symbol for the phrase "it is not the case that." Several symbols have been used for negation, such as ~ and ¬ . We'll use the latter here. So, if T is any theorem in some formal system, then the formula  ¬T is the negation of T.

Remember that our formal system FS did not have a symbol for negation. So we will extend FS into a new formal system called FSN (for FS with Negation), whose alphabet is { E, 0, 1, ¬ }. FSN has exactly one axiom, namely the same as A1 in FS. FSN also has the same inference rules as FS, namely IR1 and IR2. But it has one additional inference rule that uses negation. Here is the full description of FSN: