A simple proof of second-order strong normalization with permutative conversions

DOI10.1016/J.APAL.2005.05.009MaRDI QIDQ2566069zbMATH OpenOpenAlexFDO

Authors Makoto Tatsuta, G. E. Mints

Publication date 22 September 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.009

zbMATH Keywords

strong normalizationpermutative conversionssecond-order natural deduction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Recommendations

• Short Proofs of Strong Normalization
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Strong normalization of classical natural deduction with disjunctions
• Proofs of strong normalisation for second order classical natural deduction
• A direct proof of strong normalization for full constructive second-order logic

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3503206 (Why is no real title available?)
• scientific article; zbMATH DE number 3513750 (Why is no real title available?)
• scientific article; zbMATH DE number 1114347 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• scientific article; zbMATH DE number 3365217 (Why is no real title available?)
• A short proof of the strong normalization of classical natural deduction with disjunction
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Non-strictly positive fixed points for classical natural deduction
• On the strong normalisation of intuitionistic natural deduction with permutation-conversions
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• The completeness of Heyting first-order logic

Cited in

(9)

• Strong normalization of classical natural deduction with disjunctions
• Short Proofs of Strong Normalization
• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• Strong normalization for truth table natural deduction
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• scientific article; zbMATH DE number 4055611 (Why is no real title available?)
• Inhabitation of polymorphic and existential types
• A note on how to extend Gentzen's second consistency proof to a proof of normalization for first order arithmetic
• The existential fragment of second-order propositional intuitionistic logic is undecidable

Describes a project that uses

Uses Software

• Automath

This page was built for publication: A simple proof of second-order strong normalization with permutative conversions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2566069)