Gregory Chaitin provides an elegant account of the Gödel result in his paper on The Berry Paradox (a cleaner variant on the smallest non-interesting number folly).

Gödel's Theorem

Gödel's contribution to the study of logic revolves around the discovery of a limitation on what one can sensibly seek from a logical system. Prior to his work, a great many mathematicians, vaguely headed by the likes of Bertrand Russel, were hard at work trying to prove consistency and completeness of the Zermelo-Fränkel formalism for set theory and logic, together with Peano's axioms for the natural numbers. In so far as they were able to believe that this might fail, they expected the failure to show them how to replace their formalism with one which would be consistent and complete. Gödel derailed this project in the most spectacular manner possible: he showed that any logical system capable of supporting Peano's axioms

The crucial technical terms of the discussion:

Peano's axioms
provide a formal description of the process of counting. They can be constructed in any logical system capable of the variety of counting in which any number has a successor – so that there is no last number – and distinct numbers have distinct successors.
Consistency
(of which the foolish variety is the hobgoblin of small minds) is that desirable property of a logical system which says that there are no statements which the system regards as both true and false.
Completeness
is the desirable property of a logical system which says that it can prove, one way or the other, any statement that it knows how to address.

What Gödel proved was that any finitely-presentable logical system which can support Peano's axioms can be obliged to address itself to a question of form this statement cannot be proven true, which I shall refer to as Gödel's fork. A complete logical system can prove any statement that it knows how to address, so it must be able to prove this statement; whether it proves it true or false, it thereby proves it to be also false and true; whence it is inconsistent. Thus no logical system which can support Peano's axioms can be both complete and consistent.

Specifically, in any logical system, consistency implies that Gödel's fork is undecidable – i.e. it cannot be proven either true or false; in particular that it cannot be proven true. But that it cannot be proven true is Gödel's fork. Therefore, consistency implies Gödel's fork. Consequently, any proof of consistency of a logical system (from within that system) is a proof of Gödel's fork in that system, which implies inconsistency in the system.

Consequently, any logical system which can make up its mind about its consistency can prove itself inconsistent (provided it can count – i.e. support Peano's axioms).

An illustrative paradox

It is likely this isn't quite rigorous: I haven't taken care over the Law of the Excluded middle and its cousins. I'll update when I've looked through the implications …

Here's a paradox to which my friend Jón Fairbairn introduced me. Formally, Gödel's fork has to be stated about a logical system as: Gödel's fork in a logical system L is the statement there is no proof in L that Gödel's fork in L is true. The fact that this statement cannot be proven true in L says nothing about its provability in some logical system which subsumes L. Furthermore, if it cannot be proven either true of false in L, as arises if L is consistent, one may take it, or equally its negation, as an extra axiom, add this to L and thereby obtain a logical system no less consistent than L.

Now, rather than adding Gödel's fork in L as an axiom, Jón pointed me to what happens when you add its contradiction. You obtain a logical system, M, consisting of L and the statement Gödel's fork in L is false. Now, of course, we expect Gödel's fork in M to be undecidable in M; but what does M now say about L and Gödel's fork in L ?

Curiously, the first thing we find is that M's extra axiom says that there is a proof in L that Gödel's fork in L is true. M does not in any way provide us with such a proof, it only says that one exists: and we have every right to decide that M is wrong in saying this, so long as we cannot find such a proof. But M doesn't care: it knows what it believes and it reasons from it. Inescapably, since M believes that L contains a proof of Gödel's fork in L, and M contains all the axioms and methods of reasoning open to L, M is able to deduce that L is inconsistent. This, in turn, leads it to a proof of its own inconsistency (since any inconsistency in L is in M).

Now, M is inconsistent precisely if there is some statement which M can prove both true and false. Yet we've enabled M to prove its inconsistency without actually exhibiting such a statement. If L was unable to prove its own inconsistency then it must, at least, have been unable to exhibit an inconsistency: in particular, it must have been unable to prove its own consistency. The undecidability of Gödel's fork in L would appear to imply that M's assumption about it leaves M no better able to exhibit an inconsistency. There consequently arises the fascinating possibility that it is, in fact, impossible to find any statement which M can prove to be both true and false. Given that it has proved itself inconsistent, this would require it to be unable to prove itself consistent, of course.

In this case, M would contain no inconsistencies and yet (consistently) believe itself to be inconsistent. Now, kiddies, can we really bring ourselves to say it's wrong about that ?

Exercise for the good-humoured student [with thanks to James Sheldon]: apply either the above or just Gödel's fork to the Marxist/dialectic system of logic. For further credit, see whether there is any logic at all to the capitalist system and, if different from the Marxist/dialectic system, subject it to the same analysis.

Sketch Proof

If your logical system can count, Gödel shows how one can formally number all the statements in your logical system; by showing how you can do this within the logical system itself, he equips us with the means to talk about this numbering (effectively) within the logical system (but with a more intelligible description than the implementation details); using this within the system, one can discuss the set of integers whose associated assertions are proven in the system; he then goes on to show that there must be an assertion (somewhere out there in that numbering) tantamount to Gödel's fork.

Exploration

As a way of evading confusion about what not means, I'm going to discuss the problem in terms of two processes, proof and disproof. [For some assertion A, the archetypical proof of A is a chain of logical inferences from True to A; the archetypical disproof of A is a chain of logical inferences from A to False; the latter constitutes a proof of A implies False, which may be viewed as the statement not A. But that is just the archetype that motivates my way of describing the matter.] This simplifies discussion of what consistency and completeness say: consistency just says that no assertion is both proved and disproved; completeness that each statement is either proved or disproved.

In order to proceed, I need to discuss inference's relationship with proof and disproof. The logical system's machinery for inference constitutes the means by which it transforms proofs and disproofs of given assertions into similar for other assertions. This gives rise to four inference operations, which I now pause to name (for the purposes of the present discourse, without prejudice to whether the logical system expresses itself in similar terms):

from a proof of A, the system is able to construct a proof of B
A implies B
from a proof of A, the system is able to construct a disproof of B
A forbids B
from a disproof of A, the system is able to construct a proof of B
A else B

Note that this isn't a symmetric combination of A and B: as a clue to which I resisted the temptation to call this A or B. As a synonym, think of this as B unless A: unless is the transpose of else.

from a disproof of A, the system is able to construct a disproof of B
B demands A

Note the reversal of order; archetypically, this would be the same as B implies A.

To enable us to perform inference, we must now consider how we may combine individual steps. The definitions suffice to tell us the following:

A implies B and B implies C implies A implies C

a proof of A supplies us with one of B, which will supply us with one of C.

A implies B and B forbids C implies A forbids C

(likewise)

A forbids B and B else C implies A implies C

any proof of A gives us a disproof of B; from which we construct a proof of C.

A forbids B and C demands B implies A forbids C

from proof of A, build disproof of B; whence build disproof of C.

A else B and B implies C implies A else C

disproof of A yields proof of B, whence we infer C.

A else B and B forbids C implies C demands A

disproof of A yields proof of B, whence disproof of C

B demands A and B else C implies A else C

disproof of A yields disproof of B, whence proof of C.

B demands A and C demands B implies C demands A

disproof of A yields disproof of B, whence disproof of C.

of which the last may be re-phrased (by shuffling the assertions' names) as
A demands B and B demands C implies A demands C

as should be no surprise given the kinship between demands and implies.

by use of unless in place of else we can re-write another as:
A unless B and B demands C implies A unless C

so, just for reference, here's what we get if we re-write the other else cases in terms of unless:

A forbids B and C unless B implies A implies C
B unless A and B implies C implies C unless A
B unless A and B forbids C implies C demands A
Note that even with both unless and else we can't escape from some reversals of the easy reading, and I suspect I shall find it more practical to use only one of unless and else: so for the present, I'll take unless to tidy up the broken symmetry induced by my naming (for reasons of intuitive convenience – demands feels like a synonym of implies, as the above dynamics shows). Proofs get picked up from the left (by imply and forbid) while disproofs are gathered from the right (by unless and demands); according as what is produced is a Note that forbids only arises as conclusion if given as one of the premises; similarly, unless or else don't arise naturally – where demands and implies do, by appearing as the results of combining unless with forbids

This page is unfinished; it degenerates into fragments from here onwards.

Slogans:

I want to use Gödel's numbering of the available assertions to encode the above assertions as statements in the logical system. Candidate rules: If A implies B, D implies C and B disproves C, then A disproves D disproof of (there is a disproof of A) A implies B: not(A) or B A disproves B: not(A) or not(B); not(A and B); B disproves A A disproves B if, from any proof of A, the system can construct a disproof of B from a proof of B, can we then construct a disproof of A ? what, in general, will the logical system let me build out of a disproof of A ? a chain of inferences from any statement to a disproof of A constitutes a disproof, by that statement, of A. M disproves Z and A implies M and P implies Z infer A disproves P M !> Z and A => M and P => Z implies

Examine the collections, P and D, of integers whose associated assertions are proved and disproved, respectively, by the system. Within the system itself we can define and manipulate these collections of integers; we can thus, within the system, have statements asserting that particular integers are and are not in these collections; the fork materialises as an integer, n, for which the associated assertion reads as the index of n is in P is in D.

Let m be the index of n is in P, read n's fork as m is in D, hence read m's assertion as index(m is in D) is in P. It may help to think of index(A) is in D as not(A), for any given assertion A. Note that index(A) is in P asserts that A is proven, so implies A; and that any proof of A will imply that A's index is in P (but it'd take completeness to make A imply index(A) in P). Consistency says that no integer is in both P and D; completeness says that each integer is either in P or in D.

So, is n in P ? Is m in D ?

Now, m in P implies m's assertion, n in P; n in P says that the associated assertion, our fork, is proved by the system; so it implies the fork; which asserts m is in D. However, m is in D says that m's associated assertion, n in P, is disproved by the system. Thus m in P implies n in P implies m in D which contradicts n in P. This clearly gives us inconsistency if m is in P. Any proof of n in P, supplies a disproof of n in P; consequently m, the index of n in P, would be in both P and D; so any proof of n in P implies inconsistency; whence so does any proof of the fork (since

Now, completeness asserts m in D or m in P; the fork is m in D and we have already seen that m in P implies the fork; fork or fork implies fork; so completeness implies the fork. Thus any logical system which can prove its own completeness is able to prove the fork, which will make n be in P, which will lead to an inconsistency: a logical system which can prove its own completeness is inconsistent, ane one which can't prove its own completeness is incomplete (the example unproven assertion being completeness itself).

which will give us inconsistency if n and m are both in D. So our choices are down to:

Valid CSSValid HTML 4.01 Written by Eddy.