Strong normalization results by translation

TL;DR

This paper proves the strong normalization of full classical natural deduction systems by translating them into the simply typed lambda-mu-calculus, extending Mendler's results on recursive equations.

Contribution

It introduces a translation method to establish strong normalization for classical natural deduction, including conjunction, disjunction, and permutative conversions.

Findings

Proves strong normalization for classical natural deduction systems.

Extends Mendler's recursive equations result to this system.

Uses translation into simply typed lambda-mu-calculus.

Abstract

We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system.