Papers With

← All papers
First page of Simplified proofs of Weak Normalization for propositional logic

Simplified proofs of Weak Normalization for propositional logic

S P Suresh

cs.LO Sep 13, 2026 · v1
formalization logic
Read PDF arXiv abstract Code
TL;DR
Formalizes a new weak normalization proof for intuitionistic natural deduction, including cut definitions, cut-rank, and the one-step reduction function, in Lean.
Abstract
We present a new proof of weak normalization for intuitionistic natural deduction. The distinguishing features of this proof are that it works only with cuts rather than cut segments, provides 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. 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 intuitionistic propositional natural deduction become complicated when disjunction is added, forcing the use of cut-segments and non-obvious choices of which redex to reduce.

Approach

A new proof is given that works only with individual cuts rather than cut-segments, assigning each proof a cut-rank (a pair of naturals under lexicographic order) that decreases under reduction. Explicit local rules determine whether to contract a proof or reduce a chosen subproof, yielding a deterministic one-step reduction function. The entire development, including proofs, cut-rank, contractum, graft, and the reduction relation, is formalized in Lean, with cases elaborated for each explicit cut pattern.

Results

A succinct weak normalization proof and a deterministic normalization algorithm are obtained, fully formalized in Lean, and sketched extensions to classical logic (NK) via reductio ad absurdum and eliminators, and to first-order logic.