A short proof of the Strong Normalization of Classical Natural Deduction with Disjunction

TL;DR

This paper provides a straightforward, elementary proof demonstrating that the cut-elimination process in full classical natural deduction, including all standard logical connectives, always terminates, ensuring strong normalization.

Contribution

It offers a direct, purely arithmetical proof of strong normalization for classical natural deduction with all connectives, simplifying previous complex proofs.

Findings

Proof of strong normalization for classical natural deduction

Elementary and arithmetical approach used

Applicable to full logic with all connectives

Abstract

We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e. in presence of all the usual connectives) classical natural deduction.