Some remarks on the Curry-Howard correspondence for classical logic

In this note we focus on simply typed λ μ-calculus, the image under Curry-Howard correspondence of the →, ⊥-fragment of minimal logic extended with classical reductio. We show that simply typed λ μ-calculus delivers a non-trivial interpretation of the distinctive form of irrelevance of conclusions of reductio w.r.t. discharged assumptions, while providing a privileged normalization procedure for the →, ⊥-fragment. We give a detailed analysis of the intensional incompleteness of the →, ⊥-fragment w.r.t. full classical logic, and then discuss the philosophical significance of the failure of Böhm’s theorem for simply typed λ μ-calculus.