Formally self-referential propositions for cut free classical analysis and related systems
G. Kreisel ; G. Takeuti
GDML_Books, (1974), p.

CONTENTSIntroduction............................................................................................................................................................................................................ 5  I. Results on self-referential propositions............................................................................................................................. 11    1. Definitions of some principal metamathematical notions................................................................... 11    2. Results concerning the notions of Section 1 for cut free classical    analysis and related systems........................................................................................................................ 16  II. Formalized metamathematics of C F A.............................................................................................................................. 24    1. Completeness and reflection principles for closed 00q0 formulae..................... 24    2. Demonstrable instances of the normal form theorem......................................................................... 28    3. Demonstrable instances of deductive equivalence and of the fundamental conjecture............... 32  III. Discussion of some general issues raised in the introduction................................................................................... 34    1. Hilbert’s programme.................................................................................................................................... 34    2. C F A and the structure of proofs in analysis.......................................................................................... 36    3. Henkin’s problem [6] and the relation of synonymity............................................................................. 41  Appendix. Addenda to the literature......................................................................................................................................... 44    1. Jeroslow’s variant of literal Gödel sentences......................................................................................... 44    2. Löb’s theorem............................................................................................................................................... 44    3. Rosser variants............................................................................................................................................ 46  References.................................................................................................................................................................................. 49

EUDML-ID : urn:eudml:doc:268467
@book{bwmeta1.element.zamlynska-23b1447d-c2c3-4004-849e-d24eec516eb8,
     author = {G. Kreisel and G. Takeuti},
     title = {Formally self-referential propositions for cut free classical analysis and related systems},
     series = {GDML\_Books},
     publisher = {Instytut Matematyczny Polskiej Akademi Nauk},
     address = {Warszawa},
     year = {1974},
     zbl = {0336.02027},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.zamlynska-23b1447d-c2c3-4004-849e-d24eec516eb8}
}
G. Kreisel; G. Takeuti. Formally self-referential propositions for cut free classical analysis and related systems. GDML_Books (1974),  http://gdmltest.u-ga.fr/item/bwmeta1.element.zamlynska-23b1447d-c2c3-4004-849e-d24eec516eb8/