A General Schema for Bilateral Proof Rules

Journal of Philosophical Logic (3):1-34 (2024)
  Copy   BIBTEX


Bilateral proof systems, which provide rules for both affirming and denying sentences, have been prominent in the development of proof-theoretic semantics for classical logic in recent years. However, such systems provide a substantial amount of freedom in the formulation of the rules, and, as a result, a number of different sets of rules have been put forward as definitive of the meanings of the classical connectives. In this paper, I argue that a single general schema for bilateral proof rules has a reasonable claim to inferentially articulating the core meaning of all of the classical connectives. I propose this schema in the context of a bilateral sequent calculus in which each connective is given exactly two rules: a rule for affirmation and a rule for denial. Positive and negative rules for all of the classical connectives are given by a single rule schema, harmony between these positive and negative rules is established at the schematic level by a pair of elimination theorems, and the truth-conditions for all of the classical connectives are read off at once from the schema itself.

Author's Profile

Ryan Simonelli
University of Chicago


Added to PP

154 (#81,966)

6 months
154 (#23,910)

Historical graph of downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.
How can I increase my downloads?