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

[Richard Zach]

On Tue, 2003-06-17 at 00:26, Torkel Franzen wrote:
> The
> completeness theorems, on the other hand, depend essentially on
> introducing convoluted non-standard definitions of the axioms of
> theories.

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?

>  >Incidentially, I found the use Shapiro made of these results in his
>  >paper "Incompleteness, mechanism, and optimism"  (BSL 4 (1998) p 273;
>  >online at <http://www.math.ucla.edu/~asl/bsl/0403/0403-002.ps>) quite
>  >intriguing.
> 
>   I don't think Shapiro makes any actual use of the completeness results
> in his discussion. He does comment that

I should have said "I find it intriguing that Shapiro discusses
transfinite progressions in discussing Lucas".  I can't tell from the
paper if Lucas actually discusses transfinite progressions of theories
or just suggests something like it, and it was Shapiro who brought in
Turing/Feferman's work to make the idea precise.  Either way, I think
it's useful to do just that: make the idea of iterating the addition of
Goedel sentences precise, and then show that one can't get philosophical
mileage out of that.

>     The Feferman result entails that
>     if a human can iterate the members of O (or if she can decide
>     membership in O) then she has the wherewithal to determine the
>     truth value of every arithmetic sentence. All she has to do is
>     systematically generate the outputs of R(n) for each n in O, using
>     the Feferman reflection principle.
> 
> but we don't need Feferman's completeness result for this, since O was known
> to be Pi-1-1-complete before that result. 

But you need a connection between O and progressions of theories to get
the equivalence between "can tell if d is in O" and "is provable in
A_d".  

<snip>

>   About Turing's completeness result, Shapiro says
> 
>    He [Turing] showed that for the simple reflection principle Con-A,
>    if F is a true Pi-1-sentence, then there is an n in O (which can
>    be found effectively from F) such that |n|=w+1 and F is among the
>    theorems of R(n). This astounding result is that there is a way
>    to iterate the Gdel construction on theories, beginning with A,
>    so that when we collect together the finite iterations and take one
>    more Gdel sentence, F is decided.
> 
> This description is misleading in that it suggests that the infinitely
> many axioms Con-T, Con-(T+Con-T),.. of the final theory somehow play
> a role in proving F, whereas in fact they're not used at all, and
> the sequence proceeds to w+1 simply because it is only at limit
> ordinals that non-standard definitions of the axioms of a theory can
> be introduced, when we base the sequence on a recursive progression
> (or ordinal logic). Turing's construction is no more epistemologically
> relevant than the "collapsed" version which goes from T to T+Con-T,
> with F provable in T+Con-T.

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.

>   I don't think it's a weakness of Shapiro's paper that it doesn't make
> any actual use of the completeness theorems - I don't see how they could
> be used in a philosophical discussion concerned with what we know or
> can know in mathematics.Do you think *autonomous* progressions of theories can be so used, as in Kreisel's analysis of what can be known (ie, proved) finitistically?

-Richard
-- 
Richard Zach ...... http://www.ucalgary.ca/~rzach/
Assistant  Professor,   Department  of  Philosophy
University of Calgary, Calgary, AB T2N 1N4, Canada