基于受限初始序列的透明真值系统的切割消除
逻辑
2020-06-30 v2
摘要
本文研究了一组基于初始序列限制的完全去引号真值系统。与众所周知的替代方法不同，此类系统既展现出简单直观的模型论，又具有卓越的证明论性质。我们首先证明，由于真值规则的一种强可逆性，通过标准策略并辅以对推导中公式应用真值规则次数的适当度量，可以在这些系统中消除切割。其次，我们注意到，当向系统添加合适的算术公理时，切割仍然可消除。最后，我们在所考虑系统的无穷公式化表述中的无切割可推导性与不动点语义之间建立了直接联系。值得注意的是，与其他背景逻辑的情况不同，这种联系的建立无需对真值规则的前提施加任何限制。
引用
@article{arxiv.2006.07940,
title = {Cut elimination for systems of transparent truth with restricted initial sequents},
author = {Carlo Nicolai},
journal= {arXiv preprint arXiv:2006.07940},
year = {2020}
}