On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem

DOI10.1016/j.tcs.2016.02.028zbMath1377.03050OpenAlexW2276824306MaRDI QIDQ265002

Federico Aschieri, Margherita Zorzi

Publication date: 1 April 2016

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2016.02.028

zbMATH Keywords

natural deductionclassical first-order logicCurry-Howard correspondencedelimited exceptionsHerbrand's theorem

Mathematics Subject Classification ID

Computational learning theory (68Q32) Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40)

Related Items (6)

On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC ⋮ Unnamed Item ⋮ Proof nets for classical logic ⋮ GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION ⋮ Expansion trees with cut ⋮ QPCF: higher-order languages and quantum circuits

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The epsilon calculus and Herbrand complexity
• Lectures on the Curry-Howard isomorphism
• Epsilon substitution method for elementary analysis
• Ackermann's substitution method (remixed)
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
• Probabilistic operational semantics for the lambda calculus
• Interactive Realizers
• On quantum lambda calculi: a foundational perspective
• Gentzen's Proof of Normalization for Natural Deduction
• Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms
• A semantics of evidence for classical arithmetic
• Non-determinism, Non-termination and the Strong Normalization of System T
• On weak completeness of intuitionistic predicate logic
• Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1
• On the interpretation of non-finitist proofs–Part II

This page was built for publication: On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem