A. The three-valued predicate calculus............................................................ 8 A 1. Three-valued structures; classical case............................................. 8 A 2. Three-valued structures; intuitionistic case........................................ 10 A 3. Theories; models..................................................................................... 12 A 4. The completeness theorem.................................................................. 14 A 5. The thinness theorem............................................................................. 18 B. Three-valued analysis and cut elimination......................................................... 19 B 1. The syntax................................................................................................. 19 B 2. The semantics......................................................................................... 22 B 3. Cut-free provability................................................................................... 23 B 4. Takeuti's conjecture................................................................................ 28 C. Applications to the metamathematics of cut-free analysis.............................. 30 C 1. Poor and absorbing formulas............................................................... 31 C 2. A candidate for synonymity.................................................................... 32 C 3. Syntactic conditions for poverty............................................................. 35 C 4. Takeuti's conjectures and $∑^0_1$-reflection.................................. 36 C 5. Cut elimination in the classical case.................................................. 37 C 6. The poverty theorem............................................................................... 39 Appendix......................................................................................................................... 41 1. Tait's proof.................................................................................................... 41 2. Prawitz's proof.............................................................................................. 42 3. Prawitz's third proof..................................................................................... 43 4. The co-rule.................................................................................................... 43 5. The simple theory of types......................................................................... 44
[1] G. Kreisel and G. Takeuti, Formally self-referential propositions for cut free classical analysis and related systems, Dies. Math. 118, Warszawa 1974.
[2] М. H. Lob, Solution of a problem of Leon Henkin, JSL 20 (1955), p. 115-118.
[3] D. Prawitz, Natural deduction, a proof theoretical study, Almqvist & Wiksell, Stockholm 1965.
[4] D. Prawitz, Completeness and Hauptsatz for second order logic, Theoria 33 (1967), p. 246-258.
[5] D. Prawitz, Hauptsatz for higher order logic, JSL 33 (1968), p. 452-457.
[6] D. Prawitz, Some results for intuitionistic logic with second order quantification rules, Intuitionism & proof theory, eds. Kino, Myhill & Vesley, North Holland, Amsterdam 1970, p. 259-270.
[7] H. Rasiowa and R. Sikorski, The mathematics of metamathematics, Warszawa 1963.
[8] K. Shütte, Syntactical and semantical properties of simple type theory, JSL 25 (1960), p. 305-326.
[9] 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.
[10] M. Takahashi, A proof of cut-elimination theorem in simple type theory, J. Math. Soc. Japan 19 (1967), p. 399-410.
[11] G. Takeuti, On a generalized logical calculus, Japanese J. Math. 23 (1953), p. 39-96.