Only So Much We Can Prove

In the 19th century, many paradoxical statements, formed either in natural language or mathematics, caused concern leading to questions around the reliability of mathematical reasoning. Rigorous attempts were made to address such concerns.

One of the most notable works in this regard is Principia Mathematica, written by Alfred North Whitehead (1861–1947) and Bertrand Russell (1872–1970) in the early 1900s, with one of its primary goals as “solving paradoxes that plagued logic and set theory”. This was a bold attempt to summarize the foundations of mathematics. The idea was to get rid of paradoxes by getting rid of self-references and in efforts to make this happen, type theory was developed. Type theory essentially placed constraints on mathematical grammar, thereby disallowing the formation of ill-formed sets discussed in the likes of Russell’s Paradox.

Let R be the set of all sets that are not members of themselves. If R is not a member of itself, then its definition dictates that it must contain itself, and if it contains itself, then it contradicts its own definition as the set of all sets that are not members of themselves.

And finally, the claim that no self-referential statements can be constructed using the theory of Principia Mathematica was made.

Axioms, Rules, and Theorems

Let’s discuss a bit about formal systems, first. A formal system also referred to as an axiomatic system, is basically defined by

• a set of symbols
• a grammar that dictates how to put the symbols together to form statements (well-formed formulas, or WFF for brevity).
• a set of WFFs called axioms that are simply assumed to be true.
• a set of rules of inference, that dictate the transformation of axioms into new WFFs that are also true.

For a statement to be a WFF, it should be constructed by following the system’s grammar. It is an ill-formed formula, otherwise. Each WFF is either true or false. Applying rules of inference on WFFs give us WFFs. A rudimentary example of a WFF:

843 is a prime number.

For any WFF S, a proof of S (if exists) is a sequence of WFFs starting with an axiom and ending with S obtained using the inference rules. When such proof exists, S is referred to as a theorem.

Truth and Provability

We will now look at two desired properties of any formal system.

All provable statements must be true.

This property is called soundness and soundness implies the consistency of a system. Consistency means to not have any statement be proved both true and false.

All true statements must be provable.

This property is called completeness.

Essentially, we want truth and provability to be equivalent.

Fun question: If you could satisfy only one of completeness and consistency, which one would you pick?

Fibonacci Numbers vs Collatz Numbers

A little detour to explore two properties of numbers: Fibonacci numbers and Collatz numbers.

Fibonacci numbers start from 0 and 1 and are further defined as the sum of the last two numbers. The following are examples of Fibonacci numbers: 5, 8, 987, 1597. Given any number, say 233, it is easy to determine if it’s a Fibonacci number. We simply start from 0 and 1 and add repeatedly until we reach 233 or overshoot 233. In a sense, we have a well defined straight path from 0 and 1 to 233. Even for incredibly large numbers, the path is well defined, albeit longer.

On the other hand, Collatz numbers start from 1 and are further obtained either by doubling the number or by subtracting 1 and dividing by 3 (if such operation results in a positive integer). The following are examples of Collatz numbers: 1, 2, 4, 82, 484. To find if a number, say 24, is a Collatz number, we start from 1 and at each step, we either double it or subtract 1 and divide by 3 until we reach 24. How would we ever know if 24 is not a Collatz number? We can’t rely on overshooting in this case, since we are allowed to subtract 1 and divide by 3 which results in reducing the number. The “path” isn’t well defined and we cannot determine if a given number is a Collatz number easily, simply because we don’t know when to give up on the search.

Well-Formed Formulas vs Theorems

Why did we just talk about Fibonacci and Collatz numbers? Well, it’s because the nature of these properties is similar to the nature of well-formed formulas and theorems.

Well-formed formulas are similar to Fibonacci numbers, in the sense that given a statement, it is easy to check if the statement is a WFF using the grammar rules of the formal system. The “path” to well-formedness is straightforward.

Theorems, on the other hand, are similar to Collatz numbers. The inference rules make it difficult to check if a statement is a theorem because there are many zig-zag routes and it’s not quite clear which path will lead us to the theorem. The path in the case of a theorem is essentially the theorem’s proof.

WFFs and Theorems are formal properties of a statement. One is easy, predictable and trivial. The other is unpredictable and elusive.

Gödel’s Encoding

Kurt Gödel (1906–1979) came up with a clever encoding scheme where he uses prime factorization to encode statements in Principia Mathematica. The idea is that the integers could easily simulate complex structures and objects.

In this encoding scheme, each symbol in the grammar is assigned a unique natural number and by raising primes to use these unique numbers as powers, we get the unique encoding for each sentence.

Consider the statement S: 1+1=2, which can be encoded as shown below.

Each statement in Principia Mathematica has a unique encoding. The inference rules are encoded as numerical operations so that they can work on the encoded statements. Asking questions about the encodings would mean asking questions about the statements in Principia Mathematica.

The whole of Principia Mathematica can be expressed using numbers and numerical operations. There are numbers representing statements and operations on numbers that transform the numbers according to the rules of inference. There is a perfect one-to-one correspondence between statements and numbers and the correspondence is held even after applying the operations.

For any given statement, we encode it and ask questions as follows. Is the integer a well-formed formula? Is the integer a theorem? We just reduced the formal properties of statements in Principia Mathematica into number-theoretical properties.

To check if an integer is a WFF number, we try to factorize it into primes and obtain the sequence of integers associated with the symbols and check the grammar rules to see if it’s a WFF. WFF numbers are very much like Fibonacci numbers. Checking if a number is a WFF number is easy and to continue the analogy, the path to a WFF is clear and straightforward.

On the other hand, checking if an integer is a theorem number is similar to the likes of checking if an integer is a Collatz number. It’s not quite clear which axiom numbers to start from, which inference rule operations to apply to reach the theorem number and we simply don’t know when to give up on the search for this integer. The path is zagged and unclear.

The Dreaded Self-Reference and Associated Paradoxes

The incredible efforts of Russell and Whitehead to prevent self-references creep into Principia Mathematica were to be deemed futile. Using the clever coding scheme one can construct a well-formed formula which essentially says:

24789102 is a prime number.

The number 24789102 is arbitrary but the idea holds. This number is such that the encoding of the statement G is the number itself.

And this is it! We have a statement in Principia Mathematica that speaks about itself. The dreaded and disconcerting self-references are discovered in Principia Mathematica putting its reliability in jeopardy. Did Russell and Whitehead miss something? Or is type theory to be blamed? We’ll seek the answer in a while.

We only showed that Principia Mathematica is capable of self-referential statements. The final nail in the coffin would be to show the presence of paradoxical statements. To show a paradoxical statement, we construct another self-referential statement, G:

43311341 is not a theorem number.

This too is a self-referencing statement. The number 43311341 is the encoding of the statement G itself. The statement G is basically saying:

This statement is not a theorem.

So is G a theorem? Let g be the encoding of the statement G. There are two possibilities:

• If G is true, then g is not a theorem number (follows from what the statement says). But since G is true, g should be a theorem number (follows from the character of encoding). We have a contradiction.
• If G is false, then g is a theorem number (follows from what the statement says). But since G is false, g should not be a theorem number (follows from the character of encoding). We have a contradiction.

Both possibilities lead us to inconsistency. We cannot have as the foundations of mathematics, a system where there are statements that are both true and false!

The only way to resolve this inconsistency is to give up the equivalency of truth and provability. If G is not provable, then g is not a theorem number (follows from what the statement says). G remains true but unprovable!

This is the price we pay for the consistency of Principia Mathematica. There are going to be statements that are true but unprovable! So, the property of completeness — that all true statements must be provable, is compromised to retain consistency.

Kurt Gödel’s achievement in modern logic is singular and monumental — indeed it is more than a monument, it is a landmark which will remain visible far in space and time. … The subject of logic has certainly completely changed its nature and possibilities with Gödel’s achievement.

— John von Neumann

Maybe It is Just Principia Mathematica?

Unfortunately, it’s not just Principia Mathematica. These results apply to any sufficiently rich formal system. To justify intuitively, rich formal systems are representationally powerful and therefore can form sentences that talk about themselves making self-references and paradoxes inevitable. Since we do not want to compromise on the consistency of the system, we sacrifice completeness.

This post is largely based on this elegant lecture by Douglas Hofstadter.

Edit: Many thanks to Emmanuell Tshim for pointing out a couple of mistakes in my post.