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.
Featured Image
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.
Perspectives
Read the Original
This page is a summary of: Strong Normalization for Truth Table Natural Deduction, Fundamenta Informaticae, October 2019, IOS Press,
DOI: 10.3233/fi-2019-1858.
You can read the full text:
Contributors
The following have contributed to this page