[FOM] Re: Progressions of theories (was: Consistency of formal systems)

[Torkel Franzen]

Richard Zach says:

 >I still don't quite understand what you mean by "convoluted non-standard
 >definitions of the axioms of a theory." Feferman's formula \alpha[z; x]
 >("x is the code of an axiom of A_z, the z-th system in the progression")
 >looks to me perfectly natural ("either z =1 and x is an axiom of A_1, or
 >z = y + 1 and x is an axiom of A_y or else is Con_{A_y}, or z is the
 >limit of w_u and for some w_u, x is an axiom of A_{w_u}; see p. 285). 
 >Surely the definition of the (codes) of ordinals is where the tricky
 >stuff happens?

Consider a sequence of theories of length omega obtained from a
progression. That is, we have a total recursive function {e} with
index e, such that {e}(0),{e}(1),... are notations for a strictly
increasing sequence of finite ordinals, which we may as well assume to
be 0,1,... . From the properties of progressions, we know that
provably in PA (where I write lim(e) instead of using Kleene's
3*5^e),

     A (code for a) formula satisfies alpha(lim(e),x) iff it satisfies
     alpha({e}(m),x) for some m.

We also know, from the assumption about e, that the formulas
satisfying alpha({e}(0),x), alpha({e}(1),x),...  are in fact, assuming
that we base the progression on PA, the axioms of
PA,PA+Con(PA),PA+Con(PA)+Con(PA+Con(PA)),... (with canonically
formulated consistency statements). But what we can prove in PA
about this depends on what we can prove about the notation e.

Turing, for his completeness proof, introduces (using the recursion
theorem) an e for which it is provable in PA that for every n

   {e}(n)=the canonical notation for the finite ordinal n,
          if F(k) is true for every k<=n, and otherwise 
          the successor-notation obtained from e.

Assuming (k)F(k) to be true, e is in fact a notation for omega, and
the formulas satisfying alpha(lim(e),x) are in fact the axioms of PA
together with the various consistency statements above. In terms of
theories, then, the sequence of theories PA=T_0,T_1,..,T_omega
obtained using our notation lim(e) is in fact a standard sequence of
iterated consistency extensions of PA. Now when we form the theory
with added axiom Con(T_omega), in which (k)F(k) is provable, the
formula we use to define the axioms of T_omega in expressing
Con(T_omega) yields a non-standard description of the axioms of
T_omega, in the sense that it is not in general equivalent in PA to
the canonical definition of the set of axioms of PA together with the
various consistency statements. (The non-standard description is "x is
a formula satisfying one of alpha({e}(0),x),alpha({e}(1),x),..", where
e is defined so as to satisfy the condition above.) The reason why we
can prove (k)F(k) in T_omega + Con(T_omega) is precisely that we are
using a weird description of the axioms of T_omega, incorporating
irrelevant conditions having to do with F, in asserting the
consistency of T_omega, and the reason why this weird description is
extensionally correct is that (k)F(k) is true.

Thus the trickery involved in choosing a suitably defined notation for
omega is equivalent to trickery in choosing a formula to define the axioms
of the theory T_omega when expressing Con(T_omega).

  >The proof that F is provable in the limit proceeds by showing that F is
  >equivalent to (roughly) Con_{T + Con_T + Con_{T + Con_T} + ...}.  It
  >seems to me that they, i.e., the axioms of the final theory, do play a
  >role.

There is no use made in the argument of the fact that the final theory
proves Con_T, Con_{T + Con_T}, and so on - these axioms just happen to
be part of the theory T_omega, and we need to introduce T_omega only
because we can't sneak in any nonstandard definition of the axioms of
a theory, using progressions, until we come to a limit ordinal - or at
the very beginning. If we aren't shy about introducing a peculiar
definition of the axioms of our starting theory T_0 (rather than of
the axioms of T_omega), we can collapse Turing's argument into what I
call in my "Inexhaustibility" ms

  The Pi-completeness observation (Turing): For any true Pi-1-sentence
  F, there is a Sigma-formula theta defining the axioms of T such that
  Con_theta [the formalization of "T is consistent" using theta to
  define the axioms of T] implies F in PA.

  >Do you think *autonomous* progressions of theories can be so used, as
  >in Kreisel's analysis of what can be known (ie, proved)
  >finitistically?

  I would say that autonomous progressions are highly relevant to
mathematical epistemology, and they play a central role in my book.

---
Torkel Franzen