Non-finite Axiomatizability of Generalized Medvedev Logics

技术摘要：广义 Medvedev 逻辑的非有限公理化性

1. 问题陈述与动机
本文探讨了由特定克里普克框架构造出的中间逻辑的公理化问题。经典 Medvedev 逻辑 ($\mathbf{Med}$) 由 Medvedev 在 1962 年引入，用于形式化 Kolmogorov 的问题演算，其特征是移除 2-链 ($C(2)^n$) 的有限积中的最大元素所得到的框架类。Maksimova, Skvortsov 和 Shehtman (1979) 的一项开创性结果证明了 $\mathbf{Med}$ 是非有限公理化的。

受此结果启发，Nick Bezhanishvili 猜想，非有限公理化性质不仅限于 2-链，还扩展到了更广泛的框架类。具体而言，他提出：对于任何具有顶元素的非单元素有限根框架 $F$，由其“去顶”积（记作 $F^n$ 去除顶元素）所刻画的逻辑是非有限公理化的。本文研究这些“广义 Medvedev 逻辑” ($\mathbf{TLP}_F$)，旨在确定 $\mathbf{Med}$ 的非有限公理化性是否是此类“去顶”积构造中一种稳健的结构特征。

2. 定义与预备知识
本文在中间逻辑和有限克里普克框架（偏序集）的框架内运行。

• 去顶积 (Topless Products)： 对于具有顶元素 $t$ 的有限根框架 $F$，$n$-次积 $F^n$ 是按坐标定义的。去顶框架 $F^n-$ 是通过从 $F^n$ 中移除最大元素 $(t, \dots, t)$ 得到的。
• 广义 Medvedev 逻辑 ($\mathbf{TLP}_F$)： 定义为所有此类去顶积逻辑的交集：$\mathbf{TLP}_F = \bigcap_{n \in \omega} \text{Log}(F^n-)$。
• 预顶积逻辑 ($\mathbf{P}_F$)： 由全积 $F^n$（移除顶元素之前）所刻画的逻辑。

3. 研究方法
作者采用了克里普克框架的结构分析，特别关注 p-态射（有界态射）和 Jankov-de Jongh 公式。核心方法包括：

1. 刻画预顶逻辑： 证明对于任何具有顶元素的非单元素有限根框架，其有限积的逻辑恰好是弱排中律逻辑 ($\mathbf{KC}$)。
2. 构造反例模型： 利用“灯笼架”框架 ($L_{s,n}$ 及其变体 $L'_{s,n,m}$) 来检测逻辑之间的间隙。这些框架经过特殊构造，具有特定的分支度（branching degree）和深度，从而违反了去顶积所施加的约束。
3. 分支度分析： 建立一个界限，该界限规定了能够作为去顶积的生成子框架的 p-态射像的框架的分支度。该界限取决于框架的深度以及生成框架 $F$ 的最大分支度。
4. 与 $\mathbf{Cheq}$ 的比较： 通过分析广义 Medvedev 逻辑与棋盘集逻辑 ($\mathbf{Cheq}$) 之间的关系来扩展 Fontaine 的研究结果，利用“蝴蝶结引理”(Bowtie Lemma) 表明灯笼架是 $\mathbf{Cheq}$-框架。

4. 主要贡献与结果

• 刻画 $\mathbf{P}_F$： 本文证明，对于任何具有顶元素的非单元素有限根框架 $F$，其有限积所刻画的逻辑是 $\mathbf{KC}$（定理 3.3）。这证实了移除顶元素是产生 Medvedev 式逻辑复杂行为的关键操作。
• 证实 Bezhanishvili 的猜想： 主要结果（定理 4.8）证明，对于任何具有顶元素的非单元素有限根框架 $F$，广义 Medvedev 逻辑 $\mathbf{TLP}_F$ 是非有限公理化的。这同时解决了 Bezhanishvili 的两个猜想：
  • 该性质对任意有限链成立（定理 4.1 和推论 4.2）。
  • 该性质对任意具有顶元素的非单元素有限根框架成立（定理 4.8）。
• 与 $\mathbf{Med}$ 的关系： 本文确立了经典 Medvedev 逻辑是最大的广义 Medvedev 逻辑（引理 3.4）。此外，如果 $F$ 是一个非平凡的有限分配格，则 $\mathbf{TLP}_F$ 正好是 $\mathbf{Med}$（定理 4.1）。
• 在 $\mathbf{Cheq}$ 之上的非有限公理化性： 本文扩展了 Fontaine 的定理，证明如果 $\mathbf{Cheq}$ 是一个广义 Medvedev 逻辑 $\mathbf{TLP}_F$ 的真子逻辑，那么 $\mathbf{TLP}_F$ 在 $\mathbf{Cheq}$ 之上是非有限公理化的（定理 5.3）。这依赖于灯笼架是 $\mathbf{Cheq}$-框架这一事实。
• 序结构： 本文研究了这些逻辑的格结构：
  • 至少存在可数个两两不同的广义 Medvedev 逻辑（定理 5.4）。
  • 不存在最小的广义 Medvedev 逻辑（定理 5.5）。所有此类逻辑的交集本身并不是一个广义 Medvedev 逻辑（推论 5.6）。

5. 意义
本文声称解决了这样一个问题：即 Medvedev 逻辑的非有限公理化性是一个孤立现象，还是去顶积构造的一个普遍属性。通过证明每一个广义 Medvedev 逻辑（源自具有顶元素的非单元素有限根框架）都是非有限公理化的，这项工作阐明了由这些结构操作生成的中间逻辑的行为。它表明，阻碍有限公理化的复杂性本质上源于积框架的“去顶”特性，而与基框架 $F$ 特定的分支结构无关。此外，这些结果在中间逻辑的格中提供了这些逻辑更精细的“地理分布”，显示它们形成了位于 $\mathbf{KC}$ 与 $\mathbf{IPC}$ 之间、具有丰富且严格下降性质的无限链，且没有最小元素。