Abstract:
Graham Priest’s simple three-valued logic LP has many curious properties. It
has the same valid formulas as classical logic, but differs from classical
logic when it comes to valid sequents. The valid sequents do not uniquely
characterise the logic: it is possible to have more than one different
LP-“negation”, each of which satisfies all the LP-requirements, without being
equivalent. (The situation is not unlike modal operators in your favoured modal
logic. A modal logic like S5 does not uniquely determine the meaning of the
modal operators. The same goes for LP when characterised in terms of its
consequence relation.) One consequence of this fact is that extant proof-first
characterisations of LP are unwieldy. In some systems, connectives are given
rules featuring negation and rules without; in others, formulas occur
positively or negatively signed, and in others, sequents have three positions
in which formulas can occur instead of two. This makes relating LP to familiar
logics on a proof-first basis difficult.
The simple three-valued logic ST (strict-tolerant logic) also has many curious
properties. It has the same valid formulas and valid sequents as classical
logic, but differs from classical logic at the level of meta-inferential
validity (rules obtaining between sequents). In ST, the Cut rule is not
generally valid: from A ⇒ B and B ⇒ C, it need not follow that A ⇒ C.
Understanding the distinctive behaviour of ST on an inferential level involves
considering not only valid formulas and valid inferences but also valid
meta-inferences. However, keeping track of this ever-growing tower of
consequence relations is also difficult.
In this talk, I aim to address both
of these issues in one go. I will exploit the relationship between LP and ST,
and some prior work on mildly bilateral treatments of natural deduction to
provide a novel natural deduction proof system for both LP and ST that has the
following features:
- Each connective rule is a standard natural deduction rule, familiar from Gentzen.
- Each connective is uniquely characterised by rules governing it.
- The difference between LP and ST on the one hand, and classical logic on the other, is the addition of a purely structural rule.
- The relationship between the valid formulas, the valid sequents, and the valid meta-sequents in each of the logics in question (LP, ST and classical logic) is uniquely and systematically determined by the rules governing the construction of proofs in the underlying calculus.
The aim of this exercise is not is to not only get a better understanding the
breadth of the range of options for inferential presentations of logic LP and
ST, but to also deepen our understanding of the relationship between natural
deduction and the sequent calculus (and meta-inferential relations above the
level of the sequent), and the distinctive role of structural rules from each
of these perspectives.
