Rewriting for Fitch Style Natural Deductions

9 years 18 days ago
Rewriting for Fitch Style Natural Deductions
Logical systems in natural deduction style are usually presented in the Gentzen style. A different definition of natural deduction, that corresponds more closely to proofs in ordinary mathematical practice, is given in [Fitch 1952]. We define precisely a CurryHoward interpretation that maps Fitch style deductions to simply typed terms, and we analyze why it is not an isomorphism. We then describe three reduction relations on Fitch style natural deductions: one that removes garbage (subproofs that are not needed for the conclusion), one that removes repeats and one that unshares shared subproofs. We also define an equivalence relation that allows to interchange independent steps. We prove that two Fitch deductions are mapped to the same λ-term if and only if they are equal via the congruence closure of the aforementioned relations (the reduction relations plus the equivalence relation). This gives a Curry-Howard isomorphism between equivalence classes of Fitch deductions and simply...
Herman Geuvers, Rob Nederpelt
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where RTA
Authors Herman Geuvers, Rob Nederpelt
Comments (0)