Strong Normalization for Truth Table Natural Deduction
What is it about?
We present a proof of strong normalization of proof-reduction in a general system of natural deduction called truth table natural deduction. In previous work, we have defined truth table natural deduction, which is a method for deriving intuitionistic derivation rules for a connective from its truth table. To prove strong normalization, we construct a conversion preserving translation from deductions to terms in an extension of simply typed lambda calculus, which we call parallel simply typed lambda calculus. This makes it possible to get a grip on the non-deterministic character of conversion in the intuitionistic truth table natural deduction system.
Why is it important?
This work gives a good insight in the nature of proof-reduction for a general framework of natural deduction. In addition, it gives a technical tool for difficult strong normalization proofs.