The Proof-Theoretic Origin of Double Negation Introduction & Elimination
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912599297228800 |
|---|---|
| author | Irani, Khashayar |
| author_facet | Irani, Khashayar |
| contents | This paper investigates the proof-theoretic foundations of double negation introduction (DNI) and double negation elimination (DNE) in classical logic. By examining both sequent calculus and natural deduction, it is shown that these rules originate in reductio ad absurdum. The paper demonstrates that both rules possess harmony, ensuring balance between introduction and elimination, and normalisation, which guarantees that derivations reduce to canonical form without detours. These features reveal double negation not as a redundancy, but as a mechanism of proof-theoretic stability, securing the disciplined integration of RAA into classical logic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_17623 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Proof-Theoretic Origin of Double Negation Introduction & Elimination Irani, Khashayar Logic in Computer Science This paper investigates the proof-theoretic foundations of double negation introduction (DNI) and double negation elimination (DNE) in classical logic. By examining both sequent calculus and natural deduction, it is shown that these rules originate in reductio ad absurdum. The paper demonstrates that both rules possess harmony, ensuring balance between introduction and elimination, and normalisation, which guarantees that derivations reduce to canonical form without detours. These features reveal double negation not as a redundancy, but as a mechanism of proof-theoretic stability, securing the disciplined integration of RAA into classical logic. |
| title | The Proof-Theoretic Origin of Double Negation Introduction & Elimination |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.17623 |