可证明的逻辑（二）

4.可证明逻辑和PEALO算术

从时代GL被制定起来，研究人员想知道是否足以满足PEANO算术（PA）等正式理论（PA）：是否可以以所谓的模态语言表达的可释放概念，并且可以在PEANO算术中证明这一切或者应该将更多原则添加到GL中？ 为了使这种概念更精确，我们将实现（有时称为翻译或解释）定义为函数f，该函数f为算术，其中算术的句子的每个命题原子分配

f（⊥）=⊥;

f尊重逻辑连接，例如，f（b→c）=（f（b）→f（c））; 和

◻被翻译为可加速的谓词省，所以f（◻b）= prov（⌜f（b）⌝）。

4.1算术声音

在20世纪70年代初，它已经清楚了，GL是算法相对于PA，正式的声音：

如果gl⊢a，那么对于所有的实现f，pa⊢f（a）。

给出一些味道的元数学，让我们勾勒出声音证明。

算术声音证明剪影。 PA确实证明了引诱性Tautologies的实现，并且GL的分布公理的可证明性转化为

pa⊢prov（⌜a→b⌝）→（省（⌜a⌝）→省（⌜b⌝））

对于所有公式A和B，这只是Löb的第二个衍生性条件（参见第1节）。 此外，Pa obeys Modus Ponens，以及泛化规则的翻译：

如果pa⊢a，那么pa⊢prov（⌜a⌝），

这只是Löb的第一个衍生能力条件。 最后，主要公理（GL）的翻译确实可以在PA：

pa⊢prov（⌜prov（⌜a⌝）→a⌝）→省（⌜a⌝）。

这正是Löb在第1节中提到的正式版本。

让我们从他的衍生条件（形式化版本的证明相似）给予Löb的定理本身证明的剪影。 该证据基于Gödel的对角引理，这表示对于任何算术公式C（x），有一个算术公式b

pa⊢b↔c（⌜b⌝）。

用文字说，公式B说“我有房产C.”

Löb的定理证明： 假设pa⊢prov（⌜a⌝）→a; 我们需要展示pa⊢a。 通过对角化引理，有一个公式b

pa⊢b↔（省（⌜b⌝）→一个）。

从这完全由Löb的第一和第二次衍生性条件加上一些命题推理

pa⊢prov（⌜b⌝）↔prov（⌜prov（⌜b⌝）→a⌝）。

因此，再次由Löb的第二条件，

pa⊢prov（⌜b⌝）→（省（⌜prov（⌜b⌝）⌝）→省（⌜a⌝））。

另一方面，Löb的第三条件给出了

pa⊢prov（⌜b⌝）→省（⌜prov（⌜b⌝）⌝），

从而

pa⊢prov（⌜b⌝）→省（⌜a⌝）。

与pa⊢prov（⌜a⌝）→a一起的假设一起，这给了

pa⊢prov（⌜b⌝）→一个。

最后，对角度化引理产生的等式意味着pa⊢b，因此pa⊢prov（⌜b⌝），因此

pa⊢a，

根据需要。

请注意，取代⊥在Löb的定理中，我们得出了pa⊢¬prov（⌜⊥⌝）意味着PApa⊢⊥，这只是哥德尔第二次不完整定理的矛盾。

4.2算术完整性

可证明逻辑的标志性结果是R.Solovay的算法定理1976年，表明GL确实适用于PEANO算术：

只有在所有实现F，PApa⊢f（a）时才。

本定理基本上说，模态逻辑GL捕获了PEANO算术可以在模态术语中真实地说出其自身的可加工谓词的所有内容。 从左到右的方向，上面讨论了GL的算术声音。 Solovay阐述了另一种，更加困难，方向难以描述。 他的证据是基于复杂的自我参考技术，这里只能给出一个小的一瞥。

Segerberg的模态完整性定理是Solovay对PEANO算术的算术完整性证明的重要第一步。 假设GL不证明模态配方A.然后，通过模态完整性，有一个有限的传递反离身性树，使得该树根的A是假的。 现在，Solovay设计了一种巧妙的方式来模拟Peano算术的语言中这样的有限树。 因此，他发现从模态公式到算术句的实现f，使得PEANO算术不证明F（a）。

Solovay的完整性定理提供了一种替代方式来构建许多在PEANO算术中不可提供的算术句子。 例如，很容易制作一个可能的世界模型来表明GL不证明◻p∨◻¬p，所以通过Solovay的定理，有一个算术句子f（p），使得Peano算术不证明Prov（⌜f（P）⌝）∨prov（⌜¬f（p）⌝）。 特别是，这意味着F（p）和¬f（p）都不可在Peano算术中提供; 对于假设pa⊢f（p），然后由öb的第一个条件和命题逻辑，pa⊢prov（⌜f（p）⌝）∨prov（⌜¬f-f（p）⌝），导致矛盾，同样一个人假设pa⊢¬f-f（p）。

Solovay的定理是如此重要，因为它表明，PEANO算法等未定性正式理论的一个有趣的片段，即哪种算术可以以命题术语在其自身可保释谓词中表达 - 可以通过可解除的模态研究Logic，GL，具有呈现可能的世界语义。

5.可保释逻辑的范围

在本节中，讨论了关于可保释逻辑研究的一些趋势。 一个重要的股线涉及GL的范围的限制，主要问题是，除了PEANO算术之外的正式理论，是GL适当的命题可加工逻辑吗？ 接下来，我们讨论了更具表现力的模态语言的命题证明逻辑的一些概括。

5.1边界

自20世纪80年代后期以来，逻辑学家已经调查了许多其他算术系统，这些算术系统比PEANO算法弱。 这些逻辑管理员通常从可计算问题中获取灵感，例如对多项式时间中可增的功能的研究。 他们给出了问题的部分答案：“算术理论是索洛瓦伊的算术完整性定理（关于适当的保证谓词）仍然持有？” 要讨论这个问题，需要两个概念。 Δ0-公式是算术公式，其中所有量子均由术语界定，例如

∀y≤ss0∀z≤y∀x≤y+ z（x +y≤（y +（y + z））），

其中s是继任运算符（“+1”）。 算术理论IΔ0（我代表“诱导”），类似于PEANO算法，除了它允许较少的诱导：感应方案

一个（0）∧∀x（一个（x）→一个（sx））→∀xa（x）

仅限于Δ0-公式A.

作为De Jongh等人（1991）指出，算术完整性肯定适用于满足以下两个条件的理论T：

T证明了Δ0-公式的诱导，并且T证明EXP，表达所有X的公式，其功率2x存在。 更标准的符号：T延伸IΔ0+ exp;

T不证明形式∃xa（x）的任何误报，其中a（x）aΔ0公式。

对于此类理论，GL HOLD的算术声音和完整性，条件是◻转化为PROVT，对T的自然保险性谓词谓词谓词为D.为模态句子A：

gl⊢a如果且仅在为所有实现f，t⊢f（a）。

尚不清楚，但条件1是否在可保释逻辑范围内给出了下限。 例如，它仍然是一个开放的问题，无论gl是IΔ0+ω1的可保释逻辑，它在ω1中的IΔ0+ exp的一个理论稍微弱，是所有x的公理，它的功率Xlog（x）存在。 可证明的逻辑GL是关于IΔ0+ω1的算术声音，但除了Berarducci和verbrugge（1993）的一些部分结果，提供与IΔ0+ω1一致的算术实现，用于限制一类句子与GL一致，问题仍然是开放的。 它的答案可以铰接计算复杂理论中的开放问题。

De Jongh等人的上述结果。 显示了可保释逻辑的强大特征：对于许多不同的算术理论，GL确切地捕获这些理论对自己的可加工谓词的原理。 同时这是一个弱点。 例如，命题可证明逻辑不指向这些理论之间的任何差异，这些理论是有限的，这些理论和那些不是那些的理论。

5.2解释性逻辑

为了能够以模态语言发言，关于理论之间的重要区别，研究人员以许多不同的方式扩展了可保释的逻辑。 让我们提及一些。 一个扩展是添加二进制模态⊳，其中对于给定的算术理论t，模态句子a⊳b意味着在t + a中占据“t + b”（Švejdar，1983）。 De Jongh和Veltman（1990）调查了几种可解释性逻辑的模态语义，而De Jongh和Visser（1991）则证明了最重要的明确定点财产。 visser特征是最常见的最常见的公共结构理论的可解释性逻辑，Berarducci和Shavrukov独立地表征了PA的一个，这不是有限的公正。 看来，实际上，有限的公共理论的可解释性逻辑与Peano算术的可解释性逻辑不同（参见Montagna 1987; Visser 1990,1998; Berarducci 1990，Shavrukov 1988; Jooosten和Wisser 2000）。

5.3命题量词

延长命题可证明逻辑框架的另一种方法是添加命题量词，因此可以表达像Goldfarb这样的原则：

∀p∀q∃r◻（（◻p∨◻q）↔◻r），

对任何两个句子说，有一个第三句，如果才能提供第一个两个句子中的任何一个。 这一原理在PEANO算术中可以证明（参见例如Artemov和Beklemishev 1993）。 GL的一组GL的句子与算术量子是算术有效的，结果是不可察明的（Shavrukov 1997）。

5.4日本的双峰和多种可加工逻辑

Japaridze（1988）双峰逻辑GLB有两个类似的可保释操作员，其中由[0]和[1]表示，分别具有它们的双重次运算符⟨0⟩。 在Japaridze的解释中，人们可以考虑[0]作为PEANO算术中标准的可加工谓词。 另一方面，[1]对应于更强的可加工谓词，即ω-Provabilty。

让我们定义理解这一预期对GLB的概念所需的概念。 算术理论t被定义为ω-conventent，如果只有在所有具有自由变量x的公式a，所有n的所有公式a都意味着t⊬∃xa（x）; 这里，IN是n，即术语SS ... SS ... SS ... S0，其具有第n个出现的继承操作员S. PEANO算术（PA）是最着名的ω-一致理论的示例（另见Gödel的不完整定理）。 现在让PA +是算术理论，其公理是PA的PA与所有句子∀x¬a（x），使得对于每个n，pa⊢¬a（in）。 现在ω-Provability只是在PA +中证实，因此它是ω-一致性的双重。

Japaridze的双峰可保释逻辑GLB可以通过GL（参见第2部分）的公理和规则，单独配制的[0]和[1]。 此外，GLB有两个混合公理，即：

[0]一个→[1]一个

⟨0⟩a→[1]⟨0⟩a

Japaridze的逻辑是可判定的并且具有合理的Kripke语义，并且算法算法和与Peano算术（Japaridze 1988，Booolos 1993）完整。

近年来，日本GLB的GLB的GLB的多种多样性类似物。 GLP具有无限的许多像可保释的运营商，用盒子[n]表示每个自然数n，他们的双重⬦的运算符⟨n⟩。 同样，人们可以考虑[0]作为站立于PEANO算术中的标准保证性谓词，⟨1⟩为ω-Provency，等等。 通过从GL（参见第2部分）的原理和规则开始，GLP已经致粗化，每个[n]分开配制。 此外，GLP有三种混合的公理方案，即由Beklemishev（2010）制定：

[m] a→[n] a，用于m≤n

⟨k⟩a→[n]⟨k⟩a，用于k＜n

[m] a→[n] [m] a，用于m≤n

GLP已经赋予了克里普克语义，依据它所完成，并且还被证明在PEANO算术方面算是算法（见Beklemishev 2010A，2011A）。 就像GL一样，GLP的决策问题是PSPACE-COMPLEAT（Shapirovsky 2008），而其闭合片段是多项式时间可解除（Pakhomov 2014）。

在过去的三十年中，已经证明了许多结果的结果是强加力谓词的多元逻辑GLP。 以下遵循一些特别富有成效的主题：

GLP的封闭片段（见Ignatiev 1993; Beklemishev，Joosten和Vervoort 2005）;

GLP和校验理论顺序（Beklemishev 2004）;

GLP的邻里语义（Shamkanov 2020）;

GLP的插值定理（参见Beklemishev 2010B，Shamkanov 2011）;

拓扑语义与集合理论之间的关系，其中特殊的大型基本公理和静止反射（参见Beklemishev 2011b; Beklemishev和Gabelaia 2013,2014;Fernández-二进制2014; Aguilera和Fernández-Duque 2017）。

5.5谓词可保释逻辑

最后，一个人可以研究谓词可证明的逻辑。 语言是没有函数符号的谓词逻辑，以及操作员◻。 在这里，情况变得更加复杂，而是在命题可加工逻辑的情况下。 首先，GL的直接量化版本没有固定点属性，不适用于任何类别的KRIPKE帧，并且在PEANO算术（Montagna，1984;见Rybakov 2023年最近的概括）。 然后出现问题：是否有任何恰当的公正谓词可证明的逻辑，这是足够的，证明了证明的有效原则？ 答案不幸的是，响亮的否定：瓦达尼亚（1986年）根据Artemov（1985A）的思想证明了谓词可证明逻辑的一组句子，其实一于PA甚至没有递归放心但Π

0

2

-Complete，所以它没有合理的公理化。 visser和de Jonge（2006）显示，通过证明概括，瓦达尼亚的定理没有逃脱：对于广泛的算术理论T，所有的谓词可保证逻辑的句子都可以在t中得到证实结果是π

0

2

-CONPLETE。 然而，近距离和joosten（2020,2022）表明，基于包含命题连接∧，模态运算符⬦和量词∀的严格正面语言的谓词可保释逻辑片段是算术完成和仍然存在可判定。