Completeness of Hoare logic with inputs over the standard model
Completeness of Hoare logic with inputs over the standard model
复制标题
DOI：
10.1016/j.tcs.2015.08.004
复制
发表时间：
2016-01
期刊：
影响因子：
--
通讯作者：
Zhaowei Xu;Yuefei Sui;Wenhui Zhang
中科院分区：
文献类型：
--
作者：
Zhaowei Xu;Yuefei Sui;Wenhui Zhang
用一阶逻辑语言L和一阶理论T表示的while-程序集的Hoare逻辑记为HL（T）。Bergstra和Tucker指出，完全数论Th（N）是Peano算术PA的唯一推广T，HL（T）对它来说是逻辑完备的。完整性结果并不令人满意，因为它允许输入范围超过非标准模型。本文的目的是研究在什么情况下HL（T）是逻辑上完全的，当输入范围超过标准模型N。PA+的定义是将所有描述非终止计算的不可证明的N1-句子加到PA上。证明了N中的每个可计算函数在PA+的所有模型中都是一致可定义的，并且PA+是算术的。最后，基于从HL（T）到T的约化，证明了PA+是PA的最小扩张T，当输入的范围超过N时，HL（T）对它是逻辑完备的。这个完整性结果比Bergstra和Tucker的结果更有优势，因为PA+是算术的，而Th（N）不是。
Hoare logic for the set of while-programs with the first-order logical language L and the first-order theory T⊂ L is denoted by HL (T). Bergstra and Tucker have pointed out that the complete number theory Th (N) is the only extension T of Peano arithmetic PA for which HL (T) is logically complete. The completeness result is not satisfying, since it allows inputs to range over nonstandard models. The aim of this paper is to investigate under what circumstances HL (T) is logically complete when inputs range over the standard model N. PA+ is defined by adding to PA all the unprovable Π 1-sentences that describe the nonterminating computations. It is shown that each computable function in N is uniformly Σ 1-definable in all models of PA+, and that PA+ is arithmetical. Finally, it is established, based on the reduction from HL (T) to T, that PA+ is the minimal extension T of PA for which HL (T) is logically complete when inputs range over N. This completeness result has an advantage over Bergstra's and Tucker's one, in that PA+ is arithmetical while Th (N) is not.