CONTENTS Introduction........................................................................................................................................................................................................................5 0. Terminology and preliminaries......................................................................................................................................................................................12 1. The extent of cut elimination by absorption..................................................................................................................................................................17 2. ∏¹-completeness of second order logic and a new proof of the normal form theorem.................................................................................................24 3. Weak models and proper three-valued models of second order theories....................................................................................................................31 4. Model theoretic proofs of the normal form theorem for higher order systems: comparison with the literature..............................................................39 5. Completeness of the systems $JT^n$ and $∏^n$-completeness of $∑^n$-theories.....................................................................................................43 6. ∀-analytical completeness of the systems $JPRE^n$ and poor completeness of the theories $PRE^n$ of primitive recursive equations....................48 7. ∀¹ ∃⁰-completeness of PRE² and König's Lemma for primitive recursive 0-1-trees......................................................................................................56 References.......................................................................................................................................................................................................................62
[1] H. Friedman, Provable equality in primitive recursive arithmetic with and without induction, Pacific Journal Math. 57 (1975), 379-392.
[2] G. Gentzen, Untersuchungen über das logische Schliessen. I., Math. Zeitschrift 39 (1935), 176-210.
[3] J. Y. Girard, Three-valued logic and cut-elimination: The actual meaning of Takeuti's conjecture, Diss. Math. 136, Warszawa 1976.
[4] R. L. Goodstein. Recursive number theory, Amsterdam 1957.
[5] G. Kreisel and G. Takeuti, Formally self-referential propositions for cut free classical analysis and related systems, Diss. Math. 118, Warszawa 1974.
[6] P. Päppinghaus, Existentiell schwache Vollständigkeit der Logik zweiter Stufe und Schnittelimination, Dissertation, Univ. Heidelberg, Heidelberg 1977.
[7] D. Prawitz, Completeness and Hauptsatz for second order logic, Theoria 33 (1967), 246-253.
[8] D. Prawitz, Hauptsatz for higher order logic, JSL 33 (1968), 452-457.
[9] D. Prawitz, Some results for intuitionistic logic with second order quantification rules, in: A. Kino, J. Myhill, R. E. Vesley (eds.), Intuitionism and proof theory. Proc. of the summer conf. at Buffalo N. Y. 1968, Amsterdam 1970, 259-269.
[10] K. Schütte, Syntactical and semantical properties of simple type theory, JSL 25 (1960), 305-326.
[11] J. R. Shoenfield, Mathematical logic, Reading, Mass. 1967.
[12] W. W. Tait, A non-constructive proof of Gentzen's Hauptsatz for second order predicate logic, Bull. AMS 72 (1966), 980-983.
[13] M. Takahashi, A proof of cut-elimination theorem in simple type theory, J. Math. Soc. Japan 19 (1967), 399-410.
[14] M. Takahashi, Review of [12], JSL 33 (1968), 289-290.
[15] M. Takahashi, A system of simple type theory of Gentzen style with inference on extensionality, and the cut-elimination in it, Comment, math. Univ. Sancti Pauli 18 (1969), 129-147.
[16] G. Takeuti, On a generalized logical calculus, Jap. J. Math. 23 (1953), 39-96.
[17] G. Takeuti, Proof theory, Amsterdam 1975.
[18] A. S. Troelstra, Metamathematical investigation of intuitionistic arithmetic and analysis, Berlin-Heidelberg-New York 1973.
[19] H. Wolter, Über Mengen von Ausdrücken der Logik höherer Stufe, für die der Endlichkeitssatz und der Satz von Löwenheim-Skolem gelten, Zeitschr. f. math. Logik und Grundlagen d. Math. 18 (1972), 13-18.