Lambek-Grishin 演算：聚焦、显示与全极化

聚焦相继式演算（focused sequent calculi）是相继式演算的一种精炼，其中对推理规则适用性的附加边条件强制实现了一种证明搜索策略。聚焦的无切证明展现出一种特殊的范式，该范式被用于定义相继式演算证明的同一性。我们通过推广多类型演算（multi-type calculi）及其带有异质后承关系（heterogenous consequence relations）的代数语义理论，为 Lambek-Grishin 逻辑引入了一种新颖的聚焦显示演算 fD.LG 和一种全极化代数语义 FP.LG。演算 fD.LG 具有强聚焦（strong focalization），并且相对于 FP.LG 是可靠且完备的（sound and complete）。这一完备性结果在某种意义上强于相对于标准极化代数语义的完备性（例如见 Bastenhof 的 Lambek-Grishin 逻辑相位语义或 Hamano 与 Takemura 的线性逻辑相位语义），因为我们无需对在同一公式上连续应用移位的证明进行商化。我们计划研究该完备性结果与 Abramsky 等人引入的全完备（full completeness）概念之间是否存在联系。我们还展示了一系列附加结果。fD.LG 相对于 LG-代数是可靠且完备的：这相当于对所谓聚焦完备性（completeness of focusing）的一个语义证明，因为 Lambek-Grishin 逻辑的标准（显示）相继式演算相对于 LG-代数是完备的。fD.LG 与 Moortgat 和 Moot 的聚焦演算 f.LG 在证明上等价，事实上存在从 f.LG 推导到 fD.LG 推导的有效翻译以及反之的翻译：这提供了与操作语义的关联，因为每个 f.LG 推导都与一个有向 $\overline\lambda\mu\widetilde{\mu}$-项处于 Curry-Howard 对应中。