In mathematical practice, there is a bidirectional justification between axioms and theorems: we change the axioms until they become justified by the theorems they prove. Our foundations may change depending on the mathematical objects we want to study. I will be exploring an example of a relevant change of foundations: the passage from classical logic to linear logic, following a recent work by Michael Shulman.
Monoidal closed categories are standard categorical models of NMILL, non-commutative multiplicative intuitionistic linear logic: the monoidal unit and tensor model the multiplicative unit and conjunction; the internal hom models linear implication. In recent years, the weaker notion of (left) skew monoidal closed category has been proposed by Ross Street, where the three structural laws of left and right unitality and associativity are not required to be invertible, they are merely natural transformations with a specific orientation. A question arises naturally: is it possible to find deductive systems which are naturally modelled by skew monoidal closed categories? We answer positively by introducing a cut-free sequent calculus for a skew version of NMILL that serves this purpose. We study the proof-theoretic semantics of the sequent calculus by identifying a calculus of derivations in normal form, obtained from an adaptation of Andreoli's focusing technique to the skew setting. The resulting focused sequent calculus peculiarly employs a system of tags for keeping track of new formulae appearing in the antecedent and appropriately reducing non-deterministic choices in proof search. Focusing solves the coherence problem for skew monoidal closed categories by exhibiting an effective procedure for deciding equality of canonical maps in all models.
This is joint work with Tarmo Uustalu and Niccolò Veltri.
The syntactic calculus of Lambek is a deductive system for the multiplicative fragment of intuitionistic non-commutative linear logic. As a fine-grained calculus of resources, it has many applications, mostly in formal computational investigations of natural languages.
In this talk, I discuss a calculus of βη-long normal forms for terms in the implicational fragment of Lambek calculus and (briefly) its extension with multiplicative conjunction. Reduction to normal form follows the normalization by evaluation (NbE) strategy: (i) evaluate each term as a map in a categorical model; (ii) extract normal forms from the obtained semantic values. The extension with multiplicative conjunction makes things considerably more involved, requiring the presence of a strong monad in the categorical semantics, in analogy with the extension of typed lambda-calculus with sum types.
The reorientation of proof theory towards structural complexity (as opposed to logical complexity) has accelerated considerably in the last 30 years. The proliferation of substructural logics, in particular linear logic, has shed new light on the importance of structural rules such as weakening and contraction, in particular from the point of view of computational interpretations. In the world of pure proof theory, a cornucopia of formalisms have since emerged that place structure at their heart, including hyper- and nested-sequents, deep inference, and more recently cyclic proofs. In some sense this is arguably the natural continuation of Gentzen's original project: to trade off logical complexity in proofs for structural complexity.
In this talk I want to revisit this tradeoff in the setting of deep inference proof theory. Here the logical and structural fragments of systems are completely orthogonal, admitting the localisation of structural rules (including contraction), and the linearisation of logical rules. In fact it becomes meaningful to ask: do we need structure at all to reasonably conduct proof theoretic investigations? To this end, I will survey a line of work that has continued to fascinate me over the last 10 years, namely the theory of 'linear inferences'.
This talk is based on several joint works, involving Cameron Calk, Alex Rice, Lutz Strassburger and Tim Waring.