The Reflection Theorem: A Study in Meta-theoretic Reasoning

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.

• Type: Conference
• Year: 2002
• Where: CADE
• Authors: Lawrence C. Paulson
• Keywords: Automated Reasoning, Built-in Tools, CADE 2002, Proof Requires Reasoning, Reflection Theorem