Gentzen's Proof of Normalization for Natural Deduction
From MaRDI portal
Publication:3503742
DOI10.2178/bsl/1208442829zbMath1145.03003OpenAlexW2037693339MaRDI QIDQ3503742
Publication date: 9 June 2008
Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2178/bsl/1208442829
Cut-elimination and normal-form theorems (03F05) Collected or selected works; reprintings or translations of classics (01A75) History of mathematical logic and foundations (03-03)
Related Items (25)
On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem ⋮ Dialogues and Proofs; Yankov’s Contribution to Proof Theory ⋮ Stabilizing quantum disjunction ⋮ Proofs as Objects ⋮ General-elimination harmony and the meaning of the logical constants ⋮ AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ An ecumenical notion of entailment ⋮ Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons) ⋮ Adding Negation to Lambda Mu ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules ⋮ Proof-theoretic harmony: towards an intensional account ⋮ On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC ⋮ A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION ⋮ Cut as Consequence ⋮ Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs ⋮ GENERALITY AND EXISTENCE: QUANTIFICATIONAL LOGIC IN HISTORICAL PERSPECTIVE ⋮ Prawitz, Proofs, and Meaning ⋮ Inversion Principles and Introduction Rules ⋮ Meaning in Use ⋮ Normality, non-contamination and logical depth in classical natural deduction ⋮ Das Problem der apagogischen Beweise in BolzanosBeyträgenund seinerWissenschaftslehre ⋮ Human-centered automated proof search ⋮ Maximum segments as natural deduction images of some cuts ⋮ Normalisation and subformula property for a system of classical logic with Tarski's rule
Cites Work
This page was built for publication: Gentzen's Proof of Normalization for Natural Deduction
