Document Open Access Logo

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

Author Stefano Berardi

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Stefano Berardi

Cite AsGet BibTex

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
    PDF Downloads
    0
    Metadata Views

References

  1. T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, 1993. Google Scholar
  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. Google Scholar
  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. Google Scholar
  4. Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg. Refined program extraction form classical proofs. Ann. Pure Appl. Logic, 114(1-3):3-25, 2002. Google Scholar
  5. T. Coquand and D. Fridlender. A proof of higman’s lemma by structural induction. unpublished draft. Google Scholar
  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. Google Scholar
  7. D. Fridlender. Higman’s lemma in Type Theory. PhD thesis, Chalmers University, 1997. Google Scholar
  8. H. Friedman. Classically and intuitionistically provably recursive functions. Lecture Notes in Mathematics, 669:21-27, 1978. Google Scholar
  9. J.-Y. Girard. Proof theory and logical complexity. Studies in Proof Theory. Monographs, 1. Bibliopolis, 1987. Google Scholar
  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. Google Scholar
  11. U. Kohlenbach. Applied Proof Theory: Proof Interpretation and their Use in Mathematics. Springer-Verlag Berlin Heidelberg, 2008. Google Scholar
  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. Google Scholar
  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. Google Scholar
  14. P. Martin-Lof. Hauptsatz for the theory of species. In Proceedings of the Second Scandinavian Logic Symposium, Oslo, pages 217-233, 1971. Google Scholar
  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. Google Scholar
  16. D. Prawitz. Ideas and results in proof theory. In Proceedings of the Second Scandinavian Logic Symposium, Oslo, pages 235-307, 1971. Google Scholar
  17. K. Schutte. Proof Theory. Springer-Verlag, Berlin Heildelberg New York, 1977. Google Scholar
  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. Google Scholar
  19. Jean van Heijenoort. From Frege to Gödel, A Source Book in Mathematical Logic, 1879-1931. Harward University Press, 2002. Google Scholar
  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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact