Godel ad infinitum (was FOM: Truth of G)

[Torkel Franzen]

  Arnon Avron says:

  >One may say perhaps that con(T)
  >is not only true (in the standard model) iff T is consistent, but
  >in fact expresses this consistency. 

  This is clearly so e.g. if T is PA and we take Con(T) to be the
direct formalization of "there is no derivation in PA of a contradiction",
where a derivation in PA is defined e.g. as a finite sequence of
formulas, each of which is an axiom of PA or a logical axiom or
follows from earlier formulas in a sequence by a rule of inference.
The reason why this is unproblematic is that there is no difficulty
about how to formalize "x is an axiom of PA": we just formalize the
ordinary or canonical description of those axioms, a description which
has the form "x is one of the axioms a1,..,an or is an instance of
the induction schema".

  When we talk about arbitrary effectively axiomatizable extensions T
of PA, the situation is less straightforward, as we know at least since
Feferman's "Axiomatization of metamathematics...". There is no
canonical definition of the axioms of an arbitrary theory, and if we
just take any formula which does in fact (extensionally) define the
axioms of T and formulate Con(T) as above, the resulting Con(T) does
not in general "express the consistency of T" in any but the weak sense
that Con(T) is true if and only if T is consistent. In particular,
Con(T) may be provable in T itself. Feferman gave an example of this,
using a non-standard definition A(x) which defines the axioms of PA
computably in PA, i.e. A(k) is provable in PA if and only if k is
an axiom of PA. He also showed that a sufficient condition for the
proof of Godel's theorem to go through is that the axioms of T are
defined by an RE-formula, nowadays more perspicuously described as
a Sigma-formula, and the effectively axiomatizable theories are precisely
those whose axioms can be defined by such a formula.

  Thus when we refer to Con(T) for arbitrary effectively axiomatizable
extensions of PA, the best we can do is to stipulate that Con(T) is
formulated as above using some Sigma-formula which defines the axioms of
T. Godel's proof can then be carried out, showing that Con(T) is not
provable in T if T is consistent. However, the different Con(T) 
obtained from different Sigma-formulas defining the axioms of T are
not in general equivalent in T.

  In discussing Godel's theorem as applied to PA or ZFC or ACA_0 or any
other of the theories actually formulated in logic, Con(T) has no
problematic intensional aspects, since we have canonical definitions of
the axioms of those theories. But the problematic aspects become
prominent when we start to ponder the theories obtainable by iterating
ad infinitum the operation of extending a theory T by adding Con(T)
as a new axiom.

  Sequences of theories obtainable in this way by adding ad infinitum
consistency statements, or more generally reflection principles, have
been extensively studied in recent years by Beklemishev, and earlier
by Schmerl. Before that, the closely related notion of an "ordinal logic" was
introduced by Turing, whose work was taken very much further by
Feferman in his "transfinite recursive progressions". While the
Schmerl-Beklemishev work gives precise information about the relative
logical strength of iterated reflection principles, the Turing-Feferman
work contains a completeness theorem for progressions, and the notion
of an autonomous progression, intended to capture what can be
be proved on the basis of T by iterated extensions of this kind.

  Godel's theorem has captured the interest and imagination of people
in general like no other result in logic, and reflections on what
happens when you iterate ad infinitum the operation of adding
consistency statements also regularly occur to people who are not
logicians, in discussions touching more or less directly on
philosophy, artificial intelligence, logic. The formal details of such
iteration add many complications to the basic incompleteness theorem,
and as far as I know there isn't any exposition of the subject aimed
at the non-specialist.

  I'm just finishing an exposition intended to fill part of this gap,
in the form of a book of some 250 pages (with the title
_Inexhaustibility_), which presupposing no knowledge of logic gives a
presentation of iterated extensions by reflection, based on the
Turing-Feferman approach, together with a philosophical discussion of
the puzzling matter of the apparent inexhaustibility of our
mathematical knowledge (first commented on by Godel) which results
from the fact that any theory which we recognize as sound can be
extended to a stronger theory which we also recognize as sound. Part
of my purpose is also to make the completeness results of Turing and
Feferman, which seem to be little known and understood, comprehensible
to the general reader, both in what they achieve and in what they do
not achieve.

  This brings me to the main point of this posting. Although there is
nothing in the book which is essentially new on the technical side, I
do present various proofs and arguments which are only loosely based
on the literature, and which may contain oversights, mistakes, or
doubtful interpretations. The subject matter is demanding enough of
the reader as it is, and it would be unfortunate if the book also
contained direct mistakes. Since there are many on this list who are
well acquainted with the relevant technical aspects of the subject -
basic recursion theory, ordinal notations, formal arithmetic,
inductive definitions, partial truth definitions, and related matters -
I would like to present some such arguments and proofs on the list,
as a way of checking them out before trying to sell the final product
to the general public.