Document

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

## File

LIPIcs.CSL.2015.343.pdf
• Filesize: 430 kB
• 16 pages

## Cite As

Stefano Berardi. Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 343-358, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CSL.2015.343

## 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.
##### Keywords
• Intuitionism
• Inductive Definitions
• Proof Theory
• impredicativity
• omega rule

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, 1993.
2. Stefano Berardi, Paulo Oliva, and Silvia Steila. Proving termination of programs having transition invariants of height ω. In Proceedings of the 15th Italian Conference on Theoretical Computer Science, Perugia, Italy, September 17-19, 2014., pages 237-240, 2014.
3. Stefano Berardi and Silvia Steila. Ramsey theorem as an intuitionistic property of well founded relations. In Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pages 93-107, 2014.
4. Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg. Refined program extraction form classical proofs. Ann. Pure Appl. Logic, 114(1-3):3-25, 2002.
5. T. Coquand and D. Fridlender. A proof of higman’s lemma by structural induction. unpublished draft.
6. Thierry Coquand, Giovanni Sambin, Jan M. Smith, and Silvio Valentini. Inductively generated formal topologies. Ann. Pure Appl. Logic, 124(1-3):71-106, 2003.
7. D. Fridlender. Higman’s lemma in Type Theory. PhD thesis, Chalmers University, 1997.
8. H. Friedman. Classically and intuitionistically provably recursive functions. Lecture Notes in Mathematics, 669:21-27, 1978.
9. J.-Y. Girard. Proof theory and logical complexity. Studies in Proof Theory. Monographs, 1. Bibliopolis, 1987.
10. William A. Howard and Georg Kreisel. Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. J. Symb. Log., 31(3):325-358, 1966.
11. U. Kohlenbach. Applied Proof Theory: Proof Interpretation and their Use in Mathematics. Springer-Verlag Berlin Heidelberg, 2008.
12. Georg Kreisel. On the interpretation of non-finitist proofs: Part II. interpretation of number theory. applications. J. Symb. Log., 17(1):43-58, 1952.
13. P. Martin-Lof. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In Proceedings of the Second Scandinavian Logic Symposium, Oslo, pages 179-216, 1971.
14. P. Martin-Lof. Hauptsatz for the theory of species. In Proceedings of the Second Scandinavian Logic Symposium, Oslo, pages 217-233, 1971.
15. David Michael Ritchie Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings, pages 167-183, 1981.
16. D. Prawitz. Ideas and results in proof theory. In Proceedings of the Second Scandinavian Logic Symposium, Oslo, pages 235-307, 1971.
17. K. Schutte. Proof Theory. Springer-Verlag, Berlin Heildelberg New York, 1977.
18. W. Sieg, W. Buchholz, S. Feferman, and W. Pohlers. Iterated Inductive Definitions and Subsystems of Analysis - Recent Proof Theoretical Studies, volume 897. Springer Lecture Notes in Mathematics (LNM) Berlin-Heidelberg-New York, 1981.
19. Jean van Heijenoort. From Frege to Gödel, A Source Book in Mathematical Logic, 1879-1931. Harward University Press, 2002.
20. Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop when you are almost-full - adventures in constructive termination. In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pages 250-265, 2012.