Abstract
Sections 1 to 4 contain the strong completeness theorem of cut-free intuitionistic type theory relative to semi-Kripke-valuations, which gives the following corollaries: (1) The strong completeness theorem for intuitionistic type theory with cut rule relative to full Kripke-valuations. (2) A semantical eqivalent of cutelimination in intuitionistic type theory. Section 5 contains a proof of the cutelimination theorem and some corollaries to it.
Similar content being viewed by others
Literatur
ACZEL, P.H.G.: Saturated intuitionistic theories, Contributions to the mathematical logic, North Holland, Amsterdam, 1–11, 1968.
FITTING, M.: Intuitionistic logic model theory and forcing, 1. Aufl., North Holland, Amsterdam 1969.
HENKIN, L.: Completeness in the theory of types, J. symbolic logic 15, 81–91, 1950.
KRIPKE S.: Semantical analysis of intuitionistic logic 1, in Formal systems and recursive functions, ed. J. Crossley and M. Dummet, North Holland, Amsterdam, 92–130, 1965.
PRAWITZ, D.: Natural deduction, a proof theoretical study, 1. Aufl., Stockholm, 1965.
PRAWITZ, D.: Hauptsatz for higher order logic, J. symbolic logic 33, 452–457, 1968.
PRAWITZ, D.: Some results for intuitionistic logic with second order quantification rules, Intuitionism and proof theory, North Holland, Amsterdam, 259–270, 1970.
SCHÜTTE, K.: Schlußweisenkalküle der Prädikatenlogik, Math. Ann. 122, 47–65, 1950.
SCHÜTTE, K.: Syntactical and semantical properties of simple type theory, J. symbolic logic 25, 305–326, 1960.
TAKAHASHI, M.: A proof of cut-elimination theorem in simple type theory, The journal of the mathematical society of Japan 19, 399–410, 1967.
TAKAHASHI, M.: Cut-elimination theorem and Brouwerian-valued models for intuitionistic type theory, Comment. math. universitatis Sancti Pauli, Tokyo, 1–18, 1970.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Osswald, H. Vollständigkeit und Schnittelimination in der Intuitionistischen Typenlogik. Manuscripta Math 6, 17–31 (1972). https://doi.org/10.1007/BF01298410
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/BF01298410