Strong Normalization for Truth Table Natural Deduction
Herman Geuvers, Iris van der Giessen, Tonny Hurkens · Fundamenta Informaticae · 2019
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.This yields natural deduction rules for each connective separately.Moreover, these rules adhere to a standard format which gives rise to a general notions of detour and permutation conversion for natural deductions.The aim is to remove all convertibilities and obtain a deduction in normal form.In general, conversion of truth table natural deductions is non-deterministic, which makes it more challenging to study.It has already been shown that this conversion is weakly normalizing.To prove strong normalization, we construct a conversionpreserving translation from deductions to terms in an extension of simply typed lambda calculus