Advertisement

The Reflection Theorem: A Study in Meta-theoretic Reasoning

  • Lawrence C. Paulson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

The reflection theorem has been proved using Isabelle/ZF. This theorem cannot be expressed in ZF, and its proof requires reasoning at the meta-level. There is a particularly elegant proof that reduces the meta-level reasoning to a single induction over formulas. Each case of the induction has been proved with Isabelle/ZF, whose built-in tools can prove specific instances of the reflection theorem upon demand.

Keywords

Induction Hypothesis Automate Reasoning High Order Logic Introduction Rule Consistency Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Grzegorz Bancerek. The reflection theorem. Journal of Formalized Mathematics, 2, 1990. http://megrez.mizar.org/mirror/JFM/Vol2/zf_refle.html.
  2. 2.
    Johan G. F. Belinfante. Computer proofs in Gödel’s class theory with equational definitions for composite and cross. Journal of Automated Reasoning, 22(3):311–339, March 1999.Google Scholar
  3. 3.
    Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin, and Laurent Théry, editors. Theorem Proving in Higher Order Logics: TPHOLs’ 99, LNCS 1690. Springer, 1999.zbMATHGoogle Scholar
  4. 4.
    Frank R. Drake. Set Theory: An Introduction to Large Cardinals. North-Holland, 1974.Google Scholar
  5. 5.
    Kurt Gödel. The consistency of the axiom of choice and of the generalized continuum hypothesis with the axioms of set theory. In S. Feferman et al., editors, Kurt Gödel: Collected Works, volume II. Oxford University Press, 1990. First published in 1940.Google Scholar
  6. 6.
    G. P. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.CrossRefMathSciNetGoogle Scholar
  7. 7.
    Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. Locales: A sectioning concept for Isabelle. In Gilles Dowek, André Hirschowitz, Christine Paulin, and Laurent Théry, editors. Theorem Proving in Higher Order Logics: TPHOLs’ 99, LNCS 1690. Springer, 1999 Bertot et al. [3], pages 149–165.CrossRefGoogle Scholar
  8. 8.
    Kenneth Kunen. Set Theory: An Introduction to Independence Proofs. North-Holland, 1980.Google Scholar
  9. 9.
    Andrzej Mostowski. Constructible Sets with Applications. North-Holland, 1969.Google Scholar
  10. 10.
    Lawrence C. Paulson. Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning, 11(3):353–389, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Lawrence C. Paulson. Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning, 15(2):167–215, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Lawrence C. Paulson and Krzysztof Grcabczewski. Mechanizing set theory: Cardinal arithmetic and the axiom of choice. Journal of Automated Reasoning, 17(3):291–323, December 1996.Google Scholar
  13. 13.
    The QED manifesto. http://www-unix.mcs.anl.gov/qed/, 1995.
  14. 14.
    Art Quaife. Automated deduction in von Neumann-Bernays-Gödel set theory. Journal of Automated Reasoning, 8(1):91–147, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Markus Wenzel. Type classes and overloading in higher-order logic. In Elsa L. Gunter and Amy Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs’ 97, LNCS 1275, pages 307–322. Springer, 1997.CrossRefGoogle Scholar
  16. 16.
    Markus Wenzel. Isar: A generic interpretative approach to readable formal proof documents. In Gilles Dowek, André Hirschowitz, Christine Paulin, and Laurent Théry, editors. Theorem Proving in Higher Order Logics: TPHOLs’ 99, LNCS 1690. Springer, 1999 Bertot et al. [3], pages 167–183.CrossRefGoogle Scholar
  17. 17.
    Andrew J. Wiles. Modular elliptic curves and Fermat’s Last Theorem. Annals of Mathematics, 141(3):443–551, 1995.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Lawrence C. Paulson
    • 1
  1. 1.Computer LaboratoryUniversity of CambridgeCambridgeUK

Personalised recommendations