证明背后的若干组合结构
逻辑
2016-09-06 v1
摘要
我们试图揭示逻辑中形式证明底下的一些组合结构。为此我们研究 Craig 插值定理,它实质上是关于形式推导结构的一个命题。我们展示插值定理可推广到关于集合的更朴素结构上,并进而说明如何通过恰当解释集合论语言来得到该命题的经典与直觉主义版本。我们给出的定理是这一著名逻辑命题的几何表述,并给出了组合性系统满足插值性质的充分条件。其对象可以是图,也可以是公式或曲面。我们所用的组合映射在逻辑语言中解释时对应于“逻辑流图”的概念(即追踪证明中公式出现流向的图;此概念由 (Buss, 1991) 引入)。利用出现流向来研究证明结构的想法已见于 (Girard, 1987) 的“证明网”概念。
引用
@article{arxiv.math/9604207,
title = {Some Combinatorics behind Proofs},
author = {Alessandra Carbone},
journal= {arXiv preprint arXiv:math/9604207},
year = {2016}
}