The reflection theorem: A study in meta-theoretic reasoning

DOI10.1007/3-540-45620-1_31MaRDI QIDQ4809073zbMATH OpenFDO

Authors Lawrence C. Paulson

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2392/23920377.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Set theory (03E99)

Recommendations

• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• scientific article; zbMATH DE number 2185723
• A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
• Experimenting with Isabelle in ZF set theory
• Proof-producing reflection for HOL. With an application to model polymorphism

Cited in

(6)

• Locales: a module system for mathematical theories
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis
• Ordinal arithmetic: Algorithms and mechanization
• Reflecting rules: a note on generalizing the deduction theorem

Describes a project that uses

Uses Software

• Isar
• Isabelle/ZF

This page was built for publication: The reflection theorem: A study in meta-theoretic reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4809073)