Rule-Irredundancy and the Sequent Calculus for Core Logic

Notre Dame Journal of Formal Logic 57 (1):105-125 (2016)
  Copy   BIBTEX

Abstract

We explore the consequences, for logical system-building, of taking seriously the aim of having irredundant rules of inference, and a preference for proofs of stronger results over proofs of weaker ones. This leads one to reconsider the structural rules of REFLEXIVITY, THINNING, and CUT. REFLEXIVITY survives in the minimally necessary form $\varphi:\varphi$. Proofs have to get started. CUT is subject to a CUT-elimination theorem, to the effect that one can always make do without applications of CUT. So CUT is redundant, and should not be a rule of the system. CUT-elimination, however, in the context of the usual forms of logical rules, requires the presence, in the system, of THINNING. But THINNING, it turns out, is not really necessary. Provided only that one liberalizes the statement of certain logical rules in an appropriate way, one can make do without CUT or THINNING. From the methodological point of view of this study, the logical rules ought to be framed in this newly liberalized form. These liberalized logical rules determine the system of core logic. Given any intuitionistic Gentzen proof of $\Delta:\varphi$, one can determine from it a Core proof of some subsequent of $\Delta:\varphi$. Given any classical Gentzen proof of $\Delta:\varphi$, one can determine from it a classical Core proof of some subsequent of $\Delta:\varphi$. In both cases the Core proof is of a result at least as strong as that of the Gentzen proof; and the only structural rule used is $\varphi:\varphi$.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

On the role of implication in formal logic.Jonathan P. Seldin - 2000 - Journal of Symbolic Logic 65 (3):1076-1114.
Sequent-systems for modal logic.Kosta Došen - 1985 - Journal of Symbolic Logic 50 (1):149-168.
A minimal classical sequent calculus free of structural rules.Dominic Hughes - 2010 - Annals of Pure and Applied Logic 161 (10):1244-1253.
Cut elimination for a calculus with context-dependent rules.Birgit Elbl - 2001 - Archive for Mathematical Logic 40 (3):167-188.
A Note on Harmony.Nissim Francez & Roy Dyckhoff - 2012 - Journal of Philosophical Logic 41 (3):613-628.
Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.

Analytics

Added to PP
2015-11-25

Downloads
34 (#407,456)

6 months
2 (#670,035)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Neil Tennant
Ohio State University

Citations of this work

Normalizability, cut eliminability and paradox.Neil Tennant - 2016 - Synthese 199 (Suppl 3):597-616.

Add more citations

References found in this work

Cut for core logic.Neil Tennant - 2012 - Review of Symbolic Logic 5 (3):450-479.
Cut for classical core logic.Neil Tennant - 2015 - Review of Symbolic Logic 8 (2):236-256.
Cut as Consequence.Curtis Franks - 2010 - History and Philosophy of Logic 31 (4):349-379.

Add more references