Papers With

← All papers
First page of New Proofs of Weak Normalization for Propositional Logic

New Proofs of Weak Normalization for Propositional Logic

S P Suresh

cs.LO Sep 13, 2026 · v3
formalization logic
Read PDF arXiv abstract Code
TL;DR
Formalizes all definitions and proofs of weak normalization for intuitionistic propositional natural deduction in Lean, with a public code repository.
Abstract
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.
Problem

Standard proofs of weak normalization for propositional natural deduction with disjunction work with cut segments and lack explicit local rules for choosing which subproof to reduce. A simpler, more teachable proof is sought for intuitionistic and classical propositional logic with falsum, implication, conjunction and disjunction.

Approach

Each proof is assigned a cut-rank, a pair of natural numbers ordered lexicographically, built from the degrees and weights of its cuts. Explicit local rules decide whether to contract the whole proof or reduce a chosen subproof, and each step is shown to decrease the cut-rank. Classical logic is handled with a reductio ad absurdum rule and eliminators. The definitions and proofs are formalized in Lean, and a deterministic one-step reduction function is derived.

Results

New proofs of weak normalization are given that work with cuts rather than cut segments. All definitions and proofs of the intuitionistic case are machine-checked in Lean. A deterministic normalization algorithm is presented, and the extension to classical logic is sketched.