[FOM] Re: Progressions of theories (was: Consistency of formal systems)
Richard Zach
rzach at ucalgary.ca
Tue Jun 17 14:48:20 EDT 2003
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
More information about the FOM
mailing list