Rewriting for Fitch style natural deductions

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

8 Citaten (Scopus)

Samenvatting

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 Curry-Howard 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 typed ¿-terms. Then we define the notion of cut-elimination on Fitch deductions, which is only possible for deductions that are completely unshared (normal forms of the unsharing reduction). For conciseness, we restrict in this paper to the implicational fragment of propositional logic, but we believe that our results extend to full first order predicate logic.
Originele taal-2Engels
TitelRewriting Techniques and Applications (Proceedings 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004)
RedacteurenV. Oostrom, van
Plaats van productieBerlin
UitgeverijSpringer
Pagina's134-154
ISBN van geprinte versie3-540-22153-0
DOI's
StatusGepubliceerd - 2004

Publicatie series

NaamLecture Notes in Computer Science
Volume3091
ISSN van geprinte versie0302-9743

Vingerafdruk

Duik in de onderzoeksthema's van 'Rewriting for Fitch style natural deductions'. Samen vormen ze een unieke vingerafdruk.

Citeer dit