2026-07-22T22:17:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5424 2024-03-06T10:36:26Z ddc:004 open_access

Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness Berardi, Stefano Intuitionism Inductive Definitions Proof Theory impredicativity omega rule Assume that we may prove in Classical Functional Analysis that a primitive recursive relation R is well-founded, using the inductive definition of well-founded. In this paper we prove that such a proof of well-foundation may be made intuitionistic. We conclude that if we are able to formulate any mathematical problem as the inductive well-foundation of some primitive recursive relation, then intuitionistic and classical provability coincide, and for such a statement of well-foundation we may always find an intuitionistic proof if we may find a proof at all. The core of intuitionism are the methods for computing out data with given properties from input data with given properties: these are the results we are looking for when we do constructive mathematics. Proving that a primitive recursive relation R is inductively well-founded is a more abstract kind of result, but it is crucial as well, because once we proved that R is inductively well-founded, then we may write programs by induction over R. This is the way inductive relation are currently used in intuitionism and in proof assistants based on intuitionism, like Coq. In the paper we introduce the comprehension axiom for Functional Analysis in the form of introduction and elimination rules for predicates of types Prop, Nat->Prop, ..., in order to use Girard's method of candidates for impredicative arithmetic. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stefano Berardi 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.343 urn:nbn:de:0030-drops-54246 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.343 eng https://creativecommons.org/licenses/by/3.0/legalcode