Abstract
We present a reflection principle of the form “If ⌈ϕ⌉ is provable, then ϕ” implemented in the HOL4 theorem prover, assuming the existence of a large cardinal. We use the large-cardinal assumption to construct a model of HOL within HOL, and show how to ensure ϕ has the same meaning both inside and outside of this model. Soundness of HOL implies that if ⌈ϕ⌉ is provable, then it is true in this model, and hence ϕ holds. We additionally show how this reflection principle can be extended, assuming an infinite hierarchy of large cardinals, to implement model polymorphism, a technique designed for verifying systems with self-replacement functionality.
Cite
CITATION STYLE
Fallenstein, B., & Kumar, R. (2015). Proof-producing reflection for HOL with an application to model polymorphism. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9236, pp. 170–186). Springer Verlag. https://doi.org/10.1007/978-3-319-22102-1_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
