CONTENTS Introduction............................................................................................................................................................................................................ 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 $∑^0_0$ ∪ $∑^0_q$ 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
[1] D. de Jongh, Formulas of one propositional variable in intuitionist arithmetic, Fund. Math, (to appear).
[2] S. Feferman, Arthmetization of metamathematics in a general setting, ibidem 40 (1960), p. 35-92.
[3] J-Y. Girard, Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types, Proc. second Scand. Logic Symp., Amsterdam 1971, p. 63-92.
[4] J-Y. Girard, Three-valued logic and cut elimination: the actual meaning of Takeuti's conjecture, to appear.
[5] K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. I, Monatsh. Math. Phys. 38 (1931), p. 173-198.
[6] L. Henkin, Problem, JSL 17 (1952), p. 160.
[7] D. Hilbert and P. Bernays, Grundlagen der Mathematik I, second edition, Berlin 1968.
[8] D. Hilbert, Grundlagen der Mathematik II, second edition, Berlin 1970.
[9] R. J. Jeroslow, Redundancies in the Hilbert-Bernays derivability conditions for Gödel's second incompleteness theorem, JSL 38 (1973), p. 369
[10] G. Kreisel, On a problem of Henkin's, Indag. Math. 16 (1953), p. 405-406.
[11] G. Kreisel, Mathematical logic, in: Lectures on Modern Mathematics (ed. T. L. Saaty), vol. Ill, New York 1905, p. 95-195.
[12] G. Kreisel, A survey of proof theory, JSL 33 (1908), p. 321-388. ([9] exludes alternative (i) on p. 332 of footnote (6) by showing that Z' does not prove its own consistency.)
[13] G. Kreisel, Church's thesis: A kind of reducibility axiom for constructive mathematics, Intuitionism and Proof Theory (ed. J. R. Myhill et. al), Amsterdam 1970, p. 121-150.
[14] G. Kreisel, A survey of proof theory II, Proc. Second Scand. Logic Symp. Amsterdam 1971, p. 109-170.
[15] G. Kreisel and J-L. Krivine, Elements of mathematical logic, second revised printing, Amsterdam. 1971.
[16] G. Kreisel and A. Levy, Reflection principles and their me for establishing the complexity of axiomatic systems, Zeitschr. f. math. Logik und Grundlagen d. Math. 14 (1968), p. 97-142. (Theorem 20 on p. 135-136 can be replaced by the stronger and more elegant result : For systems S considered and k-formulae A:[(k — ConS) ∧S⊦A)] → A, if k ≤ 2. But there is a $∑^0_3$ sentence $A_0$ and an ω-consistent S such that $S ⊦ A_0$ and $A_0$ is false (9).A very much sharpened form of the assertion in the last paragraph of p. 140 has been established in [1]).
[17] G. Kreisel and A. S. Troelstra, Formal systems for some branches of intuitionistic analysis, Ann. of Math. Logic 1 (1970), p. 229-387. An addendum (by A. S. Troelstra) ibidem 3 (1971), p. 437-439.
[18] M. H. Löb, Solution of a problem of Leon Henkin, JSL 20 (1955), p. 115-118.
[19] A. Mostowski, Sentences undecidable in formalized arithmetic, Amsterdam 1954.
[20] J. B. Rosser, Extensions of some theorems of Gödel and Church, JSL 1 (1936), p. 89-91.
[21] W. W. Tait, A non-constructive proof of Gentzen's Hauptsatz for second order predicate logic, Bull. Amer. Math. Soc. 72 (1966), p. 980-983.
[22] G. Takeuti, On a generalized logical calculus, Japan. J. of Math. 23 (1953), p. 39-96.
[23] G. Takeuti, Consistency proofs of subsystems of classical analysis, Ann. of Math. (2), 86 (1967), p. 299-348.