经典逻辑的局部性
逻辑
2009-09-29 v1
摘要
在本文中，我们将在结构演算中看到经典命题逻辑与谓词逻辑的演绎系统。像相继式系统一样，它们具有可容许的切割规则。此外，它们享有自顶向下的对称性以及相继式演算中不具备的某些推导正规形。同一性公理、切割、弱化以及收缩均可归约为原子形式。这导致规则是局部的：它们不要求检查无界大小的表达式。
引用
@article{arxiv.math/0301317,
title = {Locality for Classical Logic},
author = {Kai Bruennler},
journal= {arXiv preprint arXiv:math/0301317},
year = {2009}
}