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 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

- could not be both consistent and complete; and
- could not prove itself consistent without proving itself inconsistent.

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 petty 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).

*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.

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.

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 thisA or B

. As a synonym, think of this asB unless A

:unless

is the transpose ofelse

. - 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

andB implies C

impliesA implies C

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

A implies B

andB forbids C

impliesA forbids C

(likewise)

A forbids B

andB else C

impliesA implies C

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

A forbids B

andC demands B

impliesA forbids C

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

A else B

andB implies C

impliesA else C

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

A else B

andB forbids C

impliesC demands A

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

B demands A

andB else C

impliesA else C

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

B demands A

andC demands B

impliesC 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

andB demands C

impliesA demands C

as should be no surprise given the kinship between

demands

andimplies

.- by use of
unless

in place ofelse

we can re-write another as: A unless B

andB demands C

impliesA unless C

so, just for reference, here's what we get if we re-write the other

else

cases in terms ofunless

:A forbids B

andC unless B

impliesA implies C

B unless A

andB implies C

impliesC unless A

B unless A

andB forbids C

impliesC demands A

- Note that even with both
unless

andelse

we can't escape from somereversals

of the easy reading, and I suspect I shall find it more practical to use only one ofunless

andelse

: so for the present, I'll takeunless

to tidy up the broken symmetry induced by my naming (for reasons of intuitive convenience –demands

feels like a synonym ofimplies

, as the abovedynamics

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 thatforbids

only arises as conclusion if given as one of the premises; similarly,unless

orelse

don't arise naturally – wheredemands

andimplies

do, by appearing as the results of combining unless with forbids

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

Slogans:

- implies after implies = implies
- imply what forbids to forbid
- forbid an unless to imply what must otherwise arise
- forbid what's demanded to forbid whatever demands it
- unless's constraint propagates rightwards along implication
- unless forbiden, demand
- unless's constraint can delegate to its demands (unless demands, unless)
- one demands what's demanded by what one demands

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:

- inconsistency, if either n or m is in P,
- inconsistency, if both n and m are in D, or
- incompleteness, if either n or m is in neither P nor D.