License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.343
URN: urn:nbn:de:0030-drops-54246
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5424/
Go to the corresponding LIPIcs Volume Portal

Berardi, Stefano

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

pdf-format:
21.pdf (0.4 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{berardi:LIPIcs:2015:5424,
  author =	{Stefano Berardi},
  title =	{{Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{343--358},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5424},
  URN =		{urn:nbn:de:0030-drops-54246},
  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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI