bibkey: schroederheister2024proofsemantics
authors: Peter Schroeder-Heister
year: 2024
title: Proof-Theoretic Semantics — An Autobiographical Survey
doi: 10.1007/978-3-031-50981-0_1
claim: Proof-theoretic accounts of meaning depend on the treatment of hypotheses, admissible atomic bases, and proof identity; the survey distinguishes extensional harmony from intensional questions and reports limits of a completeness program.
strata_touched:
  - D5/S0/Diagonal/Lawvere/TheoryIsConsequenceFixedPoint
  - D5/S3/ConceptDynamics/Observation/StrictOneHoleContexts
  - D5/S3/Observer/Separation/CongruenceClosureDuality
  - D5/S3/ConceptDynamics/DefinitionEscapeLaws/StrictKernelNoveltyCriterion
  - D5/S3/ConceptDynamics/DefinitionEscape/BlindKernelReductionMeasure
  - D5/S0/Rewriting/NormalizationSystem
  - D5/S3/ConceptDynamics/TransportValidity/OldLanguageValidityConservativity
license: citation-only
triage: anchor

证明论语义：规则的正当性、假设与证明同一性

这份文献注以 Schroeder-Heister 的综述为主线，结合其原始研究章节和 Stanford Encyclopedia of Philosophy 条目，整理逻辑规则如何获得意义与 正当性的不同研究问题。下文引用的是已有文献结果；研究建议不构成新定理， 也不宣称已经完成相应的逻辑演算形式化。

1. 所要解释的必然性

证明论语义尝试通过证明、推理以及证明之间的变换说明逻辑表达式的意义。 它的基础问题包括：怎样算理解一个连接词，怎样区分合理的推理规则和 仅仅被宣布为合法的规则，以及哪些推理规则能够由已经认可的规则得到辩护。 这种研究不能仅用“给定一组规则，其闭包形成一个理论”来回答；闭包结构 已经预设了后承关系，需要辩护的是后承关系本身的构成。

以合取为例，引入规则允许从 A 和 B 得到 A∧B，消去规则允许从 A∧B 取得 A 或 B。如果先引入合取再立即消去，相应证明可约化为原先的证明。 这一机制解释消去步骤为什么没有从该引入步骤取得额外信息。 Gentzen 的引入规则优先思想与 Prawitz 的反演原则是这一研究的经典起点 [2, §2.2.1]。这里的“辩护”不等于从引入规则单独形式演绎出消去规则。

Prior 的 tonk 是最小的警戒例子：若同时规定

$$\frac{A}{A\mathrm{tonk}B},\frac{A\mathrm{tonk}B}{B},$$

则任意 A 都能推出任意 B。这个例子排除的是“任意一组宣布为定义的规则 都可以赋予连接词合理意义”的主张，不能据此否定一切通过规则说明意义的方案 [2, §2.2.1；3, §6.2]。

2. 必须分别提出的四个要求

“和谐”在文献中有多种定义；表中列的是需要分别说明的要求， 不主张这些定义之间不存在定理性的蕴涵关系。提出蕴涵时必须固定演算、 结构规则、约化方式及和谐定义 [2, §§2.2.1、3.7–3.10；3, §6.2]。

全局正规化还须区分弱正规化（每个证明存在到达正规形的约化序列）与 强正规化（不存在无限约化序列）。存在局部约化规则本身不证明其中任何一项。 SEP 用朴素集合论理解规则及 Russell 悖论讨论局部反演与全局正规化的区别；相应的局部反演 并未排除不可正规化的悖论证明 [2, §3.8]。这不是对某个已经证明强正规化 的演算给出反例。

3. 假设并非已被解释完毕的背景

Schroeder-Heister 区分“假设是等待闭证明填入的空位”的占位观点， 以及把假设判断本身放在基础地位的其他方案。占位观点下，开放证明的正当性 可以通过代入适当的闭证明来考察；代入、解除假设和引入假设是关键操作。 这是一种可研究的语义立场，并非所有推理概念无须讨论的唯一解释 [4, §2；2, §3.6]。

还须说明哪些结构操作被允许：前提能否复制、丢弃、交换次序，以及 不同位置出现的同一个前提是否可被识别为一次使用。把上下文处理成集合 已经忘掉了使用次数和顺序。讨论相关逻辑、线性逻辑或其他次结构逻辑时， 不能先抹去这些区别，再声称得到普遍的推理理论 [2, §3.10]。

这一问题比“某个例子里信息是否丢失”更基础：推理所作用的对象以及 允许的操作本身需要确定。固定这些操作之后，形式定理可以给出条件明确的 必然关系；这一事实尚不替我们选择这些操作。

4. 原子基础及其扩充决定怎样的有效性

证明论语义中的原子基础可以是原子公理、生产规则、能解除假设的原子规则、 更高阶规则，或带有定义反思的系统。仅比较已经生成哪些原子命题会漏掉 这些规则结构的区别。选择哪些原子系统以及怎样允许扩充，是该语义的 实质组成部分 [1, §10；2, §2.6]。

在 SEP 讨论的一类基扩充语义中，蕴涵的有效性需对允许的基础扩充量化。 仅考察当前基础内有没有闭证明，会遇到前件没有证明时的空泛成立问题。 哪些扩充进入量化范围直接影响这种有效性 [2, §2.7]。

这也是完备性问题的关键背景。Piecha 与 Schroeder-Heister 的结果表明， 他们研究的证明论语义不能给出直觉主义命题逻辑的所求完备性。 SEP 的相应说明涉及 Harrop 规则：它在该语义下有效，却在直觉主义命题逻辑中 仅可容许而不可导出 [2, §2.8；1, §10]。可容许性是“定理前提经该规则仍得到 定理”，可导出性要求在演算中有从相应开放前提到结论的推导；两者不能混用。

这一结果不意味着所有证明论语义都不完备，也不意味着直觉主义逻辑 不一致。采用不同的基础、扩充关系或析取语义，有不同的完备性研究， 包括 Sandqvist 的方案 [2, §2.8；1, §6]。因此不能把某一方案下的反例 升级为整个领域的不可能性定理。

5. 互相可推不等于证明结构相同

原始章节给出一个更精细的区分 [4, §3.3]：

$$A\wedge B\text{与}A\wedge (A\to B)$$

在普通直觉主义命题逻辑中可以互相推出，但在保留证明结构的相应解释下， 互相可推不能保证同构。以类型解释说明其机制：

$$f:A\times B⟶A\times (A\to B),f(a,b)=(a,\lambda x.b),$$

$$g:A\times (A\to B)⟶A\times B,g(a,h)=(a,h(a)).$$

有 g∘f=id，但 f∘g 把任意函数 h 替换成常函数 λx.h(a)。 它保存了当前输入 a 上的值，却丢掉了函数在其他输入处的行为。

取 A=B=Bool，在普通有限类型语义下，两个类型的基数分别是 4 与 8， 因而不存在两者之间的双射。这一有限实例说明一般互推不能保证同构； 它不声称每一对具体 A、B 都不可能同构，也不把有限类型模型直接等同于 所有形式演算中的证明等同性。

研究证明同一性，需要选定哪些约化、展开或其他等式识别两个证明。 Schroeder-Heister 特别指出：即使明确采用同构，怎样用它定义足够的 内涵和谐仍须进一步论证，不能把某个二阶翻译的同构当成自动成功的定义 [4, §§3.3–3.4]。

Lean 的 Prop 采用证明无关性。同一命题的两份证明在该层被识别， 因此不能仅凭 Prop 中的互推来建模上述全部证明结构区别。 相应研究可采用显式推导语法及约化商，或使用保留构造信息的 Type 与范畴模型。 类型层的有限实例与命题层的逻辑等价应分别说明。

6. 与已有库及 Fibonacci 研究的关系

TheoryIsConsequenceFixedPoint 以给定的后承闭包为前提；它研究该闭包的 不动点结构，没有替我们确定或辩护后承规则。 NormalizationSystem 把终止性与局部汇合作为系统的字段；它提供这些条件 之下的正规形与唯一性结构，没有证明任意逻辑规则系统满足这些条件。 OldLanguageValidityConservativity 处理其指定语言与模型输运条件下的 旧语言有效性；它与本注的逻辑扩充问题相邻，但不是任意新规则准入的证明。 这些是源码范围的说明；本注不交付对这些模块的新形式化应用。

Fibonacci 及其教师、分类研究可以作为表达选择与规则输运的具体对象。 从一个对象的递推、分类或读取规律，尚不能直接得到逻辑连接词或结构规则的 唯一正当性。建立联系时，应逐一给出对象、判断、操作及证明变换的对应， 再问对应是否保存和反映所研究的证明结构。这是研究接口，不能以共同的 “生成”“关系”“不动点”术语替代。

7. 可推进的研究靶与哲学边界

一个具体的候选研究靶是保留证明同一性的保守扩充。 固定一个明确的演算、前提资源结构及证明等同性，比较加入原子规则或 定义反思规则前后的证明范畴。旧语言嵌入不仅要保留可证性，还要检验：

1. 新演算中旧对象之间的证明是否都能回译成旧证明；
2. 两份原先不同的旧证明是否被新等式合并；
3. 回译与重新嵌入在指定证明等同性下是否具有所需的往返性质。

在适合这一解释的范畴表示下，前两项对应满性与忠实性。 这只是明确研究标准，不是新增的满忠实定理。实际目标须寻找关于规则形状、 递归依赖和结构操作的可核查条件，证明它们如何保证上述性质；不能把 “嵌入满忠实”作为假设，再把同义结论包装成新成果。

这条路线有两类可证伪成果：一类给出同一资源条件下的安全扩充标准， 另一类构造可证结论不变而证明结构改变的规则扩充。 在实施前还须检索类型理论中的定义扩充、范畴证明论、逻辑框架及相关 保守性研究。[1] 还直接指向 Pistone 与 Tranchini 的 Intensional harmony as isomorphism；这一线索须核对原文后再用于确定实际缺口。这里未完成这些路线的原创性尽调，也未将候选研究靶认定为 已发表而未解决的具名开放问题。

这些文献支持一项方法判断：研究逻辑必然性时，须把假设的地位、允许的 变换以及同一性标准列为需要解释的对象。这项判断不等于证明哲学全部是 逻辑，不等于证明世界只有一种本体，也不等于说明任意规则同样好。 不同规则仍可依据协调性、保守性、正规化、表达能力及证明行为接受严格比较。

8. 与区分、逃逸及上下文同余的具体联系

本库已经有“定义—共同核—语义闭包—逃逸”与上下文同余的结构。 以下对应复用这些结构，用于定位证明论语义所需的接口；不把对应本身 计作新增定理，也不把认证 DAG 的路径直接当作逻辑证明项。

8.1 先指定要区分的是结论、证明还是证明行为

取 X 为某个固定判断的推导项，或者以带类型标签的并集保存不同判断的推导项。 单看结论的读数 q 会合并证明同一个结论的推导。目标 T 可以是固定等同性 下的证明类，也可以是允许的上下文中的行为。后者未必区分所有不同证明类， 二者必须分别说明。对象处于 Lean 的 Prop 层时，证明无关性也不能被忘记。

本库的目标残差是

$$E(q;T)=\{(x,y):q(x)=q(y),T(x)\ne T(y)\}.$$

它精确定位“结论读数相同，但所研究的证明区别仍不同”的对象对。 这个对应只有在选定实际推导语法、类型约束和目标等同性后，才成为某个 演算的具体模型。仅给 q、T 起证明论名字尚未完成该接口。

§5 的函数机制可作已核验的类型层实例。令 X=Bool→Bool， q(f)=f(true)，T(f)=f(false)。常假函数与 Boolean 否定函数有相同 q， 却有不同 T。现有 not_mem_semanticClosure_iff_kernel_witness 因而判定 T 不在单读数族 {q} 的语义闭包中；补入 T 会严格缩小共同核， 使用的正是现有 strict_kernel_novelty_criterion。 这说明“只保留一个输入上的结果”与“保留方法在其他输入处的行为”的区别。 有限实例不等于对任意演算证明等同性的完整模型。

8.2 连接逻辑替换的关键是上下文稳定性

如果两个推导被认为相同，把它们放进允许的推理上下文后， 应当得到哪些相同的结果，还须另作约定与证明。 只比较当前结论，可能漏掉上下文能显露的区别；只要求当前读数相同， 也不保证操作能够在相应商上良定义。

本库 StrictOneHoleContexts 固定有限元确定性部分操作， 把合法单孔上下文实际解释为 X→Option X，并分别观察失败与成功。 其 contextual_equivalence_is_greatest 给出： 所有这些上下文观察的共同核，是原读数核内部最大的强同余。 这里“强”还要求等同输入保持操作定义域，并保持定义结果的等同。 这比对每个对象单独读取一次提出了更强的替换要求。

signature_extension_refines 进一步给出：在同一对象载体、同一读数下， 保留全部旧操作及其定义域的签名扩充，只会缩小上下文等同关系。 这可以用于研究新增操作显露旧区别的情形；它不自动适用于添加新推导对象、 添加证明等式或改变判断类型的扩充。

因此与证明论语义相接的真实义务是：把类型正确的证明组合、替换、 解除假设与约化接入上述部分操作框架，证明合法性与失败标签对应准确， 再核对所选证明等同性是否具有所需的强同余性质。 尚未完成的是这个演算接口，而非重新证明已有的上下文最大性。 上下文不可区分也不能未经论证就等同于指定的 βη 证明等同性。

8.3 两种同余修复的方向相反

本库 CongruenceClosureDuality 对固定单步操作 F 与等同关系 R 给出两种修复：

$$I_F(R)\subseteq R\subseteq C_F(R).$$

I_F(R) 是 R 内最大的前向稳定等同关系，去掉那些会被后续操作分开的 错误等同；C_F(R) 是包含 R 的最小前向同余，增加等同，使现有认同 在操作下保持一致。两者有同一类前向同余作为不动点，且形成相应伴随关系。

前一种修复保留更多可区分性，后一种修复接受更多识别。 它们给证明同一性研究提供两条方向不同的路线；上述单步定理本身未把 多元、依类型变化的推理系统建模完毕。特别地，不能仅从“商上的操作终于 良定义”推出“旧证明的区别被保留”。

8.4 逃逸率必须守住比较对象与目标

至少须区分三种量：

对于目标逃逸谱，还须固定测量的是全部源对象对、基线残差对，还是 某种抽样/使用分布。对 X=Bool→Bool 的上述实例，16 个有序源对象对中， E(q;T) 有 4 个；以全部对象对为分母得到 1/4。 以基线 E 为正质量归一化时，未补充前的相对残差为 1。 它们使用不同分母，不能作为两个相互冲突的逃逸率读数。

一个直接反例守住目标变化的边界：保持 q 不变，仅把目标从 T 改成 q， 则 E(q;q)=∅，而 E(q;T) 仍非空。残差归零没有恢复 T；它改变了需要保留的区别。 若某条旧证明区别被新增等式识别，其目标证明类已经变化，亦须重新检查 比较是否仍针对同一个目标。只有经已证映射保持目标与相关操作，才可作 相应输运比较。零基线质量也不满足正质量归一化公式的前提。

固定目标之后，增加区分能力会缩小残差；正残差质量可以见证确有缺口。 但任意非负权重可能忽略某些对象对，不能从零质量反推残差集合为空。 从“新增区别”推出“严格正的质量收益”，须说明新分离的目标相关对象对 具有正质量。本库 blind_kernel_reduction_measure 只从正缩减质量推出 存在分离见证，没有无条件的反向保证。 预算谱的下确界为零也不保证某个有限预算真的取得零残差；DESC 的有限闭合、 渐近闭合和盲核边界需要各自条件，不能混作一次有限认证。

8.5 对下一研究靶的修正

这里已有的库内容使 §7 的研究靶更具体：分别检查 新增区分、上下文操作、证明等式三个方面。 观察细化不自动提供合法的证明替换；操作稳定不自动保留全部证明区别； 可证结论不变也不自动保证上述两项。

应在一个明确演算中建立类型正确的上下文接口，检验候选扩充究竟是在 提供新区分、加入测试旧区别的操作，还是增加新的证明识别。 随后比较同一目标下的区分关系与所需证明输运，再在固定测度和成本下 讨论逃逸谱。可复用的数学内容应来自这个接口中真实缺少的条件或反例， 而不是给共同核、残差与同余最大性再命名。

这一联系支持的哲学判断是：讨论“相同”“必然”或“理解”时，除了当前 结论，还应解释允许哪些替换与变换，以及什么区别必须在这些变换下保持。 这是结合文献与仓内结构的研究建议；它未证明意义等同于某个逃逸率标量， 也未证明一个观察框架已经选择了唯一正确的逻辑。

来源与定位

1. Peter Schroeder-Heister, Proof-Theoretic Semantics: An Autobiographical Survey, 2024, §§6、10，特别是 pp. 26–28。 DOI。 开放章节。
2. Peter Schroeder-Heister, Proof-Theoretic Semantics, Stanford Encyclopedia of Philosophy，首次发表 2012，实质修订版本 2023-08-18。 正文。
3. John MacFarlane, Logical Constants, Stanford Encyclopedia of Philosophy，§§6.1–6.2。 正文。
4. Peter Schroeder-Heister, Open Problems in Proof-Theoretic Semantics, Advances in Proof-Theoretic Semantics, 2016, pp. 253–283，§§2、3.3–3.4。 DOI。 开放章节。

[2] 与 [1] 指向 Piecha 与 Schroeder-Heister 的 Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-Theoretic Semantics, 2019， DOI。 本注关于该结果的报告依据 [1] 与 [2]，不声称已经逐步核对该论文的完整证明。