Rewriting for Fitch style natural deductions

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationRewriting Techniques and Applications (Proceedings 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004)
EditorsV. Oostrom, van
Place of PublicationBerlin
PublisherSpringer
Pages134-154
ISBN (Print)3-540-22153-0
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
Volume3091
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Rewriting for Fitch style natural deductions'. Together they form a unique fingerprint.

Cite this