The Reflection Theorem: A Study in Meta-theoretic Reasoning
- 280 Downloads
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.
KeywordsInduction Hypothesis Automate Reasoning High Order Logic Introduction Rule Consistency Proof
Unable to display preview. Download preview PDF.
- 1.Grzegorz Bancerek. The reflection theorem. Journal of Formalized Mathematics, 2, 1990. http://megrez.mizar.org/mirror/JFM/Vol2/zf_refle.html.
- 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
- 4.Frank R. Drake. Set Theory: An Introduction to Large Cardinals. North-Holland, 1974.Google Scholar
- 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
- 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. , pages 149–165.CrossRefGoogle Scholar
- 8.Kenneth Kunen. Set Theory: An Introduction to Independence Proofs. North-Holland, 1980.Google Scholar
- 9.Andrzej Mostowski. Constructible Sets with Applications. North-Holland, 1969.Google Scholar
- 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.The QED manifesto. http://www-unix.mcs.anl.gov/qed/, 1995.
- 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. , pages 167–183.CrossRefGoogle Scholar