Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness

DOI10.4230/LIPICS.CSL.2015.343MaRDI QIDQ5351967zbMATH OpenOpenAlexFDO

Authors Stefano Berardi

Publication date 31 August 2017

Full work available at URL https://iris.unito.it/bitstream/2318/1526139/1/21.pdf

zbMATH Keywords

impredicativityinductive definitionsintuitionismomega ruleproof theory

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Intuitionistic completeness and classical logic
• Arithmetical Completeness of the Intuitionistic Logic of Proofs
• A generalization of a conservativity theorem for classical versus intuitionistic arithmetic
• On the Hierarchy of Intuitionistic Bounded Arithmetic
• scientific article; zbMATH DE number 2152681
• Publication:3481700
• Intuitionistic completeness for first order classical logic
• Classical and intuitionistic models of arithmetic
• On the proofs of arithmetical completeness for interpretability logic
• scientific article; zbMATH DE number 4068863

Cited in

(6)

• Arithmetic transfinite induction and recursive well-orderings
• scientific article; zbMATH DE number 4068863 (Why is no real title available?)
• A generalization of a conservativity theorem for classical versus intuitionistic arithmetic
• Non-commutative classical arithmetical sequent calculi are intuitionistic
• From hierarchies to well-foundedness
• DIALOGUE THEORY OF PROOFS FOR ARITHMETIC, ANALYSIS, AND SET THEORY

This page was built for publication: Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness

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