基于逻辑的类比比例 Logic-based analogical proportions

Logic-based analogical proportions

基于逻辑的类比比例

https://arxiv.org/abs/2406.14402

摘要

作者最近在泛代数 （universal algebra）的一般框架下，提出了一种关于类比比例的抽象代数框架。本文的目的在于将该框架从泛代数提升到表达能力更强的全一阶逻辑 （full first-order logic）的设定中。我们展示了所获得的基于逻辑的框架保留了所有期望的性质，并在该扩展设定下证明了一些新结果。

1. 引言

作者近期在泛代数 的一般设定下引入了一个基于解释的、形式为“a 对 b 就像 c 对 d”——写作 a : b :: c : d ——的类比比例 抽象代数框架（Antić, 2022）。该框架已在 Antić (2023b) 中应用于逻辑程序合成，并在布尔代数（Antić, 2024）和单目代数（monounary algebras）（Antić, 2023a）的背景下进行了研究。

本文的目的是将这一模型从泛代数提升到全一阶逻辑 的设定中，其动机在于某些推理任务必然涉及量词和关系。

切入点是 Antić (2022, §6) 中对类比比例的逻辑解释 。将那种有限的逻辑解释——仅限于表示规则式解释的所谓重写公式（rewrite formulas）——转化为一个完整的、充分发展的类比比例逻辑描述，这一过程被发现并不简单。原因在于，一种天真的扩展很容易导致过度泛化，使得太多元素之间都处于类比比例关系中：

例如，考虑结构 (N, S, 0) ，其中 S 是后继函数；在这个结构中，我们可以将每一个自然数 a 与数符（numeral）ā := Sᵃ0 相对应。给定一些自然数 a, b, c, d ∈ N ，公式：

因此，主要的挑战在于找到一个合适的一阶逻辑片段，用以表达两个给定元素之间的关系。本文通过引入“连通公式 ”（connected formulas）的概念（见 §3）来实现这一点。

从那时起，本文在精神上与 Antić (2022) 相似，但在技术层面上有所不同，因为现在的解释可以包含关系符号以及原子的合取。

在 §4 中，我们证明：本文所扩展的框架保留了 Antić (2022, 定理 28) 中证明的所有期望性质（这些性质基于 Lepage (2003) 的公理化方法），因此在这方面它与原始框架是一致的。此后，一些结果被推广到新的设定中，其中最重要的是第 §5 节中的同构定理 （Isomorphism Theorems）。

在 §6 中，我们展示了一个有趣的新结果，将等式依赖性 （equational dependencies）与类比比例联系起来。需要强调的是，由于之前的框架无法通过重写解释显式地表示方程，这类结果在早期版本的框架中是无法得出的。

在 §7 中，我们重新证明了 Antić (2023a) 中的差异比例定理 （Difference Proportion Theorem），该定理指出：在由自然数和一元后继函数构成的结构 (N, S) 中，我们有：

最初该定理是相对于形式为 s → t 的重写解释进行证明的，其所在的等式片段仅包含形式为 s = t 的解释。

在 §8 中，我们研究了图结构，所使用的路径片段（path fragment）仅包含某种特定形式的路径解释，这些解释编码了路径长度的信息。

2. 预备知识

我们主要按照 Hinman (2005, §2) 的方式来回顾一阶逻辑的语法与语义 。

2.1 语法

一个（一阶）语言 L 包含以下组成部分：

• 一组 L-关系符号 （L-relational symbols），记作 Rsᴸ ；

• 一组 L-函数符号 （L-function symbols），记作 Fsᴸ ；

• 一组 L-常量符号 （L-constant symbols），记作 Csᴸ ；

• 一个函数 r : Fsᴸ ∪ Rsᴸ → N ，用于为每个函数或关系符号指派 元数 （arity）。

其中集合 Rsᴸ、Fsᴸ 和 Csᴸ 是两两不相交的。
Rsᴸ ∪ Fsᴸ ∪ Csᴸ 中的元素被称为语言 L 的非逻辑符号 （non-logical symbols）。

此外，每种语言都包含如下逻辑符号 （logical symbols）：

• 一个可数无限的 变量集 X ；

• 等号符号 = ；

• 联结词： ¬（非）、∨（析取）、∧（合取） ；

• 量词： ∃（存在量词）、∀（全称量词） 。

一个 L-原子项 （L-atomic term）是语言 L 中的一个常量符号或一个变量。

一个 L-项 （L-term）归纳定义如下：

• 每个 L-原子项 都是一个 L-项 ；

• 对于任意函数符号 f 和任意 L-项 t₁, ..., tᵣ₍₎ ，表达式 f t₁ ... tᵣ₍₎ 也是一个 L-项 。

我们用 Xₜ 表示出现在项 t 中的所有变量的集合。
一个项的秩 （rank）由它所包含的变量个数给出。

一个 L-原子公式 （L-atomic formula）具有以下形式之一：

• s = t

  ，其中 s、t 是 L-项 ；

• p t₁ ... tᵣ₍₎

  ，其中 p 是一个 L-关系符号 ，而 t₁, ..., tᵣ₍₎ 是 L-项 。

一个 L-公式 （L-formula）归纳定义如下：

• 每个 L-原子公式 是一个 L-公式 ；

• 如果 α 和 ψ 是 L-公式 ，那么 ¬α、α ∨ ψ、α ∧ ψ 也是 L-公式 ；

• 如果 α 是一个 L-公式 ，且 x ∈ X 是一个变量，那么 (∃x)α 和 (∀x)α 也是 L-公式 。

一个 L-公式 的秩 （rank）是指它的自由变量 （free variables）的数量。
如果一个变量不在任何量词的作用域内，则称为自由变量 。
我们用 Xₐ 表示出现在公式 α 中的所有变量的集合（不一定是自由变量）。

我们假设所有被量化的变量都是不同的，这意味着我们不允许出现如下形式的公式：
(∀x)Px ∧ (∃x)Rx 。

2.2 语义

一个 L-结构 （L-structure）由以下部分组成：

• 一个非空集合 A ，称为 A 的论域 （universe）；

• 对于每个关系符号 p ∈ Rsᴸ ，指定一个关系 pᴬ ⊆ Aʳ⁽ᵖ⁾ ，称为 A 中的 p 的解释 ；

• 对于每个函数符号 f ∈ Fsᴸ ，指定一个函数 fᴬ : Aʳ⁽⁾ → A ，称为 A 中的 f 的解释 ；

• 对于每个常量符号 c ∈ Csᴸ ，指定一个元素 cᴬ ∈ A ，称为 A 中的特殊元素 。

每个项 s 按照通常方式诱导出一个函数 sᴬ : Aʳ⁽ˢ⁾ → A 。

我们归纳地定义逻辑蕴含关系 （logical entailment relation）如下：
对于任意 L-结构 A、L-项 s, t、L-公式 α, ψ ，以及 a ∈ Aʳ⁽α⁾⁻¹ ，我们有：

引理 1 . 同构保持 L-项 和 L-公式 的解释。

3. 类比比例

在本节中，我们将 Antić (2022) 中提出的类比比例的代数框架从泛代数 提升到一阶逻辑 中。
在下文中，设 L 是一个一阶语言，A 和 B 是 L-结构 。

切入点是 Antić (2022, §6) 中关于类比比例的模型论类型 （model-theoretic types）意义上的逻辑解释。

主要难点在于找到一个合适的一阶公式片段，用以表达两个给定元素之间的关系，使得所有相关性质都可以被表达出来，同时排除不合适的元素关系，从而避免出现过度泛化的问题——即太多元素之间被认为处于类比比例关系中（参见 §1 中的讨论）。

本文通过引入“连通公式 ”（connected formula）的概念解决了这一问题：

定义 2 . 一个 2-L-公式 （2-L-formula）是指恰好包含两个自由变量 x 和 y 的公式。

合取 L-公式 （conjunctive L-formula）的集合由不包含否定（¬）或析取（∨）的 L-公式组成。

我们如下定义一个合取的 2-L-公式的无向依赖图 （undirected dependency graph）：

• 其顶点集是由该公式中出现的所有变量组成的集合 Xₐ ；

• 对于两个变量 w, z ∈ Xₐ ，如果它们同时出现在该公式的某个原子公式中，则在它们之间存在一条（无向）边 {w, z} 。

我们称一个合取 L-公式 α 为一个连通 L-公式 （connected L-formula），或简称 c-公式 （c-formula），当且仅当它的依赖图是一个连通图 （connected graph），即：图中任意两个顶点之间都存在路径，并且该图必须包含变量 x 和 y 。

我们将 L 上所有 c-公式 的集合记作 c-Fmᴸ 。

一个 c-项 （c-term）（或 c-原子公式 ，c-atom）是指一个既包含变量 x 又包含变量 y 的 L-项（或 L-原子公式）。

这表明该公式不是一个连通公式 。粗略地说，子公式 w = z 没有包含任何关于 x 和 y 之间关系的信息，因此被认为是冗余的。而简化后的公式 x = y 则显然是一个连通公式。

以下定义——它是对在泛代数框架下给出的一个更受限定义（Antić, 2022, 定义 8）的一种推广——其动机来自于如下观察：形式为 a : b :: c : d 的类比比例最好通过箭头比例 （arrow proportions）a → b : · c → d 来定义，后者形式化了有向关系，并在解释集合上施加了一个极大性条件 （maximality condition）。更确切地说，“a 与 b 的关系正如 c 与 d 的关系”意味着所有形如 α(a, b) 和 α(c, d) 的连通公式 α 所组成的解释集合相对于 d 是极大的，直观上这意味着关系 a → b 与关系 c → d 是最大程度相似 的。

4. 性质

沿袭古希腊的传统，Lepage（2003）在语言学背景下提出了一组性质，作为类比比例形式化模型的指导原则。此后，许多学者对他的列表进行了扩展，目前包含以下性质：

请注意，中心 p-传递性 （central p-transitivity）可由 p-传递性 （p-transitivity）推出。

下面的定理表明，本文所提出的一阶逻辑框架具有与原始泛代数框架相同的性质（参见 Antić, 2022, 定理 28）：

定理 6 . 如定义 4 所定义的类比比例关系满足以下性质：

• p-对称性

  （p-symmetry），

• 内 p-对称性

  （inner p-symmetry），

• 内 p-自反性

  （inner p-reflexivity），

• p-自反性

  （p-reflexivity），

• p-确定性

  （p-determinism）；

而一般来说，它不满足 以下性质：

• 中心置换性

  （central permutation），

• 强内 p-自反性

  （strong inner p-reflexivity），

• 强 p-自反性

  （strong p-reflexivity），

• p-交换性

  （p-commutativity），

• p-传递性

  （p-transitivity），

• 内 p-传递性

  （inner p-transitivity），

• 中心 p-传递性

  （central p-transitivity）。

证明 . 我们有如下证明（其中一些与 Antić (2022) 中定理 28 的原始证明非常相似，为完整起见在此重复给出）：

• 对称性和内对称性 成立是显然的，因为该框架设计之初就旨在满足这些性质。

• 内自反性 成立是因为 x = y 是形如 a → a : · c → c 和 c → c : · a → a 的比例的一个特征解释。

• 接下来我们证明自反性 。我们首先证明：

5. 同构定理

我们有理由期望同构映射 （即结构保持的双射映射）与类比比例是相容的。在本节中，我们将 Antić (2022) 中的第一同构定理 和第二同构定理 提升到本文所讨论的框架中。

6. 等式比例定理

在本节中，我们证明在某些条件下，等式依赖性 （equational dependencies）会导致一个类比比例 （analogical proportion）的成立。也就是说，在某些情况下，如果我们有 t(a, b) = t(c, d) （其中 t 是某个项函数），那么我们期望 a : b :: c : d 成立——请注意，为了使这个等式有意义，t(a, b) 和 t(c, d) 必须属于同一个域。

下一个定理建立了一个使得该蕴含关系成立的情境：

7. 等式片段

在许多情况下，通过对解释 （justifications）进行句法上的限制，来研究完整框架的一个受限片段 （restricted fragment），这是有意义的。在本节中，我们考察仅包含简单形式 s = t （其中 s 和 t 是项）的解释所组成的等式片段（equational fragment），并从这一视角重新证明 Antić (2023a) 中的差异比例定理 （Difference Proportion Theorem）（定理 17）。这为底层框架的稳健性 （robustness）提供了进一步的概念性佐证。

8. 图

一个（无向）图是一个关系结构 G = (Vᴳ, Eᴳ) ，其中：

如果在图 G 中顶点 a 和 b 之间有一条边，我们写作 a —ᴳ b 。

如果一个图 F 满足 Vᶠ ⊆ Vᴳ 且 Eᶠ ⊆ Eᴳ ，则称 F 是 G 的子图。

图中的一条路径 （path）是指连接一系列顶点的有限或无限边序列。

我们写作 a —ⁿᴳ b 表示在图 G 中 a 和 b 之间存在一条长度为 n 的无向路径；
我们写作 *a —ᴳ b 表示存在某个 n ≥ 0 ，使得 a —ⁿᴳ b 成立。

如果一个图中任意两个顶点之间都存在路径，则称该图是连通的 （connected）。

给定一个一阶公式 α ，如果 α 在图 G 中成立，我们写作 G ⊨ α 。

需要指出的是，每一个 路径公式 π(x, y) 在 §3 的意义上都是一个 连通公式 （connected formula），因为它仅包含合取（conjunction），并且变量 x 和 y 是相互连接的，这意味着在 π 的依赖图中，顶点为 x, z₁, ..., zₙ, y ，且对于任意两个变量 v, v′ ，只要在 π 中存在关系 vEv′ ，它们之间就有一条边，从而在 x 和 y 之间存在一条路径。

9. 结论

本文的目的是将一个关于类比比例的抽象代数框架从泛代数 提升到表达能力更强的全一阶逻辑 （full first-order logic）的设定中。这一目标通过将抽象重写扩展为包含任意量词和关系的连通解释 （connected justifications）而得以实现，同时禁止使用析取和否定。

我们已经证明了扩展后的框架保留了所有期望的性质，并展示了全新的等式比例定理 （Equational Proportion Theorem 13），该定理在纯代数设定下是无法证明的。此外，我们还分析了图结构中类比比例的表现。

未来研究的主要方向是进一步将本文的概念和结果从一阶逻辑 提升到二阶逻辑 ，并最终推广至包含量化函数与关系的高阶逻辑 （如 Leivant, 1994 所述）。这是值得追求的方向，因为某些类比比例无法在一阶逻辑中表达。例如，在给定两个由以下方式定义的关系 P 和 R 的结构中：

a → b : · c → d 的所有解释集合是空的，而在二阶逻辑中，该比例包含解释 (∃S) S(x, y) 。也就是说，二阶逻辑和更高阶的逻辑使我们能够发现那些在一阶逻辑中无法被识别的相似性。

原文链接：https://arxiv.org/abs/2406.14402