Published in

Springer Verlag, Lecture Notes in Computer Science, p. 377-391

DOI: 10.1007/3-540-45620-1_31

Links

Tools

Export citation

Search in Google Scholar

The Reflection Theorem: A Study in Meta-theoretic Reasoning.

Proceedings article published in 2002 by Lawrence C. Paulson
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Upload
Green circle
Postprint: archiving allowed
Upload
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

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.