普雷斯堡尔算术

普雷斯堡尔算术是自然数加法的一阶理论，为纪念1929年提出的莫伊泽斯-普雷斯堡尔而命名。普雷斯堡尔算术的签名只包含加法运算和平等，完全省略了乘法运算。该公理包括一个归纳的模式。普雷斯堡尔算术比佩阿诺算术弱得多，佩阿诺算术包括加法和乘法运算。与皮亚诺算术不同，普雷斯堡尔算术是一种可解理论。这意味着，对于普氏算术语言中的任何句子，可以通过算法确定该句子是否可以从普氏算术的公理中得到证明。然而，正如Fischer&Rabin(1974)所显示的，这种算法的渐进运行时间的计算复杂性至少是双指数的。

Presburger算术的语言包含常数0和1以及二进制函数+，被解释为加法。在这种语言中，Presburger算术的公理是以下的普遍封闭。¬(0=x+1)x+1=y+1→x=yx+0=xx+(y+1)=(x+y)+1让P(x)是Presburger算术语言中的一个一阶公式，有一个自由变量x（可能还有其他自由变量）。那么下面的公式是一个公理：(P(0)∧∀x(P(x)→P(x+1))→∀yP(y)。(5)是一个归纳法的公理模式，代表无限多的公理。这些不能被任何有限数量的公理所取代，也就是说，在一阶逻辑中，Presburger算术是不能被有限公理化的。普雷斯堡尔算术可以被看作是一个具有平等性的一阶理论，它恰恰包含了上述公理的所有后果。或者，它可以被定义为那些在预定解释中为真的句子的集合：非负整数与常数0、1的结构，以及非负整数的加法。Presburger算术被设计为完整和可解的。因此，它不能将诸如可分性或首要性等概念形式化，或者更广泛地说，任何导致变量乘法的数字概念。然而，它可以制定可分性的个别实例；例如，它证明对于所有的x，存在y:(y+y=x)∨(y+y+1=x)。这说明每个数字都是偶数或奇数。

莫伊兹-普雷斯堡尔证明普雷斯堡尔算术是。一致。在普雷斯堡尔算术中，没有任何语句可以从公理中推导出来，而其否定也可以推导出来。完整。对于普雷斯堡尔算术语言中的每一条语句，要么可以从公理中推导出它，要么可以推导出它的否定。可解码。存在一种算法来决定普雷斯堡尔算术中的任何给定语句是定理还是非定理。普雷斯堡尔算术的可解性可以用量子消除法来证明，并辅以算术同构的推理。用来证明量词消除算法的步骤可以用来定义递归公理化，它不一定包含归纳的公理模式。相比之下，作为对Entscheidungsproblem的否定答案的结果，Peano算术，也就是用乘法增强的Presburger算术，是不可解的。根据哥德尔不完全性定理，Peano算术是不完全的，它的一致性在内部是无法证明的（但见Gentzen的一致性证明）。

普雷斯堡尔算术的决策问题是计算复杂性理论和计算中一个有趣的例子。假设n是Presburger算术中一个语句的长度。然后Fischer&Rabin(1974)证明，在最坏的情况下，该语句在一阶逻辑中的证明的长度至少有{displaystyle2{2{cn}}}，对于某个常数c>0来说。因此，他们对Presburger算术的决策算法的运行时间至少是指数级的。Fischer和Rabin还证明，对于任何合理的公理化（在他们的论文中精确定义），都存在长度为n的定理，其证明的长度是双指数的。直观地说，这表明计算机程序所能证明的东西是有计算限制的。费舍尔和拉宾的工作还意味着，只要输入量小于相对较大的界限，就可以用Presburger算术来定义正确计算任何算法的公式。界限可以增加，但只能通过使用新的公式。另一方面，Oppen(1978)证明了PresburgerArithmetic的决策程序的三重指数上界。Berman(1980)使用交替的复杂度等级证明了一个更严格的复杂度界限。Presburger算术（PA）中的真语句集对于TimeAlternations(22nO(1),n)来说是完整的。因此，其复杂度介于双指数非决定性时间（2-NEXP）和双指数