双重否定引入与消除的证明论起源
计算机科学中的逻辑
2025-09-23 v1
摘要
本文研究了经典逻辑中双重否定引入（DNI）和双重否定消除（DNE）的证明论基础。通过考察相继式演算和自然演绎，证明了这些规则起源于归谬法（RAA）。本文证明了这两条规则都具有协调性，确保引入与消除之间的平衡，以及正规化，保证推导可归约为典范形式而不走弯路。这些特征表明双重否定并非冗余，而是证明论稳定性的机制，确保 RAA 在经典逻辑中的规范整合。
引用
@article{arxiv.2509.17623,
title = {The Proof-Theoretic Origin of Double Negation Introduction & Elimination},
author = {Khashayar Irani},
journal= {arXiv preprint arXiv:2509.17623},
year = {2025}
}
备注
Draft