💻 computer science

Inference-Behaviour Semantics for All $^\ast$ Connectives in Two-Dimensional Sequent Calculi

本文通过系统地分析二维序贯演算中的一万多对联结词规则，以识别出 21 种具有意义的联结词，并精确映射它们在各种逻辑系统中的语义相互关系，从而验证了新的推理-行为语义（I-bS）方法，揭示了直觉主义联结词恰好捕捉了其经典对应物一半的含义。

原作者： Sophie Nagler

发布于 2026-07-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Sophie Nagler

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正试图理解一个词真正的含义。你可能会认为这关乎字典里的定义，但一群哲学家和逻辑学家认为，意义实际上在于使用。这就像学习骑自行车：你不会通过阅读手册来理解“骑行”，而是通过如何踩踏、平衡和转向来理解。在形式逻辑的世界里，这些“词”是被称为联结词（如“与”、“或”、“非”）的符号。几十年来，逻辑学家一直试图通过研究规则如何控制它们的使用过程，来弄清楚这些符号的真实含义。这个领域被称为证明论语义学。核心问题在于：如果我们改变了游戏的规则（逻辑），这些词的含义会随之改变吗？还是说，每个联结词都有一个无论在何种语境下都保持不变的核心、不可改变的“灵魂”？

本文使用一种称为**推论行为语义学（Inference-Behaviour Semantics, I-bS）**的新方法，深入探讨了这个问题。你可以把 I-bS 想象成一台高科技扫描仪，它不仅观察纸面上的规则，还观察一个符号在被迫在最精简、最基本的环境中证明自身存在时是如何表现的。作者想知道：如果我们考虑每一种编写逻辑联结词规则的可能性，并在这种极简环境中进行测试，哪些规则实际上拥有独特的、有意义的“指纹”？他们不仅仅是在猜测；他们构建了一个庞大的试验场，以观察哪些规则能够生存，而哪些规则会崩溃。

伟大的联结词普查

作者测试了惊人的数量的可能性：10,816 对不同的规则对。想象一个巨大的网格，每一个方格代表一种使用最多两个起始步骤和两个活性成分来定义逻辑“词”的方式。他们将所有 10,816 个候选者输入到他们的“最小可推导关系”中。你可以将这种关系看作是一个只包含推理最基本要素的微型、空旷的房间：一条规则说“A 是 A”（同一性），另一条规则说“如果你有 A 导致 B，且 B 导致 C，那么你有 A 导致 C”（切断/Cut）。这在逻辑上相当于一套生存主义者的工具包——没有花哨的装饰，没有额外的工具，只有最本质的东西。

目标是观察这 10,816 个候选者中，有哪些能在这种房间里证明自己是“可定义的”。要实现可定义，一个联结词必须通过两项严格测试：

保守性（Conservativity）： 它不能神奇地证明那些在没有它时原本不可能证明的新事物。它必须讲道理。
唯一性（Uniqueness）： 它必须是能做它所做之事的唯一事物。如果另一个符号能做完全相同的工作，那它就不够独特，无法拥有自己特殊的意义。

过滤器：从 10,816 到 21

当尘埃落定时，结果出人意料地精确。在 10,816 个候选者中，只有 376 个通过了第一项测试（保守性）。但当第二项测试（唯一性）应用时，名单进一步缩减。最终，作者发现恰好有 21 个联结词是“最小意义化”的。

这 21 个幸存者是逻辑词的“纯粹”版本。它们包括：

底（Bottom）与顶（Top）： 逻辑上的“假”与“真”。
两种类型的否定： 一种在直觉主义逻辑中表现得像“非”（一种谨慎的否定），另一种在对偶直觉主义逻辑中表现得像“非”（一种更具侵略性的否定）。论文表明，我们在日常数学中使用的“经典”否定实际上是这两种截然不同含义的混合体。
合取（与/Conjunctions）： 有一个“相加式”（additive）版本（类似于标准的“与”）和一个“相乘式”（multiplicative）版本（一种更严格的、消耗资源的“与”）。
析取（或/Disjunctions）： 同样，有一种标准的“或”和一种更严格的“分裂式”（fission）版本。
蕴涵（如果……那么/Implications）： 有右蕴涵和左蕴涵，且各具相加式和相乘式的风味。
逆向与反向（Converses and Inverses）： 论文还发现了这些联结词被翻转或颠倒后的有意义版本。

其他的 10,795 个候选者呢？它们被拒绝了。有些是“冗余联结词”（bloctnectives）——这些规则在纸面上看起来不同，但在行为上与 21 个获胜者完全相同，只是多了一些无用的步骤。其他的则是非保守的（破坏了房间的规则）或非唯一的（与其他符号过于相似，以至于无法拥有独特的身份）。

“半个意义”的发现

关于这些意义在不同逻辑类型之间如何变化的发现，其中之一既有趣又深刻。论文论证了经典逻辑（大多数数学使用的标准逻辑）就像一台将不同成分混合在一起的搅拌机。

例如，在经典逻辑中，我们通常认为“与”只是一个东西。但本文表明，经典“与”实际上是两种截然不同含义的混合：相加式“与”和相乘式“与”。当你切换到直觉主义逻辑（一种用于计算机科学和构造数学的逻辑）时，你会失去相乘式的版本。你只剩下了相加式的版本。

作者得出结论，直觉主义的否定、析取和蕴涵各仅捕捉了其经典对应物一半的意义。这就像经典逻辑说：“我是一个完整的三明治，”而直觉主义逻辑说：“我只是面包，”对偶直觉主义逻辑说：“我只是馅料。”两者都并非“错误”，但它们都只使用了其中的一半成分。

为什么这很重要

这不仅仅是一场符号分类的游戏。该论文验证了一种理解意义的新方式，即推论行为语义学。通过证明这种方法能自然地过滤掉噪音，并留下逻辑学家研究了几十年的这 21 个联结词，作者展示了他们的方法是有效的。这表明，逻辑词的“意义”并不是我们任意发明的；它是通过观察一个词在被剥离到最基本本质时如何表现而发现的。

该论文并不声称解决了逻辑中的每一个谜题。它对于如何处理更复杂的规则或不同的逻辑类型留下了开放性的问题。但对于这 21 个通过测试的联结词，我们现在拥有了一个精确的、独立于规则的意义图谱。我们知道，“与”不仅仅是“与”，而“非”也不仅仅是“非”。它们是复杂且多层面的工具，而这篇论文终于为区分它们提供了蓝图。

技术摘要：二维相继式演算中所有∗联结词的推导行为语义学

1. 问题陈述

本文探讨了证明论语义学（P-tS）中的一个核心挑战：如何在不同的逻辑系统（如经典逻辑、直觉主义逻辑、线性逻辑和对偶直觉主义逻辑）中，为逻辑联结词提供意义不变的语义解释。传统的路径，如模型论语义学（M-tS）和基扩展语义学（B-eS），通常受到“全局主义”的影响，即改变逻辑必然导致联结词含义的改变（例如，经典“与”与直觉主义“与”的区别）。这导致逻辑上的分歧被简化为由于定义不同而导致的单纯的沟通障碍，而非对共享概念的实质性分歧。

本文处理的具体问题是**推导行为语义学（I-bS）**缺乏系统的、形式化的实现。I-bS 是 Nagler [Nag26] 最近提出的一种方法，旨在通过隔离联结词的“最小推导行为”来定义其意义，但该方法此前缺乏对可能联结词规则空间的全面技术评估。本文旨在通过将 I-bS 应用于一组庞大的、无结构的候选联结词集合，来验证 I-bS 的有效性，从而确定哪些联结词拥有独立于特定结构规则（如弱化或收缩）的独特且最小的意义。

2. 研究方法

本研究采用严谨的数据驱动方法，在最小化设置中衡量联结词的“意义”。

2.1 研究对象：所有∗联结词

作者将调查范围定义为所有∗联结词：即在受以下约束的二维相继式演算中可形式化的运算规则对：

运算规则： 必须是独立的、显式的且对称的（定义 3）。
约束条件： 最多有两个前提相继式，且每个规则最多有两个活跃公式。
总空间： 这产生了正好 10,816 个语法上唯一的规则对（前提形状与活跃公式位置的组合）。

2.2 测试环境：最小可推导关系

为了将联结词的意义从特定逻辑的结构特征中分离出来，作者使用了一个由以下部分组成的最小背景演算：

恒等式 ( $Id_{pr}$ )： 仅限于原始公式。
剪切 ( $Cut_{cd}$ )： 一个区分上下文的剪切规则。
结构假设： 该演算假设交换律（多重集），但排除了弱化和收缩。这代表了许多逻辑共有的“亚结构内核”。

2.3 测量装置：推导行为

核心指标是推导行为，定义为当联结词在其可定义性在最小演算中得到证明时所表现出的句法模式。

可定义性标准： 遵循 Belnap [Bel62]，如果添加一个联结词会导致保守扩张（不产生没有该联结词的新定理）且具有唯一性（该联结词在同构意义下是唯一确定的），则称该联结词是可定义的。
语义子句： 联结词的“意义”被识别为其产生最小推导行为剖面的最小运算规则对（即在证明可定义性过程中，联结词及其活跃公式所占据的组成部分位置的最短列表）。

2.4 数据生成与分析

作者系统地过滤了 10,816 个候选者：

过滤器 1（可形式化性）： 所有 10,816 个规则对。
过滤器 2（保守性）： 对正向情况进行剪切消去证明，并为非保守情况构建反例。这使集合减少至 376 个保守联结词。
过滤器 3（唯一性）： 建立水平和垂直的可互推导性。这进一步将集合减少至 150 个唯一可定义的联结词。
最小性分析： 在 150 个可定义联结词中，作者区分了“最小”联结词与“冗余联结词”（具有句法冗余的等价联结词）。通过应用前提类型最小性（前提相继式的最低基数）的标准，作者分离出了真正的最小语义子句。

3. 主要贡献与结果

3.1 识别出 21 个具有最小意义的联结词

主要结果是识别出了正好 21 个具有最小意义的联结词。这些联结词对应于熟悉的逻辑常量及其逆/反向形式，但在加性（格）版本和乘性（群）版本之间有着精确的区别：

零元： 底 ( $\bot$ ) 和顶 ( $\top$ )。
一元： 两种形式的否定（直觉主义 $\neg$ 和对偶直觉主义 $\sim$ ），以及一种“平凡”的反向否定。
二元：
- 合取： 加性 ( $\sqcap$ ) 和乘性 ( $\otimes$ )。
- 析取： 加性 ( $\sqcup$ ) 和乘性 ( $\oplus$ )。
- 蕴含： 加性右蕴含 ( $\rightsquigarrow$ )，乘性右蕴含 ( $\to$ )，加性左蕴含，以及乘性左蕴含。
- 逆与反向： 上述每种都有其对应的逆（交换组件）和反向形式的独特语义子句。

3.2 语义子句与框架

本文为这 21 个联结词提供了显式的语义子句（最小规则对）。至关重要的是，它证明了这些意义是逻辑无关的。例如，乘性合取 ( $\otimes$ ) 的语义子句无论出现在线性逻辑、经典逻辑还是直觉主义逻辑中都是相同的。这些联结词在完整逻辑中的行为差异（例如，经典逻辑中 $\otimes$ 与 $\sqп$ 的等价性）归因于结构资源（如收缩和弱化），而非联结词核心意义的变化。

3.3 跨逻辑的语义相互关系

研究绘制了这 21 个联结词在各种逻辑中的语义兼容性图谱：

经典逻辑 (LK)： 将合取、析取和蕴含的加性版本与乘性版本混淆。它也将两种形式的否定混淆。
直觉主义逻辑 (LJ)： 与合取和析取的加性版本以及“右”蕴含兼容，但仅捕捉到了经典否定的一半意义（具体而言是 $\neg_{min}$ ，排除了 $\sim_{min}$ ）。
对偶直觉主义逻辑 (LDJ)： 捕捉了经典否定的另一半 ( $\sim_{min}$ ) 以及其他联结词的对偶。
线性逻辑 (LL)： 区分所有 21 个联结词，将它们视为语义上不同的个体。

3.4 I-bS 的验证

本文声称通过证明 I-bS 的有效性，其方法在没有针对特定逻辑进行偏见的盲目、穷尽搜索下，自然地收敛于已建立逻辑系统中发现的标准联结词。这种“噪声”（其余 10,795 个规则对）被作为不可定义或非最小而被过滤掉的事实，构成了该理论的一个“合理性检查”。

4. 意义与主张

本文将其发现定位为对 推导行为语义学 框架的验证。其意义在于：

逻辑无关性： 它提供了一种定义在不同逻辑中保持不变的联结词意义的方法。改变逻辑（例如添加弱化）并不会改变联结词的意义；它只是改变了联结词运作的结构语境。
解决意义变化问题： 它为为什么经典逻辑和直觉主义逻辑看似存在分歧提供了语义解释。它们并不一定在“与”或“或”的意义上存在分歧；相反，它们的分歧在于允许哪些最小联结词进行交互，以及允许哪些结构规则。例如，经典“与”是两个截然不同的最小意义（ $\otimes$ 和 $\sqcap$ ）的混淆，而直觉主义“与”则是严格的 $\sqcap$ 。
本体论简约性： 该方法不需要外部模型或基，仅依赖于证明系统的亚结构内核。
穷尽性： 通过覆盖在给定约束下所有可形式化规则的空间，本文声称已提供了二维相继式演算中最小联结词意义的完整分类法。

作者对于研究范围保持谦逊，指出这些结果是相对于特定的约束（两个前提、两个活跃公式、特定的最小演算）而言的，未来的工作可以探索多维演算、量化或替代的最小可推导关系。然而，在定义的范围内，本文断言 I-bS 成功地分离出了逻辑联结词的原始意义。