Proof-Producing Reflection for HOL With an Application to Model Polymorphism

被引：9
作者：
Fallenstein, Benja [1 ]
Kumar, Ramana [2 ]
机构：
[1] Machine Intelligence Res Inst, Berkeley, CA USA
[2] Univ Cambridge, Comp Lab, Cambridge, England
来源：
INTERACTIVE THEOREM PROVING | 2015年 / 9236卷
关键词：
LOGIC;
D O I：
10.1007/978-3-319-22102-1_11
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a reflection principle of the form "If ([)phi(]) is provable, then phi 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 phi has the same meaning both inside and outside of this model. Soundness of HOL implies that if ([)phi(])is provable, then it is true in this model, and hence phi 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.
引用
收藏
页码：170 / 186
页数：17
相关论文
共 20 条
  • [1] Allen S. F., 1990, Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science (90CH2897-7), P95, DOI 10.1109/LICS.1990.113737
  • [2] [Anonymous], TECHNICAL REPORT
  • [3] [Anonymous], CRC053 SRI
  • [4] [Anonymous], J AUTOM REASON UNPUB
  • [5] [Anonymous], THEOREM PROVING HIGH
  • [6] [Anonymous], INTERACTIVE THEOREM
  • [7] [Anonymous], 1931, Monatshefte fur Mathematik und Physik, DOI DOI 10.1007/BF01700692
  • [8] Dybjer P, 1999, LECT NOTES COMPUT SC, V1581, P129
  • [9] Feferman S., 1962, J SYMBOLIC LOGIC, V27, P259, DOI DOI 10.2307/2964649
  • [10] Transfinite progressions:: A second look at completeness
    Franzén, T
    [J]. BULLETIN OF SYMBOLIC LOGIC, 2004, 10 (03) : 367 - 389
12