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...

• Type: Conference
• Year: 2004
• Where: RTA
• Authors: Herman Geuvers, Rob Nederpelt
• Keywords: Fitch Deductions, Fitch Style, Natural Deductions, RTA 2004, Theoretical Computer Science