A proof of cut-elimination theorem in simple type-theory

DOI10.2969/jmsj/01940399zbMath0206.27503OpenAlexW2009247993MaRDI QIDQ2542723

Moto-o Takahashi

Publication date: 1967

Published in: Journal of the Mathematical Society of Japan (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2969/jmsj/01940399

Mathematics Subject Classification ID

Related Items (30)

Cut-elimination for quantified conditional logic ⋮ On nonstandard models in higher order logic ⋮ A semantics for \(\lambda \)Prolog ⋮ A compact representation of proofs ⋮ Simple type theory of Gentzen style with the inference of extensionality ⋮ A cut-free calculus for second-order Gödel logic ⋮ Resolution in type theory ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ An intensional type theory: motivation and cut-elimination ⋮ Kripke semantics for higher-order type theory applied to constraint logic programming languages ⋮ A simple proof that super-consistency implies cut elimination ⋮ Hauptsatz for higher-order modal logic ⋮ A proof of the cut-elimination theorem in simple type theory ⋮ Completeness of type assignment systems with intersection, union, and type quantifiers ⋮ Prawitz, Proofs, and Meaning ⋮ Theory of proofs (arithmetic and analysis) ⋮ Typing and computational properties of lambda expressions ⋮ Vollständigkeit und Schnittelimination in der intuitionistischen Typenlogik ⋮ Ein syntaktischer Beweis für die Zulässigkeit der Schnittregel im Kalkül von Schütte für die intuitionistische Typenlogik ⋮ Ein starker Normalisationssatz für die intuitionistische Typentheorie ⋮ Mechanized metatheory revisited ⋮ On Takeuti's early view of the concept of set ⋮ Memories of Kurt Schütte and the logic group in Munich: A personal report ⋮ On the Convergence of Reduction-based and Model-based Methods in Proof Theory ⋮ Neo-Logicism and Its Logic ⋮ Annual Meeting of the Association for Symbolic Logic ⋮ Interpolation for first order S5 ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

This page was built for publication: A proof of cut-elimination theorem in simple type-theory