公理系统I-10的第二不完全性定理及其Herbrand演绎版本分析

理论计算机科学电子笔记165（2006）213-226www.elsevier.com/locate/entcs公理系统I-10对第二不完全性定理丹·E 威拉德奥尔巴尼大学摘要在1981年，Paris和Wilkie [21]指出，对于Herbrand演绎，I_0是否满足第二不完全性定理是一个悬而未决的问题。我们将证明，I0既服从又不服从第二不完全性定理的Herbrandized版本，这取决于我们检验I0的几个等价定义中的哪一个。关键词：Güodel1引言哥德尔Güodel'sseminalre sul t [ 1，2，3，4，5，6，7，8，1 2，1 5，1 8，1 9 ] [ 21，22，23，24，25，26，28，27，29，30，33，35，37，39]有许多generalizations和ndextensin al re例如，Pudlak和Solovay[23，26]的结合工作将Successor（x）=x+1作为一个全函数来计算，从而证明了一个在Hilbert演绎下自洽的定理.在1981年，Paris和Wilkie [21]注意到公理系统I_（10）是否满足第二不完全性定理对于无割演绎法是一个开放性问题。有趣的是，Paris-Wilkie观察到I0 +Exp甚至无法证明像Q这样简单的公理系统的希尔伯特相容性[31]。后来。Adamowicz-Zbierski [1，3]表明I0 +Ω1无法验证其Herbrand和语义表的一致性，Willard [33，35]扩展了这一点1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.047214D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）2130000结果表明，第二不完全性定理的无割版也适用于标准教科书版[10，13，17]的I-Jiango2005年11月16日，我们收到了一封来自洛杉矶的有趣的电子邮件关于这个问题的Kol-odziejczyk它观察到有两种自然的形式化I ~（10）的公理化，以下称为Ax-1和Ax-2。两者都应该把塔斯基-莫斯托夫斯基-罗宾逊公理系统Q作为他们的出发点。在φ（x，y）是Δ0公式的上下文中，这些形式将分别使用等式（1）和（2）。（2）表示其诱导方案。（一）（二）{{φ（x，0）} ∧ ∀y[φ(x, y) =⇒φ(x, yJ)]}=⇒∀yφ(x, y)}Jy≤z[φ（x，y）=y≤z φ（x，y）}Kol-odziejczyk注意到，逻辑上等价的公理系统，如Ax-1和Ax- 2，对于第二不完全性定理的无割版本，不一定具有相同的性质。因此他问[35]我们对这个问题的两部分答案的一半出现在另一篇论文中[40]。它解释了我们先前关于Ax-1的无割不完全性的结果如何直接推广到Ax-2。我们的两部分答案的后半部分将出现在这份会议文件中。具体如下：假设一个人希望扮演一个非常敌对的角色，成为魔鬼的辩护律师然后，我们可以构造 出第 三个 非正 统的 公理 化， 称为 Ax-3 ，它 回避 了第 二不 完全 性定 理的Herbrandized版本。为了理解这一非常违反直觉的现象的本质，从理论上讲，将α和β这两个轴向系统重新定义为αβ=βd是有用的证明同一套定理。中心点是，这样的等价并不限制两个系统可以独立地提供具有“α= β“的系统。由于这个原因，当一个逻辑等价的公理系统α满足第二不完全性定理的固定版本时，我们当然不能自动地假定β满足第二不完全性定理的固定版本。因此，本文将形式化I_0的第三个等价公理化，它至少避开了第二不完全性定理的Herbrandized版本。2一个新版本的I-10一个公式将被称为ΔR i，它具有类似于Δ0公式的结构，除了它的有界量化器，在本协议内不 . 相反，ΔR公式将只使用最大值函数作为唯一允许的运算符来定义变量的有界范围。（算术函数允许出现在ΔR的身体的其他地方。公式） 因此，等式（3）是ΔR公式，和（4）是一个例子D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）2132150101（x） ≤y x=y）∀x ∀y∧的 Δ0 公式不是 ΔR。(3)p≤Max（x，y）[（p+y≤x+ 2<$y）<$（p<$y≤y <$y<$y）](4)<$p≤x<$y[（p+y≤x+ 2<$y）<$（p<$y≤y <$y<$x）]让我们称一个公式为Ri，它可以写为R i，1，2，...... v n φ（v1，v2，. v n）其中φ（v1，v2，. v n）是Δ R公式。Ax-1、Ax-2和Ax-3中的每一个都将包含一个公共的九个BRR公理的集合，称为Q0，并在下面列出。 Q0的主要目的将是定义加法，乘法，整数后继，最大值以及=和≤的结构。（五）J1 = 0J∧2 = 1J0= 0 ∧0J/= 0 ∧0≤ 0 ∧ ¬[ 0 ≤0]（六）（七）（八）（九）（十）（十一）（十二）（十三）阿克斯 （ x +0 = x∧x·0 = 0∧x·1 =x）J J阿斯特丽德 （ x= y轴x=y）阿斯特丽德 （x≤y）J J Jx·y= （x·y）+xx + y= （x+y）xZ=Z] x = z x=x]x x≤zx x≤xx Max（x，y）= y） Max（x，y）=x）在上面对Q0的定义的上下文中，I =0的Ax-1和Ax-2公理化将被正式定义为Q0分别与方程（1）和（2）类似地，IndR将被定义为Q0与方程（2）的归纳图式的所有实例的并216D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）213100101集本段将定义一组句子，称为Trivial-R，IndR + Trivial-R证明了与更传统的Ax-1和Ax-2公理化相同的一组定理。 在我们的讨论中，元组（a0，a1，a2，.当满足以下条件时，a N）被称为非负整数x的分裂表示：N(14)x=ai（a0+ 1）i1AND 一 ≤a 拉瓜 ≤a 我... a≤ a−0 2 0N 0i=1对于固定整数N，令Split N（x，a0，a1，. a N）表示Δ R公式，（14）满意。的每个算术运算符， + 、 你好， 麦克斯 = 和 ≤， 斧头-移徙组织 Trivial-R系统 将有 可用 口之家 ΔR 谓词而公理，用于模拟这些函数在处理整数的分裂表示时的操作。因此对于 一个固定的三元组（I，J，K），设Mult I，J，K（a0，a1. a I，b0，b1.... b J，c0，c1.. c K）表示ΔR谓词模拟整数乘法的动作，当它的输入是两个分裂的整数（a0，a1.. a I）和（b0，b1. b J），其结果是（c0，c1. c K）。我们的系统Trivial-R的伴随的BRR公理，表明这个谓词正确运行，然后将是：1D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）2132170x你好，我是... b J 卡茨克{[拆分I（x，a0. a I）分割J（y，b0. b J）n Split K（z，c0. c K）]=[xy = zMult I，J，K（a0. a I，b0. b J，c0. c K）]}同样地，Trivial-R将有上述公理的适当的R11类似物，类似地模拟加法，最大值，相等和小于或等于分裂整数的形式主义假设Ax-3表示公理系统IndR + Trivial-R。第3节将证明Ax-3证明了与Ax-1和Ax-2相同的一组定理定义1令α∈β表示α(This定义同样假设α表示一致公理sys-tem和D表示一种演绎方法，（α，D）称为第二不完备性E的一个阈值i.所有相容扩张α∈α都具有这样的性质，即α∈ α不能用演绎方法D证明其证明的相容性.否则，（α，D）将被称为反阈值。(It是指某个相容的α可以在演绎方法D下证明一个自洽的定理。在这种情况下，我们的主要结果将是Ax-3是第二不完全性定理的Herbrandized版本的反阈值。这意味着肯定存在某个相容系统α<$$>Ax-3，其中α<$可以证明一个证明其Herbrand相容性的定理该结果是令人惊讶的，因为Ax-1和Ax-2同时是Herbran化的阈值。我们再次提醒读者，逻辑上等价的系统可以我们已经开始着手准备这份工作了。这是因为，α=β并不意味着，两个公理系统α和β证明了同一组定理。在我们的符号下，它并不意味着必须使rα或βc都能保留该静态方法“α c = β“。（Thisis）对Ax-3的阈值特性与Ax-1和Ax-2的阈值特性不同的直观解释3基本框架和基本直觉本节将正式证明Ax-3证明了与Ax-3相同的一组定理。1和AX-2。它也将直观地解释为什么Ax-3定理3.1 Ax-1、Ax-2和Ax-3中的每一个都证明了同一组定理。证据众所周知，Ax-1和Ax-2证明了同一组定理。这一切都是因为第三条规则。1，我们可以假定Ax-2=Ax-3。我们将使用的产品Paris和Dimitracopoulos [20]观察到在模型论意义上，Δ0公式与其等价的ΔR形式表示之间存在一一对应。218D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）213000（x，y，y，. y）]}01kk00XX00n在此基础上，我们将完全忽略Ax-2=Ax-3。相反，我们的证明草图将探索一个例子，说明这个不变量背后的潜在因此，令（x，y）表示ΔR公式 对于任何整数k，都有可能构造Δ R公式ΔR（x，y0，y1，. y k），它是整数的分裂表示的对应物，满足以下性质：x克雷蒂克（15）{Split k（y，y. y）=[（x，y）令大小L（y0，y1，. j k）表示Δ R公式，其指示（y0，y1，. j k）表示≤ L的整数。然后Ax-3可以使用它的平凡-R公理来首先证明等式（15），然后正式证明两个Δ0公式：y0≤x k≤ xSize k（y0，y1，. y k）x，y0，y1，. y k）y0≤x k≤ xSizek（y0，y1，. y k）x，y0，y1，. y k）因此，本质上通过将该技术（及其明显的类似物）的n次迭代应用于具有n个有界量化器的任何初始Δ 0公式，Ax-3可以将任意Δ 0公式转换为可证明等价的Δ R公式。 因此，尽管Ax-3系统在技术上仅包含等式（2）的公理的实例，虽然它是Δ R公式的公理模式，但它仍然有能力将Δ 0公式的这个公理模式的所有剩余实例正式证明为定理。Q我们证明Ax-3是不完全性定理的Herbrandized版本的反阈值将出现在第4节。在开始讨论之前，应该解释一下为什么Ax-2和Ax-3的操作如此不同。让卢恩 表示由等式（16）定义的Δ0语句。 注意这句话--tence由O（n） 逻辑符号，它断言变量2我v0，v1，v2，. v n， 具有v i= 2的 性 质 。v0≤2 vn≤vn−1(16)v0 = 2 v1 = v0v0v2 = v1v1. vn=vn−1很容易看出存在着一些ΔR句，称之为说R这是对应的0n用分裂整数表示的公式（16这句话将表示存在一个分裂整数序列 S0，S1，S2，. S n，在哪里2我SI 代表的是 二、然而，尽管它们在某种意义上代表了等价的概念，但Δ 0句n和它的Δ R对应句R之间存在着根本的区别。0n如果一个人使用的逻辑语言只有3个字母，那么这种差异就很容易解释命名常量，0，1和2，如果拆分整数被编码为基数为2的数字。然后EURR将被编码为至少2N人物，但肖恩时间复杂度为O（n）。作为这种区别（及其推广）的结果，我们可以确定，尽管Ax-2和Ax-3证明了D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）213219n12n12n形式定理的相同集合，它们对许多定理的证明在长度这一事实对于理解为什么这两种形式主义具有不同的不完全性阈值特性至关重要。它直观地解释了为什么Ax-2（在我们的Companion论文[40]中）遵守第二不完全性定理，但Ax-3（在下一节中）实际上回避了它。4主要分析在命题演算中，如果一个句子是不可满足的，那么这个句子就被称为反重言式（Anti-Tautology）（即，<$是一个重言式）。我们对Herbrand演绎的定义将被定义为：Adamowicz，Ha′jek-Pudla′kanddKo-lodziejczyk，[1，10，15]，除了我们将使用这个定义的双重版本，遵循德摩根换句话说，我们的定义将使用众所周知的恒等式，（十七）i=1i=nφii=1我们对Herbrand演绎的定义将通过使用（17）恒等式的右侧（而不是左侧）而不同于其更常规的定义。这种符号上的变化是不必要的，但它确实有助于简化我们的证明。设A表示一个任意的前趋正规句，如下面的原型，其中所选择的前趋正规句被定义为A。（18）x1y1x2y2. .， yn xn，yn）在一个上下文中，其中f∈（x），f∈（x，x）. f（x，x，. x）是新的功能符号，11212n1 2n方程（19）被称为方程（18）的Skolemization。ψ ψ（19） x1x2. . ，[x1，f（x1），x2，f（x1，x2）.. . xn，f∈（x1，x2. xn） ]在L是逻辑语言，α是公理系统的上下文中，我们将设CL和FL表示与以下项相关联的常数和函数符号的集合：L.类似地，Fα将表示与α公理相关联的“Skolemized”函数符号的集合因此，使用（18）和（19）的符号，设α表示公理系统，其中公理1，公理2，公理3.。，对于任意指数i，让其Skolemized函数符号携带诸如f 1、f2、f3、.等名称。 的商标化术语我我我这个有序对（α，L）将被定义为由下式生成的所有项的集合：集合C L中的常数与集合F α<$F L中的函数运算相结合。一个Skolemized公理的Herbrandized实例是一个与这个公理相同的句子，除了它 的 所 有 泛 量 化 变 量 都 被 Herbrandized 项 取 代 。 例 如 ， 在 T1 ， T2 ， T3. 是Herbrandized项，等式（20）是（19）公理的这样一个实例：ψ ψψ（20）双曲[T1，f（T1），T2，f（T1，T2）.. . Tn，f（T1，T2. Tn）]220D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）213设 表 示 的 逻 辑 常 数 。 公 理 系 统 α 中 的 一 个 Hebrandized 证 明定 义 为 α 的Herbrandized实例的有限集合，并在纯命题演算中证明，这些例子是反同义反复。定义2使用我们修改后的符号约定，定理1可以说有来自公理系统β的Herbrandized证明，当且仅当并公理系统β的一个加了句子<$的证明产生了<$的Herbrandized证明。更多的符号：让我们说，一个函数G（x1，x2，. xn）是一个非增长函数i ∈ G（x1，x2，. xn）≤ Max（x1，x2，. x n）。将函数集合S定义为算术控制集合i，S包括以下算术函数：加法、乘法和后继函数及其所有其它函数都是非增长函数。另外，定义一个术语不 作为算术控制项it是仅使用0、1和2的符号作为其输入常数并且其所有函数符号来自某个算术控制集S的项。 因此，如果G1和G2是非增长函数，则等式（21）表示算术控制项。（21）G1 [（1 + 1）<$（1 + 1）， 1+ 0 ] ∗G2（1 + 1 + 0， 1+1 + 1+1）此外，在Ct和Ft表示t中常数和函数符号的数量的上下文中，我们将使用以下符号：(i) MinG（t）将表示量2Ct+Ft。(ii) Val（t）将表示由项 t.例如，如果G1（x，y）= |x-y|并且G2（x，y）= Min（x，y），则等式（21）的项t将具有 Val （t）= 3^4 = 12 和MinG （t）= 225 （因为t包含12 个函数符号和13个常数符号）。引理4.1设t是满足不等式Val（t）≥ 4的算术控制项。则Val（t） Val（t）= 2k在这种情况下是有效的，因为前面的乘积有k个由k−1连接的常数2的出现乘法符号的出现。此外，很容易证明，不是2的幂的项永远不会以比2的幂更压缩的形式表示。他们超过的2的最大幂因此引理4.1对Val（t）≥4的所有项都有效。Q定义3对于一个固定常数B >0，函数集S被定义为一个B-有界算术集，它包括加法、乘法和后继算术函数以及它的所有其他函数。 G 满足约束的(22)G（x1，x2，. xn）≤ Max（x1，x2，. xn）时，Max（x1，x2，. x n） MinG（t）时，只要证明P包含Herbrand项t。(Such编码被称为定理4.3假设α是一个由B −有界有效的BRR语句组成的规范算术公理系统，并且Θ再次满足定义6的约定编码性质。 则任何来自公理系统α的关于θ的Herbrand证明P将满足不等式Θ（P）> B。关于定理4.3及其证明的一般性评论：在一个直观的定理4.3可以看作引理4.2和定义4- 6的结果这是因为定理4.3的假设中的B-有界有效性条件可以用来表明Herbrand证明P 必须包含一些术语 不 其中Val（t）≥B。 在这种情况下，引理4.2并且定义6将使P的Godeelnumb定理4.3的一个正式证明在附录中提供。我们的建议是，如果读者确实希望检查本附录的证明，他只有在完成本文的下两页之后才这样做。他们将解释定理4.3的形式主义如何使我们能够证明令人惊讶的结果，即I =0的Ax-3公理化是第二不完全性定理的Herbrandized版本的反阈值222D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）213111100定理4.4对于任意公理系统α和演绎方法 D，令Diagonal（α，D）表示下列句子：Diagonal（α，D）=从公理系统α与这个句子“Diagonal（α，D）“的结合中没有证明（使用演绎方法D）此外，在i= 1、2或3的上下文中，让Diag（i）表示Diagonal（α，D）的特殊变体，其中α = Ax−i，D表示Herbrand演绎。这两个结构都有很好的定义，Diag（i）也有一个WAR编码。定理4.4 早在1938年，Kleene就观察到[14]句子Diagonal（α，D）的一种形式被很好地定义了。最近，Willard [34，37]观察到这个句子在传统的算术语言中也有一个101推广[34，37]Q澄清意见：在解释定理4.4的含义时，人们应该有些谨慎。它并不表示Diag（i）在自然数的标准模型下是一个逻辑上有效的陈述。相反，它只是表明Diag（i）是一个定义良好的BRR句子。事实上，Diag（1）和Diag（2）可以被证明是逻辑上无效的语句（见脚注1）。 相反，定理4.5（下面）将证明Diag（3）在逻辑上有效。定理4.5设Ax-3* 表示Ax-3与句子Diag（3）的并集。那么Ax-3* 是一致的。（因此，Ax-3是第二不完全性定理在定义1的符号约定下的Her- brandized版本的Ax-3* 的一致性证明：为了建立矛盾证明，假设Ax-3* 是不一致的。然后，我们可以确定P的一个基本性质，即G？de？el？numb？rΘ（P）是小G？de？el？numb？r关于Ax-3* 的证明。 我们现在将从P构造一个替代Herbrand证明了R的，其中Θ（R）<Θ（P）。这样一个R的形式构造将使我们的反证法达到它所期望的目的，因为这样一个R的形式构造将使我们的反证法达到它所期望的目的。一 R 不可能存在（由于P我们的策略是使用定理4.3从P构造R。 定理4.3 与Ax-3* 有关（但与Ax-1或Ax-2的类似物无关这种区别的出现是因为Ax-3（以及Ax-3*）的归纳方案使用ΔR公式（不像更自由的Ax-1和Ax-2归纳方案，它们用ΔR公式代替Δ R公式）。1对于任意公理系统α，设αD表示α与附加句子Diagonal（α，D）的并。大多数的系统都不可能被证明是你会忽略Güodel的第二不完全性定理。 我们先前研究的要点[32，34，37，39]是通常的范式Wheerea nesessenallyclasicGüodel-lik ediagonalizationargummntllrender αD 我的意思是，我的意思是，我的意思是，mostt，但不是所有的系统都是αD。从而证明了在Herbrand演绎下，类Géodell-like方程对Ax-1和Ax-2都是适用的. 另一方面，本文的最后结果（定理4.5）将证明Ax-3是完全不同的。D.E. Willard/Electronic Notes in Theoretical Computer Science 165（2006）21322311较难管理的Δ0表达式）由于所有Ax-3*句子，我们可以应用定理4.3得出结论，对于某个BΘ（P），Ax-3* 的公理句不是B-有界有效的公理句。 此外，很明显，Ax-3的所有公理都具有无限的有效性水平（即它们对所有可能的B都是有界有效的。）因此，这两个观察结果意味着Diag（3）不是B−有界有效的（简单地说，因为Ax-3* 中的某个公理必定不是B−有界有效的，而Diag（3）是Ax-3* 中唯一不是Ax-3成员的公理。后一个观察，结合Diag（3）< (This是因为Diag（3）因此，Θ（R）

下载后可阅读完整内容，剩余1页未读，立即下载