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,
ST, TS and more) as consisting of a single broad family of connectives which
are set in different structural contexts given a particular choice of the shape
of sequents, and the structural rules governing those sequents. The sequent
calculus has proved to be a useful lens through which to view a broad range of
logical systems, both in terms of their formal properties, and their
interpretation.
In this talk, I will consider the relationship between the “big
four” traditional substructural logics 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 A 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, and that each of the four constructive substructural logics
have their classical counterpart inside them-not only at the level of
provability, but also at the level of proofs-by way of a natural generalisation
of the double negation translation of classical logic inside intuitionistic
logic. The talk will end (if there is time) with some discussion of the
significance of this result for understanding the classical/constructive
divide.
