论文标题
吉拉德（Girard）的线性逻辑学家的先验语法的温和介绍
A gentle introduction to Girard's Transcendental Syntax for the linear logician
论文作者
论文摘要
从技术上讲，先验语法是关于用计算基础设计逻辑的。它提出了一个新的证明理论框架，其中逻辑（证明，公式，真理，...）不是原始的，而是计算是原始的。所有逻辑实体和活动都将作为给定的计算模型上的格式/结构呈现，该模型应尽可能一般，简单和自然。先验语法中逻辑的选定基础是我称之为“恒星分辨率”的计算模型，它基本上是对鲁滨逊一阶clausal分辨率的无逻辑重新印象，具有与瓷砖系统相关的动力学。先验语法的初始目标是从这个新框架中检索线性逻辑。特别是，该模型自然地编码了用于证明结构的切割。通过使用“交互式键入”的想法，让人联想到真实性理论，可以设计概括线性逻辑连接剂的公式/类型。多亏了交互式打字，我们才能够到达一个无语言的空间，在该空间中，正确性标准被视为测试（如单位测试或模型检查），以证明逻辑正确性，从而有效地使用逻辑实体。
Technically speaking, the transcendental syntax is about designing logics with a computational foundation. It suggests a new framework for proof theory where logic (proofs, formulas, truth, ...) is no more primitive but computation is. All the logical entities and activities will be presented as formatting/structuring on a given model of computation which should be as general, simple and natural as possible. The selected ground for logic in the transcendental syntax is a model of computation I call "stellar resolution" which is basically a logic-free reformulation of Robinson's first-order clausal resolution with a dynamics related to tile systems. An initial goal of the transcendental syntax is to retrieve linear logic from this new framework. In particular, this model naturally encodes cut-elimination for proof-structures. By using an idea of "interactive typing" reminiscent of realisability theory, it is possible to design formulas/types generalising the connectives of linear logic. Thanks to interactive typing, we are able to reach a semantic-free space where correctness criteria are seen as tests (as in unit testing or model checking) certifying logical correctness, thus allowing an effective use of logical entities.
