[FOM] Progressions of theories (was: Consistency of formal systems)
rzach at ucalgary.ca
Mon Jun 16 19:53:22 EDT 2003
On Sun, 2003-06-15 at 00:00, Torkel Franzen wrote:
> Richard Zach says:
> >The main results are that if you add Con and
> >iterate through O (ie, all constructive ordinals), you get all true
> >\Pi_1 sentences of arithmetic; same if you add local reflection
> >(Pr(\phi) -> \phi for all sentences \phi). If you iterate adding global
> >reflection ((\forall x)Pr(\phi(x)) -> (\forall x)\phi(x) for all
> >formulas \phi(x)) you get all true sentences of arithmetic.
> This is a bit misleading, since Feferman and Spector also showed
> that you can iterate uniform reflection through the constructive
> ordinals and not even get every true Pi-1-sentence. But you can also
> get all true sentences of arithmetic, by using certain convoluted
> non-standard definitions of the axioms of the theories involved when
> choosing notations for limit ordinals.
Yes, my bad. 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 Feferman/Spector paper is in JSL 27 (1962) p 383, if anyone cares.
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
> My forthcoming volume in the LNL series ("Inexhaustibility") includes
> an exposition, presupposing no prior knowledge of logic, of transfinite
> progressions of theories and the central argument of Feferman's paper.
I look forward to it.
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