可证明的逻辑（三）

5.6其他概括

在上面的讨论中遗漏是许多其他重要的可证明逻辑及其延伸的研究。 感兴趣的读者指向以下区域：

直觉算术的可加工逻辑（参见Troelstra 1973; Visser 1982,1999,2002，2008; Iemhoff 2000,2001,2003; Ardeshir和Mojtahedi 2018; LITAK和visser 2018，即将到来; Mojtahedi 2022 [其他互联网资源]; visser和zoethout 2021; van der Giessen和Iemhoff 2021; van der Giessen 2023; Shillito 2023）;

可证明逻辑分类（参见visser 1980，Artemov 1985b，Beklemishev 1989，Beklemishev等，1999）;

Rosser订购和证明加速（参见Guaspari和Solovay 1979，Švejdar1983，Montagna 1992）;

具有可证明的不同理论的有证明运营商的两种双峰证实逻辑（见Carlson 1986;smoryński1985; Beklemishev 1994,1999; Visser 1995）;

标准可证明的可证明逻辑与外部枚举PA的不寻常可加速度谓词，例如Feferman和Parikh的可证明谓词和缓慢可加速度谓词（参见Feferman 1960; Parikh 1971; Montagna 1978; visser 1989; carbone和montagna 1990; Shavrukov 1994;Lindström1994,2006; Henk和Pakhomov 2016（其他互联网资源））;

利用可证明和可解释性逻辑分析Gödel的第二个不完整定理（Visser 2016; 2020）;

明确证明的逻辑（见Artemov 1994,2001; Artemov和Montagna 1994; Yavorskaya 2001; Artemov和Iemhoff 2007; Kuznets和Studer 2019）;

可证明逻辑与辩护逻辑之间的对应关系（参见Artemov和Nogina 2005; Shamkanov 2016（其他互联网资源）;适合2020）;

基于相关性逻辑R的相关可保释逻辑（参见Mares 2000）;

证明逻辑证明理论的应用（见Beklemishev 1999,2003，2004,2005，2006）;

证明模态逻辑的证明理论与可保释逻辑GL密切相关，即GRZegorczyk逻辑（GRZ）和弱格尔茨科克逻辑（WGRZ）（参见LITAK 2007; Maksimova 2014;Goré和Ramanayake 2014; Dyckhoff和Negri 2016; Savateev和Shamkanov 2019,2021）;

积极的可证明逻辑和反射微积分（参见Beklemishev 2012，2014,2018a，2018b; Dashkov 2012）;

多种可证明逻辑GLP的概括，即具有杂项许多方式的可证明逻辑（参见Beklemishev等，2014;Fernández-duque和Joosten 2013a，2013，2014，2014年，2018; Joosten 2021; Beklemishev和Pakhomov 2022）;

可证明逻辑与μ-微积分之间的关系（见Van Benthem 2006，Visser 2005，Alberucci和Facchini 2009）; 和

可证明代数，也称为对角线化代数或Magari代数（参见Magari 1975a，1975b; montagna 1979,1980a，1980b; bernardi和d'aquino 1988; Shavrukov 1993a，1993b，1997; Zambella 1994;对于近期结果的基础理论，见2015年Pakhomov 2012年，2015年（其他互联网资源），2015年。

对于希望为可赋予可证明逻辑和概括的领域提供贡献的读者，Beklemishev和visser（2006年）提出了一个有趣的开放问题的注释列表。

6.哲学意义

尽管所谓的可证明逻辑是一种具有一种“必要性”运营商的模态逻辑，但它抵消了Quine（1976）的争议批评的模态概念，因为它已经明确和明确的算术解释。 例如，与许多其他模态逻辑不同，具有嵌套模态的公式，如◻⬦p→◻⊥不成问题，也没有任何争议，也没有任何争议。 事实上，可证明的逻辑体现了Quine（1953）所阐述的句法治疗的所有Desiderata。

Quine的主箭头指向模态谓词逻辑，尤其是在量子范围内包含模态运算符的句子的构建（“量化”）。 然而，在谓词可证明的逻辑中，其中量词范围在自然数范围内，De Dicto和De Re模式都具有简单的解释，与其他模态逻辑的情况相反（参见DE DICTO / de RE SINTINENTENT的说明）。 例如，公式如

∀x◻∃y（y = x）

根本不是问题。 如果将数字N分配给X，则对于此分配IFF，◻∃y（y = x）为trueff句子（y = in）在Peano算术中可提供句子; 这里，IN是n，即术语SS ... SS ... SS ... S0，其具有第n个出现的继承操作员S. 对于自然数的标准模型中的所有N，这句话是如此，并且∀x◻∃y（y = x）甚至可以在Peano算术中提供。

顺便说一句，巴尔卡州公式

∀x◻a（x）→◻∀xa（x）

对于整数而不是真的，更不用说可证明（例如，需要（x）公式“x没有编码⊥”）。 它的交谈

◻∀xa（x）→∀x◻a（x）

另一方面，对于任何公式A的PEANO算法可提供。

可证明的逻辑具有来自其他模态逻辑的原则非常不同，即使是具有看似类似的目的的原则。 例如，虽然可证明的逻辑在算术的正式理论中捕获可证明，但是，算术，认识逻辑致力于描述知识，这可以被视为一种非正式可用的可加工。 在许多版本的认识逻辑中，最重要的原则之一是真相公理（5）：

s5⊢◻a→a，（如果一个人知道，那么a是真的）。

类似的原则显然不会持有GL：毕竟，

如果gl⊢◻a→a，那么gl⊢a。

因此，似乎误导了比较两个概念的强度或将它们组合在一个模态系统中。

自20世纪40年代以来，数学哲学家在非正式可证明或绝对可证明的概念（Gödel1946，Kreisel 1967）的概念中，包括关于其适当定义的争议（见Leach-Krouse 2013;肯尼迪2014; Crocco 2019;对于对这些争议的良好讨论）。 Williamson（2016）给出了以下定义：“只有在原则上以正常的数学过程所知，才能确认数学假设。”。 无论如何，很明显，绝对可证明的概念与给定正式系统中的正式保证的概念非常不同，这是本文其余的关于可保释逻辑的中央概念。

与绝对可证明的陈述的概念有关，这是绝对不可判断的陈述，即，既不能够绝对可证明的那些陈述A NOR¬A。 一个有趣的问题是哥德尔的分离持有：是“心灵无法机械化”或“绝对无可救药的陈述”的情况吗？ 迷人接受这个问题可以在（Koellner 2016，Leach-Krouse 2016，Williadmson 2016）中找到。

讨论哥德尔的不完整性定理的后果有时涉及围绕可证明概念的困惑，引起人类可以在“了解”定理中击败正式系统; 参见（戴维斯1990,1993;Franzén1995;Lindström2001），以便对此类索赔的良好批判性讨论。

总而言之，正式可规定是一个精确定义的概念，比真理和知识更重要。 因此，保证范围内的自我引用不会导致像骗子这样的语义悖论。 相反，它导致了关于数学的一些最重要的结果，例如Gödel的不完整定理。