ronse@prlb2.UUCP (Christian Ronse) (09/30/87)
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}jserembu@sjuvax.UUCP (J. Serembus) (10/02/87)
In article <362@prlb2.UUCP> ronse@prlb2.UUCP (Christian Ronse) writes: > 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. This seems to me to be a fairly ambiguous and inaccurate way of describing what takes place when one has an axiom system along with a rule or rules of inference. Theorems are those statements which are derivable or provable from the axioms or other theorems by means of the rules of inference. At this level they should not be referred to as true. It is only when one is concerned with semantics that the notion of truth comes into play. One of the major tasks of anyone working with a logic of the kind in question is to try to determine if the set of all statements flagged as `derivable` or `provable` by the deductive apparatus (syntax) is coextensive with the set of all statements flagged as `true` or `valid` by the semantics. In essence, Goedel showed that they are not coextensive. There are statements that fall into the latter set but not the former. Or, to put it naively, there are "more" statements in the latter set than in the former one. Or yet again, The former set is a proper subset of the latter one.