Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!mnetor!uunet!mcvax!prlb2!ronse
From: ronse@prlb2.UUCP (Christian Ronse)
Newsgroups: sci.math,sci.philosophy.tech
Subject: G"odel made easy (Part I)
Message-ID: <362@prlb2.UUCP>
Date: Wed, 30-Sep-87 05:40:50 EDT
Article-I.D.: prlb2.362
Posted: Wed Sep 30 05:40:50 1987
Date-Received: Sat, 3-Oct-87 08:23:11 EDT
Organization: Philips Research Laboratory, Brussels
Lines: 79
Keywords: G"odel's incompleteness theorem
Xref: mnetor sci.math:2169 sci.philosophy.tech:497


There has sometimes been discussions concerning the relevance of G"odel's
incompleteness Theorem (for example in sci.philosophy.tech on `uncertainty in
the real world'). The common understanding states that G"odel proved that in
any system of axioms powerful enough to derive integer arithmetic, there are
unprovable statements whose negation is also unprovable. In fact, this is not
exactly the matter. That Theorem does not speak of `unprovable' statements.

The title of G"odel's 1931 paper, translated in English, reads as:

``On Formally Undecidable Propositions of Principia Mathematica and Related
Systems, I''.

(G"odel intended to write a second paper ``---,II'' in order to justify
himself, but that was not necessary). The title does not say `unprovable', but
`formally undecidable'. What does that mean? G"odel was concerned with formal
systems of axioms, such as the Principia Mathematica by Russel and Whitehead,
and propositions that can be formally derived from them by a mechanical
application of the rules of inference of formal logic. So, given these axioms
and rules of logical inference, one can derive statements called theorems.
These theorems are of course true statements within that axiomatic system, but
they do not necessarily coincide with all true statements, even not with all
`provable' statements. Indeed, G"odel's _tour_de_force_ consists in getting
out of the axiomatic system, and proving results about it. One gets thus
statement which are not mechanically derived from that formalism, but which
can nevertheless be proved to be true. Thus they are `formally undecidable',
but `extra-formally provable'.

G"odel's Theorem states _grosso_modo_ that:

Every omega-consistent axiomatic system powerful enough to express arithmetic
contains a formally undecidable proposition.

Let us explain these terms. Let X be a statement (a well-formed expression
according to the rules of syntax for expressions); write ~X for the logical
negation of X. Given a system of axioms and rules of logical inference, we
will write Theorem(X) if X can be derived from the axioms by these rules of
inferences. Then the system is _inconsistent_ if we have

	Theorem(X) and Theorem(~X) for some X; 

otherwise it is _consistent_. On the other hand, the system is
_omega-inconsistent_ if we have a statement X(n) with a free integer variable
n (in other words where the variable n is not quantified by `for all' or
`there exists'), such that we have

	Theorem(there exists n, X(n)), and for every n, Theorem(~X(n));

otherwise it is _omega-consistent_. As the fact that ``for every n,
Theorem(~X(n))'' is weaker than ``Theorem(for every n, ~X(n))'',
omega-inconsistency is weaker than consistency, in other words
omega-consistency is stronger than consistency.

A statement X is _formally_undecidable_ (in that system of axioms and rules of
inferences) if we have neither Theorem(X) nor Theorem(~X). This does not mean
that X or ~X is unprovable by other means (for example by mathematical
arguments applied to that formal system).

G"odel studied an axiomatic system as a kind of grammar for combining symbols
into expressions, and coded these symbols and expressions by numbers. The
formal rules for logical inferences became thus number-crunching rules for
modifying these numerical codes. (This is a bit like what is done in modern
computers, but in 1931 that seemed quite extraordinary). He obtained by some
hocus pocus an an arithmetical statement G, which meant in terms of the
number-crunching rules for the codes, that a given code C could not be
obtained from the codes of the axioms, in other words that a given statement
corresponding to C could not be derived from the axioms. Now by computing the
code of G, one obtains C! Thus statement G is equivalent to the fact that G
itself cannot be derived from the axioms by the rules of logical inference.

In a next posting, I will describe in more details G"odel's code and the way
the statement G is obtained. The significance of G will be considered in a
third posting.

Follow-ups and queries to sci.math. I don't read sci.philosophy.tech anymore.

----------------------------------------
Christian Ronse		maldoror@prlb2.UUCP
{uunet|philabs|mcvax|...}!prlb2!{maldoror|ronse}