Syntactical and semantical properties of simple type theory
From MaRDI portal
Publication:3845367
DOI10.2307/2963525zbMath0109.00511OpenAlexW2089702017MaRDI QIDQ3845367
Publication date: 1960
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2963525
Related Items
Cut-elimination for quantified conditional logic ⋮ Proofs with monotone cuts ⋮ Is cut-free logic fit for unrestricted abstraction? ⋮ A semantics for \(\lambda \)Prolog ⋮ Schnittelimination in einem Teilsystem der einfachen Typenlogik ⋮ A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic ⋮ Natural Deduction, Inference, and Consistency ⋮ Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants ⋮ Simple type theory of Gentzen style with the inference of extensionality ⋮ A cut-free calculus for second-order Gödel logic ⋮ Completeness and cut-elimination for first-order ideal paraconsistent four-valued logic ⋮ Cut elimination, identity elimination, and interpolation in super-Belnap logics ⋮ One step is enough ⋮ Category theory in Isabelle/HOL as a basis for meta-logical investigation ⋮ Completeness of cut-free type theories ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ A simple proof that super-consistency implies cut elimination ⋮ Prawitz, Proofs, and Meaning ⋮ Semantical Approach to Cut Elimination and Subformula Property in Modal Logic ⋮ Paraconsistency and the need for infinite semantics ⋮ Vollständigkeit und Schnittelimination in der intuitionistischen Typenlogik ⋮ Ein starker Normalisationssatz für die intuitionistische Typentheorie ⋮ Memories of Kurt Schütte and the logic group in Munich: A personal report ⋮ Reminiscences of Kurt Schütte ⋮ Cut-Elimination for SBL ⋮ From Probability Measures to Each Lévy Triplet and Back ⋮ Lorenzen Between Gentzen and Schütte
Cites Work
