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:

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

Notice that the new rule of inference takes any theorem (the premise) starting with E and ending in 0 and produces a new theorem that results from adding a negation symbol in front of the E and replacing the final 0 with a 1.

Can FSN produce all of the theorems that FS produces? Does FSN produce new theorems? If so, which form do these new theorems have? And, most importantly, ...

... is FSN consistent?

And if so, can we come up with an absolute proof of consistency?

The first step in an absolute proof, as envisioned by Hilbert, is to completely formalize the axiomatic system whose consistency we want to prove. Since FSN is already formalized, we can skip this step here.

However, classical axiomatic systems, such as Euclidean geometry, were not formalized. As shown above, a formal system is comprised of axioms and inference rules, each of which is built out of strings of meaningless symbols according to purely formal or syntactical rules. The main advantage of formalized axiomatic systems is that all logical steps are explicit and no hidden assumptions can creep in. In contrast, Euclidean geometry stated its axioms and theorems using informal and meaningful language (Greek). In addition, its inference rules were not formalized, allowing for unstated assumptions and implicit inferences. Since these are not allowed in a rigorous proof, we must get rid of them by formalizing the axiomatic system.

The second step in an absolute proof of consistency is to prove that the formalized axiomatic system can never produce (i.e., prove) a theorem and its negation. Since the way theorems are produced is completely mechanical, based on explicit and unambiguous symbol manipulations, it may be possible to build a rigorous proof of consistency by studying the formal system from the outside.

At this point, it is important to distinguish reasoning that takes place within the formal system from reasoning that takes place outside the system.

Reasoning within the system is limited to asserting axioms and applying inference rules. This reasoning, as discussed before, is purely syntactic and meaningless. Here are a few "sentences" that can be generated within the system:

1. E0
2. E00
3. E10
4. ¬ E1
5. ¬ E101

Now, what kind of reasoning are we going to need to prove that our formal system FSN is consistent (assuming that it is)? Clearly, the theorems of FSN cannot prove the consistency of FSN. The theorems of FSN are meaningless strings of symbols. They are not about anything. They cannot say anything about FSN. Therefore, they cannot say that FSN is consistent.

To prove the consistency of FSN, we need to reason about the whole set of theorems of FSN. If the proofs obtained within FSN constitute a kind of (formal) reasoning, then reasoning about this reasoning is called meta-reasoning. Proving that FSN cannot prove both a theorem and its negation requires meta-reasoning. Here are some examples of statements about FSN that might result from meta-reasoning:

1. The theorem 'E110' is derivable from the axiom 'E0' by two applications of IR2.
2. The symbol 'E' appears exactly once in each theorem of FSN.
3. '¬E100' is not a theorem of FSN.
4. FSN is consistent.
5. FSN is not consistent.

Hopefully, by now, you have figured out which one of statements 4 and 5 above is true.

Now, we can step back from our made-up formal system and consider the kind of formal systems that Hilbert was interested in. These formal systems, of course, focused on mathematics and included Whitehead and Russell's Principia Mathematica as well as Giuseppe Peano's formal system for arithmetic. The reasoning within these formal systems model mathematical reasoning. Therefore, statements about these formal systems are about mathematics. They are part of meta-mathematics. So, the question whether one of these systems is consistent is part of meta-mathematics.

Let's wrap-up with one more important feature of these formal systems: they contain a finite number of axioms (or axiom schemata) and a finite number of inference rules (or reasoning patterns). Why does this matter? Remember how the model-based approach to proving consistency suffered from the impossibility of inspecting all of the elements of an infinite model (e.g., a model for arithmetic would have to include an infinite set of elements to be mapped to the set of natural integers).

With the absolute approach proposed by Hilbert, there is no need for a model. Instead, in this framework, the proof of consistency is based solely on the study of a formal system, which is fully defined by a finite number of patterns of reasoning. This is the crux of the argument. Reasoning about an infinite domain of knowledge (such as arithmetic) is reduced to the study of a finite formal system. If possible, this approach would satisfy Hilbert's quest for so-called finitary or finitistic methods.