New Proofs of Weak Normalization for Propositional Logic
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.