归谬规则应用的后置与Glivenko定理再探（扩展版）
逻辑
2017-10-26 v2
摘要
本文聚焦于在经典自然演绎中推迟应用归谬规则（raa）的技术。首先，展示了该技术与经典逻辑的两种规范化策略——Prawitz给出的一种和Seldin给出的另一种——之间的联系。其次，提出了Seldin的raa后置策略的一个变体，并探讨了其与Prawitz方法的相似性。特别地，表明如同Prawitz的情况，可以利用Seldin策略的这一变体来诱导从经典逻辑到直觉主义逻辑和极小逻辑的否定翻译，而这无非是Kuroda翻译的一个变体。通过此翻译，证明了直觉主义逻辑和极小逻辑下的Glivenko定理。
引用
@article{arxiv.1710.08854,
title = {Postponement of raa and Glivenko's theorem, revisited (extended version)},
author = {Giulio Guerrieri and Alberto Naibo},
journal= {arXiv preprint arXiv:1710.08854},
year = {2017}
}