理由逻辑（五）

尽管算术语义是不可能的，但在（Fitting 2008）中，为 \mathsf{LP} 的版本给出了可能的世界语义和公理证明理论，其量词范围超过正当性。健全性和完整性得到了证明。此时，可能的世界语义与算术语义分离，这可能会也可能不会引起警报。还表明，通过将 \Box Z 翻译为“存在一个证明 x 使得 x : Z^{*}”，\mathsf{S4} 嵌入到量化逻辑中，其中 Z^{*} 是 Z 的翻译。虽然这个逻辑有点复杂，但它已经找到了应用，例如，在（Dean and Kurokawa 2009b）中，它被用来分析知识者悖论，尽管有人对此分析提出了反对（阿洛-科斯塔和岸田，2009 年）。

Artemov 和 Yavorskaya (Sidon) (2011) 中提出了一阶证明逻辑 \textsf{FOLP}，其中带有单个变量的量词。在 \textsf{FOLP} 中，证明断言由 t{:}_X A 形式的公式表示，其中 X 是单个变量的有限集，这些变量被视为可供替换的全局参数。 X 中出现的所有在 A 中自由的变量在 t{:}_X A 中也是自由的。A 的所有其他自由变量都被视为局部变量，因此绑定在 t{:}_X A 中。例如，如果 A(x, y) 是原子公式，则在 p{:}_{\{x\}} A(x,y) 中，变量 x 是自由的，变量 y 是束缚的。同样，在 p{:}_{\{x,y\}} A(x,y) 中，两个变量都是自由的，而在 p{:}_{\emptyset} A(x,y) 中，x 和 y 都不是自由的。

证明（论证）由不包含单个变量的证明项表示。除了 \textsf{LP} 运算之外，还有一系列关于证明项的运算，{\sf gen}_x(t)，对应于单个变量 x 的泛化。控制该操作的新公理是 t{:}_X A {\rightarrow}{\sf gen{:}_x(t)}_X\forall x A，其中 x\not\in X。 \textsf 的完整列表{FOLP} 原理以及一阶 \textsf{S4} 的实现可以在 Artemov 和 Yavorskaya (Sidon) (2011) 中找到。 \textsf{FOLP} 的语义已在 Fitting (2014a) 中开发。

9. 历史注释

最初的论证逻辑系统，即证明逻辑 \mathsf{LP}，于 1995 年在（Artemov 1995）中引入（也参见（Artemov 2001）），其中首先建立了诸如内化、实现、算术完整性等基本属性。 \mathsf{LP} 为哥德尔的可证明性逻辑 \mathsf{S4} 提供了预期的可证明性语义，从而为直觉命题逻辑提供了 Brouwer-Heyting-Kolmogorov 语义的形式化。认知语义和完整性（Fitting 2005）首先是为 \mathsf{LP} 建立的。 \mathsf{LP} 的符号模型和可判定性归功于 Mkrtychev (Mkrtychev 1997)。复杂性估计首次出现在（Brezhnev and Kuznets 2006，Kuznets 2000，Milnikel 2007）中。所有可判定性和复杂性结果的全面概述可以在（Kuznets 2008）中找到。系统 \mathsf{J} 、 \mathsf{J4} 和 \mathsf{JT} 首次在（Brezhnev 2001）中以不同的名称和稍微不同的设置被考虑。 \mathsf{JT45} 独立出现在 (Pacuit 2006) 和 (Rubtsova 2006) 中，而 \mathsf{JD45} 则独立出现在 (Pacuit 2006) 中。单一结论证明的逻辑已在（Krupski 1997）中找到。 (Artemov 2006) 提供了一种基于合理知识的更通用的常识方法。 (Renne 2008, Renne 2009) 研究了论证逻辑和带有论证的动态认知逻辑的博弈语义。论证逻辑与逻辑全知问题之间的联系在（Artemov and Kuznets 2009，Artemov and Kuznets 2014，Wang 2009）中进行了研究。论证逻辑这个名称是在（Artemov 2008）中引入的，其中 Kripke、Russell 和 Gettier 的例子被形式化；这种形式化已用于解决悖论、验证、隐藏假设分析和消除冗余。在（Dean and Kurokawa 2009a）中，论证逻辑被用于分析知识者和可知性悖论。

关于论证逻辑的前两本专着于 2019 年出版（Artemov 和 Fitting 2019、Kuznets 和 Studer 2019）。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。