Abstract
Assume that we may prove in Classical Functional Analysis that a primitive recursive relation R is wellfounded, using the inductive definition of wellfounded. In this paper we prove that such a proof of wellfoundation may be made intuitionistic. We conclude that if we are able to formulate any mathematical problem as the inductive wellfoundation of some primitive recursive relation, then intuitionistic and classical provability coincide, and for such a statement of wellfoundation 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 wellfounded is a more abstract kind of result, but it is crucial as well, because once we proved that R is inductively wellfounded, 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.
BibTeX  Entry
@InProceedings{berardi:LIPIcs:2015:5424,
author = {Stefano Berardi},
title = {{Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive WellFoundedness}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {343358},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897903},
ISSN = {18688969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5424},
URN = {urn:nbn:de:0030drops54246},
doi = {10.4230/LIPIcs.CSL.2015.343},
annote = {Keywords: Intuitionism, Inductive Definitions, Proof Theory, impredicativity, omega rule}
}
Keywords: 

Intuitionism, Inductive Definitions, Proof Theory, impredicativity, omega rule 
Collection: 

24th EACSL Annual Conference on Computer Science Logic (CSL 2015) 
Issue Date: 

2015 
Date of publication: 

07.09.2015 