A note on strong normalization in classical natural deduction

TL;DR

This paper explores how the De Morgan translation in classical natural deduction affects strong normalization, showing that normalization properties can be transferred from disjunction-free systems to full systems through optimized proof translations.

Contribution

It demonstrates that strong normalization in disjunction-free systems can be extended to full systems via the De Morgan translation with an optimized, length-preserving reduction map.

Findings

Reduction sequences in full systems correspond to those in disjunction-free systems.

The De Morgan translation allows transferring strong normalization properties.

An optimized proof map preserves reduction lengths during translation.

Abstract

In the context of natural deduction for propositional classical logic, with classicality given by the inference rule reductio ad absurdum, we investigate the De Morgan translation of disjunction in terms of negation and conjunction. Once the translation is extended to proofs, it obtains a reduction of provability to provability in the disjunction-free subsystem. It is natural to ask whether a reduction is also obtained for, say, strong normalization; that is, whether strong normalization for the disjunction-free system implies the same property for the full system, and whether such lifting of the property can be done along the De Morgan translation. Although natural, these questions are neglected by the literature. We spell out the map of reduction steps induced by the De Morgan translation of proofs. But we need to "optimize" such a map in order to show that a reduction sequence in the full system from a proof determines, in a length-preserving way, a reduction sequence in the disjunction-free system from the De Morgan translation of the proof. In this sense, the above questions have a positive answer.