束蕴涵逻辑的语义分析

我们提出了一种证明逻辑（下称对象逻辑）可靠性与完备性的新方法，该方法绕过模型中的真而直接处理有效性。我们不再使用特定模型中的特定世界，而是在任意模型中使用本征世界（即世界的泛型代表）进行推理。这种推理由一种元逻辑（此处为经典一阶逻辑）的相继式演算所刻画，该演算具有足够的表达能力以刻画对象逻辑的语义。本质上，人们得到了一种关于对象逻辑的有效性演算。该方法通过归约逻辑（而非更为传统的演绎逻辑范式）的视角推进，使用归约空间作为媒介，以证明对象逻辑的相继式演算中的归约与有效性演算中的归约在行为上是等价的。我们没有泛泛地研究该技术，而是以束蕴涵逻辑 为例对其进行说明，因此也处理了 IPL 和 MILL（不含否定）。直观上，BI 是直觉主义命题逻辑与乘法直觉主义线性逻辑的自由组合，这使得其元理论相当复杂。关于 BI 的文献包含许多相似但最终不同的代数结构和满足关系，它们要么仅能刻画该逻辑的片段（尽管是很大的片段），要么对某些连接词具有复杂的子句（例如，用 Beth 的子句代替 Kripke 的子句来处理析取）。正是这种复杂性促使我们使用 BI 作为这种语义方法的案例研究。