[FOM] Re: Progressions of theories (was: Consistency of formal systems)
torkel at sm.luth.se
Tue Jun 17 02:26:24 EDT 2003
Richard Zach says:
>Correct me if I'm wrong though, but my understanding was
>that the incompleteness is not a result of "using certain convoluted
>non-standard definitions of the axioms" but on the choice of paths
>through O along which the progressions of theories are considered. In
>particular, the phenomenon is not (directly) related to the "convoluted
>non-standard" definitions of consistency formulas which are provable
>(familiar from Feferman's "Arithmetization of metamathematics ...") --
>or is it?
The incompleteness result of Feferman and Spector is very general
and only depends on the existence of Pi-1-1 paths through O - the
details of how theories are defined don't enter into it. The
completeness theorems, on the other hand, depend essentially on
introducing convoluted non-standard definitions of the axioms of
theories. Unlike the kind of non-standard definitions given in
"Arithmetization..." these are still given by Sigma-1-formulas, so
Gödel's incompleteness theorem applies.
>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
I don't think Shapiro makes any actual use of the completeness results
in his discussion. He does comment 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. He also says, referring
to the completeness results,
The key to wielding these results is the ability to decide membership
in O, or to find effective notations for recursive ordinals generally.
but doesn't actually indicate any wielding of the results. What is
relevant to the discussion is rather the general fact that a theory
R(n) (using Shapiro's notation) in a sequence of extensions by
reflection formalizes part of our (potential or implicit) mathematical
knowledge if we know n to be a notation for an ordinal.
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 Gödel construction on theories, beginning with A,
so that when we collect together the finite iterations and take one
more Gödel 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.
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.
More information about the FOM