Hostname: page-component-74656f9884-2dmjx Total loading time: 0 Render date: 2026-11-08T15:06:10.738Z Has data issue: false hasContentIssue false
  • English
  • Français

Classical mathematics for a constructive world

Published online by Cambridge University Press:  01 July 2011

RUSSELL O'CONNOR
RUSSELL O'CONNOR*
Affiliation:
Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada and Microsoft Research – INRIA Joint Centre Email: roconn@mcmaster.ca
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory, and classical reasoning is typically supported by adding additional non-constructive axioms. However, there is another perspective that views constructive logic as an extension of classical logic. This paper will illustrate how classical reasoning can be supported in a practical manner inside dependent type theory without additional axioms. We will show several examples of how classical results can be applied to constructive mathematics. Finally, we will show how to extend this perspective from logic to mathematics by representing classical function spaces using a weak value monad.

References

Altenkirch, T. and McBride, C. (2006) Towards observational type theory. Manuscript, available online.Google Scholar
Altenkirch, T., McBride, C. and Swierstra, W. (2007) Observational equality, now! In: PLPV '07 Proceedings of the 2007 workshop on Programming languages meets program verification, ACM 57–68.Google Scholar
Barendregt, H. and Geuvers, H. (2001) Proof-assistants using dependent type systems. In: Robinson, A. and Voronkov, A. (eds.) Handbook of Automated Reasoning 2, Elsevier Science Publishers 1149–1238.CrossRefGoogle Scholar
Bauer, A. and Taylor, P. (2009) The Dedekind reals in abstract Stone duality. Mathematical Structures in Computer Science 19 757–838.CrossRefGoogle Scholar
Coq Development Team (2009) The Coq Proof Assistant Reference Manual – Version V8.2, INRIA-Rocquencourt. (Available at http://coq.inria.fr.)Google Scholar
Geuvers, H., Koprowski, A., Synek, D. and van der Weegen, E. (2010) Automated machine-checked hybrid system safety proofs. In: Kaufmann, M. and Paulson, L. (eds.) Proceedings Interactive Theorem Proving, ITP 2010. Springer-Verlag Lecture Notes in Computer Science 6172259–274.Google Scholar
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E. and Théry, L. (2007) A modular formalisation of finite group theory. In: Schneider, K. and Brandt, J. (eds.) Proceedings Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007. Springer-Verlag Lecture Notes in Computer Science 473286–101.Google Scholar
Gonthier, G. and Stéphane, L. R. (2009) An Ssreflect Tutorial. Technical Report RT-0367, INRIA. (Available at http://hal.inria.fr/inria-00407778/en/.)Google Scholar
Gödel, K. (1933) Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines mathematischen Kolloquiums 4 34–38. (English translation: On intuitionistic arithmetic and number theory. In: M. Davis (ed.) The Undecidable – Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Raven, New York, 1965 (Reprint, Dover, 2004) 75–81.)Google Scholar
Kock, A. (1972) Strong functors and monoidal monads. Archiv der Mathematik 23 113–120.CrossRefGoogle Scholar
Leroy, X. (2009) Programming with dependent types: Passing fad or useful tool? (Available at http://www.comlab.ox.ac.uk/ralf.hinze/WG2.8//26/slides/xavier.pdf.)Google Scholar
Mines, R., Richman, F. and Ruitenburg, W. (1988) A Course in Constructive Algebra, Springer-Verlag.CrossRefGoogle Scholar
Nordström, B., Petersson, K. and Smith, J. M. (1990) Programming in Martin-Löf's type theory: an introduction, Clarendon Press.Google Scholar
Norell, U. (2007) Towards a practical programming language based on dependent type theory, Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden.Google Scholar
O'Connor, R. (2008a) Certified exact transcendental real number computation in Coq. In: Mohamed, O. A., Muñoz, C. and Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). Springer-Verlag Lecture Notes in Computer Science 5170246–261.CrossRefGoogle Scholar
O'Connor, R. (2008b) A computer verified theory of compact sets. In: Buchberger, B., Ida, T. and Kutsia, T. (eds.) Proceedings of Austrian–Japanese Workshop on Symbolic Computation in Software Science (SCSS 2008). RISC-Linz Report Series (08-08) 148–162.Google Scholar
O'Connor, R. (2009) Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory, Ph.D. thesis, Radboud Universiteit Nijmegen.Google Scholar
Rasiowa, H. and Sikorski, R. (1968) The Mathematics of Metamathematics (second edition), Polish Scientific Publishers.Google Scholar
Simpson, S. G. (1999) Subsystems of second order arithmetic, Perspectives in Mathematical Logic, Springer-Verlag.CrossRefGoogle Scholar
Thompson, S. (1991) Type Theory and Functional Programming, Addison Wesley.Google Scholar
Troelstra, A. S. and Schwichtenberg, H. (1996) Basic Proof Theory, Cambridge tracts in theoretical computer science 43, Cambridge University Press.Google Scholar
Wadler, P. (1995) Monads for functional programming. In: Jeuring, J. and Meijer, E. (eds.) Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques – Tutorial Text. Springer-Verlag Lecture Notes in Computer Science 92524–52.Google Scholar