Contributed Talks 11
Chair: Alexis Saurin
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
17:30 
Lutz Straßburger, Lambek Calculus with Banged Atoms for Parasitic Gaps 
Authors: Mehrnoosh Sadrzadeh and Lutz Straßburger Lambek Calculus is a noncommutative substructural logic for formalising linguistic constructions [1]. However, its domain of applicability is limited to constructions with local dependencies [2]. We propose here a simple extension that allows us to formalise a range of relativised constructions with long distance dependencies, notably medial extractions and the challenging case of parasitic gaps [3]. In proof theoretic terms, our logic combines commutative and noncommutative behaviour, as well as linear and nonlinear resource management [4]. This is achieved with a single restricted modality. But unlike other extensions of Lambek Calculus with modalities [5], our logic remains decidable, and the complexity of proof search (i.e., sentence parsing) is the same as for the basic Lambek calculus. Furthermore, we provide not only a sequent calculus, and a cut elimination theorem, but also proof nets [6]. Keywords. {Substructural Logics, Permutation and Contraction, Exponentials, Proof Nets, Polarised Systems, Natural Language, Relativisation, Long Distance Dependencies } References. Bibliography


17:50 
Vitor Greati, Knotted substructural logics have fastgrowing complexity 
Substructural logics are obtained from classical logic and intuitionistic logic (\(\mathbf{IL}\)) by rejecting axioms corresponding to familiar structural properties like exchange (\(\mathbf e\)), weakening (\(\mathbf w\)) and contraction (\(\mathbf c\)). Such logics exhibit resourceawareness and this additional expressivity is wellsuited for applications in mathematics, computer science, linguistics and philosophy. For the same reason, these logics tend to be computationally very challenging. This is best illustrated by the decision problems of provability (the input formula is provable) and deducibility (the input formula is provable from an input set of formulas). For example, removing \((\mathbf c)\) from \(\mathbf{IL}\) yields a logic whose provability is PSPACEcomplete, and deducibility is {TOWER}complete (i.e., nonelementary). Remove \((\mathbf e)\) and \((\mathbf w)\) instead and both problems are undecidable. Removing just \((\mathbf w)\) from \(\mathbf{IL}\) yields a logic whose provability and deducibility are both Ackermanniancomplete (i.e., nonprimitive recursive, at level \(\mathbf{F}_\omega\) in the ordinalindexed fastgrowing hierarchy). We have already seen how the computational status varies with different combinations of structural properties. In this work, we discuss a natural family of logics arising when replacing \((\mathbf c)\) and \((\mathbf w)\) in \(\mathbf{IL}\) with a knotted axiom \(p^m \to p^n\). These logics possess analytic proof calculi but their analysis is impeded by sizeincreasing rules and the heavy combinatorial nature of the proofs. Specifically, we study the complexity of axiomatic extensions of the full Lambek logic \(\mathbf{FL}\) (that is, \(\mathbf{IL}\) minus \(\{(\mathbf e), (\mathbf w), (\mathbf c) \})\) with knotted axioms yielding fastgrowing complexity classifications. A key feature here is the reliance on multiple areas of mathematics and computer science: proof theory and wellquasiorder theory for deriving upper bounds, and reductions using algebraic counter machines to obtain lower bounds. Joint work with Nikolaos Galatos (Denver), Revantha Ramanayake (Groningen), and Gavin St. John (Salerno). 

18:10 
Valentina Trucco Dalmas, Investigating uniform interpolation via global termination 
A logic \(L\) has the Uniform Interpolation Property (UIP) if for every formula \(\phi\), and every propositional variable \(p\), there exists a formula \(E p. \phi\) built from variables in \(\phi\) different from \(p\), that satisfies \(\phi \to E p. \phi \in L\) and that whenever \(\phi \to \psi \in L\), we have \(E p. \phi \to \psi \in L\) for all \(\psi\) not containing \(p\). UIP can be interpreted as saying that the propositional quantifier \(\exists p\) is definable. In addition, UIP is a stronger version of the relatively betterunderstood Craig Interpolation Property. Interpolation properties are highly correlated with the expressive power of a logic and have been studied for many logics, including many nonclassical logics. In 1992, Andrew Pitts [1] established that Intuitionistic Propositional Logic has the UIP using a prooftheoretic approach. Pitts’ method crucially relies on a locally terminating proof calculus, i.e., a calculus where every rule’s premise is smaller than the conclusion w.r.t. some measure. While Pitts’ argument has been adapted to many nonclassical logics, all of these arguments use a locally terminating proof calculus or rely on the ability of the logic to express fixpoints, such as in the case of the modal \(\mu\)calculus. In this investigation, we aim to isolate the global termination conditions under which a modified Pitts’ method would remain applicable, to widen the scope of the prooftheoretic argument to nonclassical —and in particular, substructural— logics. This is joint work with Helle Hvid Hansen (Groningen) and Revantha Ramanayake (Groningen). Bibliography
