面向线性逻辑学者的Girard超越性语法温和导论

Boris Eng

面向线性逻辑学者的Girard超越性语法温和导论

计算机科学中的逻辑 2022-04-06 v5

作者: Boris Eng

摘要

从技术上讲,超越性语法(transcendental syntax)是关于设计具有计算基础的逻辑。它提出了证明论的一个新框架,其中逻辑(证明、公式、真值等)不再是原初的,而计算才是。所有逻辑实体和活动都将表现为对给定计算模型的格式化/结构化,该模型应尽可能通用、简单和自然。超越性语法中选为逻辑基础的是一个我称之为“星状消解(stellar resolution)”的计算模型,它基本上是Robinson一阶子句消解的无逻辑重构,其动力学与瓦片系统相关。超越性语法的初始目标是从这一新框架中重新获得线性逻辑。特别地,该模型自然编码了证明结构中的切消。通过使用让人联想到实现(realisability)理论的“交互式类型化(interactive typing)”思想,可以设计推广线性逻辑连接词的公式/类型。借助交互式类型化,我们能够抵达一个无语义空间,其中正确性准则被视为测试(如单元测试或模型检测)来认证逻辑正确性,从而允许对逻辑实体的有效使用。

关键词

超越性语法线性逻辑证明论星状消解交互式类型化切消

引用

@article{arxiv.2012.04752,
  title  = {A gentle introduction to Girard's Transcendental Syntax for the linear logician},
  author = {Boris Eng},
  journal= {arXiv preprint arXiv:2012.04752},
  year   = {2022}
}

面向线性逻辑学者的Girard超越性语法温和导论

摘要

关键词

引用

相关论文