Abstract:
Since the 1990s, we have seen how to understand a very wide range of logical
systems (classical logic, intuitionistic logic, dual intuitionistic logic,
relevant logics, linear logic, the Lambek calculus, affine logic, orthologic
and more) by way of the distinction between operational and structural rules.
We can have one set of rules for a connective (say, conjunction, negation, or
the conditional) in a sequent calculus, and get different logical behaviour
depending on the shape of the sequents allowed and the structural rules
governing those sequents.
In this talk, I will consider the relationship between the “big four”
traditional substructural logics—intuitionistic, relevant, affine and
linear—corresponding to the four options for including or excluding the
structural rules of weakening and contraction, in the setting of
Gentzen/Prawitz-style natural deduction proofs for implication and the simply
typed λ calculus. Such a natural deduction setting—in which proofs have any
number of premises and a single conclusion—has a natural bias toward
constructive, or intuitionistic logic.
I will show how the choice of whether to “go classical”, expanding the
structural context to allow for more than one formula in positive position is
orthogonal to the choice of the other structural rules, so that even in the
context of natural deduction proofs, the familiar pair of traditional
implication introduction and elimination rules gives rise to eight different
propositional logics, four of which are “classical” and four of which are
“constructive”. Furthermore, the familiar double-negation translation of
classical logic inside intuitionistic logic generalises to the other three
classical/constructive pairings.
I will explain these results, and, if there is time, I will end the talk with
some reflections on what this might mean for the relationship between classical
and constructive reasoning.
-
The talk is a presentation at the Leeds Logic Seminar.
-
If, for some reason you’d like to see the slides, they’re here.
