[FOM] Consistency of formal systems

[Torkel Franzen]

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.

  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.

  By the way, Feferman was recently awarded the Schock prize by the
Swedish Academy of Sciences "for his works on the arithmetization of
metamathematics, transfinite progressions of theories, and
predicativity".

(http://www.kva.se/KVA_Root/eng/_news/detail.asp?NewsId=353)
---
Torkel Franzen