Metraipolis › archive › dc_4cd9067340f2

New Proofs of Weak Normalization for Propositional Logic — arXiv:2609.14314

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.14314
License (as archived): CC0-1.0
Archived: 2026-10-16T02:16:06.357Z
SHA-256 of the archived text: d59d01a5fd3a338eaf2f2723a279f5403031a124ffe0d1426c4177162a9e1bbd
Stable URL of this page: https://metraipolis.com/documento/dc_4cd9067340f2

How to cite

New Proofs of Weak Normalization for Propositional Logic — arXiv:2609.14314 — arXiv (en), https://arxiv.org/abs/2609.14314 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_4cd9067340f2 (Metraipolis archive dc_4cd9067340f2, sha256 d59d01a5fd3a338eaf2f2723a279f5403031a124ffe0d1426c4177162a9e1bbd)

BibTeX

@misc{dc4cd9067340f2,
  title = {New Proofs of Weak Normalization for Propositional Logic — arXiv:2609.14314},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.14314},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_4cd9067340f2; sha256 d59d01a5fd3a338eaf2f2723a279f5403031a124ffe0d1426c4177162a9e1bbd},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.14314. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

We present new proofs of weak normalization for intuitionistic and classical propositional logics (with the full set of operators -- falsum, implication, conjunction and disjunction). These proofs work with cuts rather than cut segments, and they provide explicit ``local'' rules for determining whether to contract a whole proof or reduce one of its subproofs, and in the latter case, which subproof to reduce. Interestingly, much of the complication in the case of intuitionistic logic is due to the disjunction elimination rule, while our version of the same rule for classical logic has falsum as conclusion always, and so is much easier to handle. All the complication in the case of classical logic shifts to cuts involving the reductio ad absurdum rule. We also discuss a formalization of the entire proof in Lean, and present a deterministic algorithm for weak normalization.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-09-15 in cs.LO).
Categorie arXiv: Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2609.14314 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-16T01:56:28.444Z dalla pagina https://arxiv.org/catchup/cs.LO/2026-09-15?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).