Authors: Mehrnoosh Sadrzadeh and Lutz Straßburger

Lambek Calculus is a non-commutative 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 non-commutative behaviour, as well as linear and non-linear 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

1. Joachim Lambek. The Mathematics of Sentence Structure. American Mathematical Monthly, 65:154–170, 1958.
2. Guy Barry, Mark Hepple, Neil Leslie, Glyn Morrill. Proof Figures And Structural Operators For Categorial Grammar. EACL 1991, 5th Conference of the European Chapter of the Association for Computational Linguistics. 198–203, 1991.
3. Elisabet Engdahl. Parasitic Gaps. Linguistics and Philosophy, 6: 5–34, 1983.
4. , Jean-Yves. Linear Logic. Theoretical Computer Science. 50: 1-102, 1987.
5. Kanovich, Kuznetsov, Scedrov. Undecidability of the Lambek calculus with a relevantmodality. Lecture Notes in Computer Science, 9804:240–256, 2016.
6. Fran\c{c}ois Lamarche and Christian Retoré. Proof nets for the Lambek-calculus — an overview. Proceedings of the Third Roma Workshop “Proofs and Linguistic Categories. 241-262, 1996.

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 resource-awareness and this additional expressivity is well-suited 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 PSPACE-complete, and deducibility is {TOWER}-complete (i.e., non-elementary). 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 Ackermannian-complete (i.e., non-primitive recursive, at level \(\mathbf{F}_\omega\) in the ordinal-indexed fast-growing 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 size-increasing 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 fast-growing complexity classifications. A key feature here is the reliance on multiple areas of mathematics and computer science: proof theory and well-quasi-order 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).

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 better-understood Craig Interpolation Property. Interpolation properties are highly correlated with the expressive power of a logic and have been studied for many logics, including many non-classical logics.

In 1992, Andrew Pitts [1] established that Intuitionistic Propositional Logic has the UIP using a proof-theoretic 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 non-classical 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 proof-theoretic argument to non-classical —and in particular, substructural— logics.

This is joint work with Helle Hvid Hansen (Groningen) and Revantha Ramanayake (Groningen).

Bibliography

1. Andrew M. Pitts,On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional LogicJournal of Symbolic Logic,vol. 57 (1992), no. 1, pp. 33–52.