自动推理（八）

柏拉图的形式（例如三角形）

\Phi_T =_{df}\iota x(A!x \amp \forall F(xF \equiv \Box \forall x(Tx \rightarrow Fx)))

莱布尼茨的概念（例如亚历山大）

c_a =_{df}\iota x(A!x \amp \forall F(xF \equiv Fa))

弗雷格数

0 =_{df}\iota x(A!x \amp \forall F(xF \equiv\lnot\exists yFy))

1 =_{df}\iota x(A!x \amp \forall F(xF \equiv \exists y(Fy \amp \forall z(Fz \rightarrow z = y))))

ETC。

真理价值观

\top =_{df}\iota x(A!x \amp \forall F(xF \equiv \exists p(p \amp F = [\lambda y p])))

\bot =_{df}\iota x(A!x \amp \forall F(xF \equiv \exists p(\lnot p \amp F = [\lambda y p])))

情况和可能的世界

\textit{情况}(x) =_{df} \forall F(xF \rightarrow \exists p(F = [\lambda y p]))

s \vDash p =_{df} s[\lambda y p]

\textit{PossibleWorld}(x) =_{df} \Diamond \forall p((s \vDash p) \equiv p)，由此可以推导出莱布尼兹原理，即如果在所有世界中 p 为真，则 p 是必要的， \vdash \ Box p \equiv \forall w(w \vDash p)，以及刘易斯原理，即对于世界可能的每一种方式，都有一个世界是方式， \vdash \Diamond p \equiv \exists w(w \vDash p)

理论数学对象（例如 ZF 中的空集）

\varnothing_{ZF} =_{df}\iota x(A!x \amp \forall F(xF \equiv ZF \vDash F\varnothing))

AOT 正在不断发展，有关该理论的更多详细信息，读者可以参考其最新的表述之一 (Zalta 2022)。 AOT 的计算分析是由 Fitelson 和 Zalta (Fitelson & Zalta 2007) 使用一阶系统 Prover9 开创的。使用一阶证明者对 AOT 等高阶理论进行计算研究具有固有的局限性，最好在高阶证明者的计算框架内工作。然而，AOT 基于与经典高阶逻辑显着不同的逻辑基础，理想情况下，人们希望使用 AOT 本身的定理证明器。当然，这样做的缺点是，人们需要构建这样一个证明器，而这并不是一项简单的任务。但是，通过将 AOT 的浅层语义嵌入（SSE）构建到现有的高阶证明器中，例如，可以在很大程度上“近似”这样一个系统。 Isabelle/HOL，研究人员可以忠实地表示 AOT 的公理和演绎系统（Benzmüller 2019，Kirchner 2021）。在此设置中，Isabelle/HOL 充当 SSE 的元逻辑框架，为 AOT 提供“自定义”定理证明器。但总是需要权衡，构建嵌入也带来了一系列挑战。其中的关键是，AOT 的某些方面可以很容易地用关系类型理论来表述，但在 Isabelle/HOL 的基础功能类型理论中重新表述时却提出了挑战。例如，并非 AOT 中的每个公式都可以转换为 lambda 项，除非愿意面对矛盾！凭借一些独创性，人们可以使用 Isabelle/HOL 的函数演算来定义一些复杂类型，以帮助构建 AOT 的 Aczel 模型，然后在自由逻辑的上下文中根据复杂类型解释那些有问题的 lambda 表达式。底线：AOT 的每个公式都可以表示为 lambda 项，但并非所有这些项都表示；因此，保持了一致性。

Isabelle/HOL 中 AOT 的 SSE 的关键方面包括使用 Aczel 模型构建嵌入的模型、再现 AOT 的语法、扩展 Isabelle 的“外部”语法（以应对 AOT 中推理的某些挑战）、表示抽象语义AOT的，指定Hilbert \varepsilon算子的逻辑，表示现实算子的逻辑，表示超内涵性，推导公理系统和演绎系统，以及其他考虑因素 - 有关详细信息，请参阅 Kirchner 2021。其中最突出的是抽象层的使用（Kirchner 2017），它在确定目标理论的演绎系统（此处为 AOT）的陈述的可推导性方面发挥着重要作用。通过证明AOT的公理和推导规则在SSE中语义上有效来构建抽象层；此后，所有后续推理（例如由 Isabelle/HOL 的主要自动推理工具 sledgehammer 进行的推理）都仅限于依赖派生公理和演绎规则本身，并且可能不涉及底层语义。这项工作大约用了 Isabelle/HOL 的 25,000 行：大约 5,000 行用于构建所需的模型结构和语义以及 AOT 的语法表示，其余 20,000 行用于 AOT 中的逻辑推理。在嵌入下，AOT 的计算探索可以以更“原生”的方式进行，如下图所示，以 Isabelle/HOL 表示法的 9 行证明表明没有对象既普通又抽象（Kirchner 2021）：

第7571章

第7572章 证明（规则“raa-cor：2”）

第7573章

第7574章

7575 使用“∃E”[旋转]通过爆炸

第7576章

第7577章 (metis "&E"(1) "合取简化"(2) "≡E"(1)

第7578章

7579 qed

另外 1,000 行这样的计算推导导致的结果是存在无法通过示例区分的不同抽象对象： \exists x\exists y(A!x \amp A!y \amp x \ne y \amp \forall F(Fx \equiv Fy))。更多的推导得到了一个重要的新发现，它提供了分析方法来确定 AOT 中的 lambda 表达式是否表示： [\lambda x \phi]\downarrow \equiv \Box \forall x\forall y(\forall F( Fx \equiv Fy) \rightarrow(\phi \equiv \phi(y/x)) 且 y 在 \phi 中不自由 并且，作为推论， [\lambda x \phi]\downarrow。 \rightarrow \forall x\forall y(\forall F(Fx \equiv Fy) \rightarrow \Box(\phi \equiv \phi(y/x)) 其中 y 在 \phi 中不自由。后者的证明在SSE 的上下文采用 Isabelle/HOL 中的 20 行，如下所示：

第8761章

第8762章

第8763章 证明（规则“→I”；规则GEN；规则GEN；规则“→I”）

第8764章

第8765章

第8766章

第8767章

第8768章

第8769章

第8770章

8771 通过爆炸使用“∀E”

第8772章

第8773章

第8774章

8775通过爆炸使用“∀E”

第8776章

第8777章 不服输

第8778章

第8779章

8780 奎德

在建立关于基本逻辑对象、受限变量、扩展关系理解和可能世界的进一步结果后，计算探索可以重定向到 Dedekind-Peano 算术，其中自然数的假设在没有数学原始概念的系统中正式导出和数学公理——弗雷格定理——从而支持 AOT 可以为数学对象提供哲学基础的主张。 Kirchner 2021 的计算方法以先前在 Zalta 1999 中给出的证明大纲为指导，但现在在 Isabelle/HOL 中重建，产生了完整细节和形式的假设推导。

假设1

AOT_定理“0-n”：❬ [ℕ]0 ❭

假设2

AOT_定理“0-pred”： ❬ ←∃n [ℙ]n 0 ❭

假设3

AOT_theorem "no-same-succ": ❬ ∀n∀m∀k([ℙ]nk & [ℙ]mk → n = m) ❭

假设4

AOT_theorem "th-succ": ❬ ∀n∃!m [ℙ]nm ❭

假设5

AOT_定理归纳： ❬ ∀F([F]0 & ∀n∀m([ℙ]nm → ([F]n → [F]m)) → ∀n[F]n) ❭

上述计算探索是使用 AOT 的二阶片段完成的，但 SSE 可以扩展到完整的高阶逻辑 AOT (Kirchner 2021)，可应用于理论数学分析。需要强调的是，将目标理论嵌入到现有证明者的高阶逻辑中不仅仅会导致理论的形式化：SSE 允许在目标理论中发现新结果，如上例所示，以及目标理论本身的研究和进一步发展，例如将理论置于更坚实的基础上，例如避免已知的悖论（Zalta 2018，Kirchner 2021）。这里描述的 AOT 的计算分析也可以被解释为在高阶证明者的框架内对嵌入理论（简单的和复杂的）概念的又一次测试。它说明了该方法的强大功能和便利性，自动推理领域的研究人员可能需要认真考虑在定理证明工作中使用 SSE（Benzmüller 2019）。

莱布尼茨的梦想是拥有一个通用特征和微积分推理器，使我们能够以与几何和分析大致相同的方式在形而上学和道德中进行推理；也就是说，要像会计师那样解决哲学家之间的争端：“拿起笔，坐在算盘前，如果朋友愿意的话，可以叫来朋友，互相说：让我们来算一算吧！”从上述自动推理的应用来看，人们会同意研究人员的观点，即这些结果在某种程度上实现了莱布尼茨的计算形而上学目标（Fitelson & Zalta 2007，Benzmüller & Paleo 2014）。

程序认识论

计算形而上学的工作对哲学的其他领域有影响，例如认识论。一个明显的例子是，当我们推理中的错误被（计算地）检测到并纠正时，我们的认识论地位就会得到提高。此外，自动推理系统产生的证明可以帮助我们更好地理解复杂的论证，并更快地看到通过引入、删除或公理修改我们的理论的后果——一种“假设分析”。为了说明这一点，为了简化 AOT 的基础，人们可以尝试消除理解原理中的约束，但可以证明这一举动会以一种不平凡的方式导致悖论（Kirchner 2021）。为给定理论找到替代公理集可以帮助减少证明元理论结果（例如合理性）所需的认识论负担。简而言之，“使用计算技术的一大好处是使我们能够准确地看到我们的理论的承诺是什么”（Zalta 2018）。

作为认识论的直接应用，非单调定理证明者可以为“计算实验室”提供基础，在其中探索和实验不同的人工理性模型；定理证明器可用于为人工理性智能体配备推理引擎，以推理并获取有关世界的信息。在这种程序认识论中，理性主体是可废止的（即非单调的），因为新的推理导致接受新的信念，但也导致在新信息存在的情况下撤回先前持有的信念。在任何给定的时间点，智能体持有一组合理的信念，但该组信念可以修改，并且随着进一步推理的进行而处于连续的变化之中。这个模型比所有信念都有保证的模型更好地反映了我们所接受的理性概念，即一旦获得的信念就永远不会收回。实际上，一组有保证的信念可以被视为“在极限内”的合理信念，即主体寻求关于其世界的真实知识的最终认知目标。 （Pollock 1995）提供了以下定义：

一个集合是可废可枚举的，当且仅当存在一个有效的可计算函数 f，使得对于每个 n，f(n) 是一个递归集合并且以下两个条件成立

1.

(\forall x)(x \in A \rightarrow (\exists n)(\forall m \gt n) x \in f(m))2。

(\forall x)(x \not\in A \rightarrow (\exists n)(\forall m \gt n) x \not\in f(m))

为了比较概念，如果 A 是递归可枚举的，则存在一系列递归集 A_i，使得每个 A_i 都是 A 的子集，并且每个 A_i 单调增长，在极限内逼近 A。但如果 A 只能是可枚举的，那么 A_i 仍然在极限内逼近 A，但可能不是 A 的子集，并且会间歇性地从上方和下方逼近 A。 OSCAR 项目（Pollock 1989）的目标是构建一个通用的理性理论，并在基于计算机的人工理性代理中实施它。因此，系统使用可废止的自动推理器，该推理器根据保证信念集应该是可废止可枚举的准则进行操作。 OSCAR 已经酝酿了一段时间，并且自动非单调推理的应用也被用来扩展其能力，以对感知和时间、因果关系和决策理论规划进行可撤销的推理（Pollock 2006）。

4.7 数学

自动推理的主要目标之一是数学的自动化。对此的早期尝试是自动数学（de Bruijn 1968），它是第一个用于检查证明和整本数学书籍的正确性的计算机系统，包括兰道的《Grundlagen der Analysis》（van Benthem Jutting 1977）。自动化已被更现代、更强大的系统所取代，其中最著名的是 Mizar。 Mizar 系统（Trybulec 1979，Muzalewski 1993）基于 Tarski-Grothendieck 集合论，并且像 Automath 一样，由用于编写数学定理及其证明的形式语言组成。一旦用该语言编写了证明，Mizar 就可以自动检查其正确性。 Mizar 证明是正式的，但非常可读，可以引用定义和之前证明的定理，并且一旦经过正式检查，就可以添加到不断增长的 Mizar 数学库 (MML) 中（Bancerek & Rudnicki 2003，Bancerek et al. 2018）。截至 2018 年 6 月，MML 包含约 12,000 个定义和 59,000 个定理。 Mizar 语言是数学文本中使用的标准英语的子集，具有高度结构化，以确保生成严格且语义明确的文本。以下是 Mizar 中存在有理数 x^y 的示例证明，其中 x 和 y 是无理数：

定理T2：

ex x, y st x 是无理数 & y 是无理数 & x.^.y 是有理数

证明

设 w = √2；

H1：根据 INT_2:44,T1，w 是无理数；

w>0 通过 AXIOMS​​:22,SQUARE_1:84;

然后 (w.^.w).^.w = w.^.(w•w) by POWER:38

.= w.^.(w2) by SQUARE_1:58

.= w.^.2 由 SQUARE_1:88

.= w2 功率：53

.= 2 by SQUARE_1:88；

那么 H2: (w.^.w).^.w 根据 RAT_1:8 是有理数；

每箱；

假设 H3：w.^.w 是有理数；

取w，w；

因此论文由H1，H3；

假设H4：w.^.w是无理数；

取 w.^.w, w;

因此论文由H1，H2，H4；

结尾；

Mizar 检查过的证明示例包括 Hahn-Banach 定理、Brouwer 不动点定理、Kőnig 引理、Jordan 曲线定理和哥德尔完备性定理。 Rudnicki (2004) 讨论了形式化维特韦德伯恩定理证明的挑战：每个有限除环都是可交换的。使用 MML 中现有的形式化可以轻松地制定该定理，但证明需要进一步进入库以形式化代数、复数、整数、单位根、分圆多项式和一般多项式的概念和事实。我们花了几个月的时间才向 MML 图书馆提供缺失的材料，但一旦到位，证明就会在几天内正式化并检查正确。显然，形式化数学事实和定义的存储库是更高级应用的先决条件。 QED 宣言（Boyer 等人 1994 年，Wiedijk 2007 年）有这样的目标，并且还有很多工作要做：Mizar 拥有最大的此类存储库，但即使经过 30 年的工作，“相对于已建立的主体而言，它还是微不足道的”。数学”（Rudnicki 2004）。最后一句话应该被理解为呼吁加大对数学自动化这一重要方面的努力。

Mizar 的目标是协助从业者将证明形式化并帮助检查其正确性；其他系统旨在自行寻找证据。几何一直是早期自动校对工作的目标。 Chou (1987) 使用 Wu 方法和 Gröbner 基方法提供的代数方法，通过将假设和结论表示为多项式方程，证明了 500 多个几何定理。 Quaife (1992) 提供了另一项在一阶数学中寻找证明的早期努力：Neumann-Bernays-Gödel 集合论中的 400 多个定理、算术中的 1000 多个定理、欧几里得几何中的许多定理以及哥德尔的不完备性定理。该方法最好被描述为半自动或“交互式”，用户提供大量输入来指导定理证明工作。这并不奇怪，因为当人们将自动推理系统应用到更丰富的数学领域时，这些系统更多地扮演着证明助手的角色，而不是定理证明者的角色。这是因为在更丰富的数学领域中，系统需要对理论和高阶对象进行推理，这通常会让它们更深入地了解不可判定的事物。交互式定理证明可以说是数学中自动推理的“杀手级”应用，并且人们正在花费大量精力来构建功能日益强大的推理系统，这些系统可以充当专业数学家的助手。证明助手 Isabelle/HOL 为用户提供了一个环境，可以在其中进行以结构化但人类可读的高阶逻辑语言表达的证明，并且该环境包含许多可提高用户生产力、自动证明验证和验证的设施。证明任务，并为用户提供了一种模块化的方式来构建和管理理论层次结构（Ballarin 2014）。最近，使用自动和交互式定理证明技术，Quafie 在塔尔斯基几何方面的工作得到了扩展，证明了其他定理（其中一些需要博士级别的证明），包括 Quaife 尚未解决的四个挑战问题，以及从塔斯基公理推导希尔伯特 1899 年的几何公理（Beeson 和 Wos 2017）。