The paper has two parts: 1. A brief exposition of proof-theoretic semantics, not necessarily in connection to natural language. 2. A review, with a contrastive flavour, of some of the applications of PTS to NL with an indication of advantages of PTS as a theory of meaning for NL.

The goal of creating Artificial General Intelligence (AGI) – or in other words of creating Turing machines (modern computers) that can behave in a way that mimics human intelligence – has occupied AI researchers ever since the idea of AI was first proposed. One common theme in these discussions is the thesis that the ability of a machine to conduct convincing dialogues with human beings can serve as at least a sufficient criterion of AGI. We argue that this very ability (...) should be accepted also as a necessary condition of AGI, and we provide a description of the nature of human dialogue in particular and of human language in general against this background. We then argue that it is for mathematical reasons impossible to program a machine in such a way that it could master human dialogue behaviour in its full generality. This is (1) because there are no traditional explicitly designed mathematical models that could be used as a starting point for creating such programs; and (2) because even the sorts of automated models generated by using machine learning, which have been used successfully in areas such as machine translation, cannot be extended to cope with human dialogue. If this is so, then we can conclude that a Turing machine also cannot possess AGI, because it fails to fulfil a necessary condition thereof. At the same time, however, we acknowledge the potential of Turing machines to master dialogue behaviour in highly restricted contexts, where what is called “narrow” AI can still be of considerable utility. (shrink)

This paper is a reflexion on the computability of natural language semantics. It does not contain a new model or new results in the formal semantics of natural language: it is rather a computational analysis, in the context for type-logical grammars, of the logical models and algorithms currently used in natural language semantics, defined as a function from a grammatical sentence to a set of logical formulas—because a statement can be ambiguous, it can correspond to multiple formulas, one for each (...) reading. We argue that as long as we do not explicitly compute the interpretation in terms of possible world models, one can compute the semantic representation of a given statement, including aspects of lexical meaning. This is a very generic process, so the results are, at least in principle, widely applicable. We also discuss the algorithmic complexity of this process. (shrink)

Lambek elegantly characterized part of natural language. As is well-known, his substructural logic L, and its non-associative version NL, handle basic function/argument composition well, but not scope taking and syntactic displacement—at least, not in their full generality. In previous work, I propose $$\text {NL}_\lambda $$, which is NL supplemented with a single structural inference rule (“abstraction”). Abstraction closely resembles the traditional linguistic rule of quantifier raising, and characterizes both semantic scope taking and syntactic displacement. Due to the unconventional form of (...) the abstraction inference, there has been some doubt that $$\text {NL}_\lambda $$ should count at a legitimate substructural logic. This paper argues that $$\text {NL}_\lambda $$ is perfectly well-behaved. In particular, it enjoys cut elimination and an interpolation result. In addition, perhaps surprisingly, it is decidable. Finally, I prove that it is sound and complete with respect to the usual class of relational frames. (shrink)

\ is a 7000 line Prolog parser/theorem-prover for logical categorial grammar. In such logical categorial grammar syntax is universal and grammar is reduced to logic: an expression is grammatical if and only if an associated logical statement is a theorem of a fixed calculus. Since the syntactic component is invariant, being the logic of the calculus, logical categorial grammar is purely lexicalist and a particular language model is defined by just a lexical dictionary. The foundational logic of continuity was established (...) by Lambek while a corresponding extension including also logic of discontinuity was established by Morrill and Valentín :167–192, 2010). \ implements a logic including as primitive connectives the continuous and discontinuous connectives of the displacement calculus, additives, 1st order quantifiers, normal modalities, bracket modalities, and universal and existential subexponentials. In this paper we review the rules of inference for these primitive connectives and their linguistic applications, and we survey the principles of Andreoli’s focusing, and of a generalisation of van Benthem’s count-invariance, on the basis of which \ is implemented. (shrink)

We define and prove a formal semantics divided into two complementary interacting components: the strictly linguistic semantics, we call linguistic agent, and the strictly logical and referential semantics, we call rational agent. This Linguistic \ Rational Agents’ Semantics applies to Deep Dependency trees or more generally, to discourses, i.e. sequences of DD-trees, and interprets them by functional structures we call Meaning Representation Structures, similar to the DRT, but interpreted very differently. LRA semantics incrementally interprets the discourses by minimal finite models, (...) called proto-models, in a monotonic logic of the LA and checks the proto-models with respect to the classical models of the RA. The proto-model is considered as the linguistic sense of the discourse. We define in full detail the LA which, as we believe, must be universal. On the other hand, we don’t propose a particular RA. We only define the scheme of interaction between the two agents and the stimuli of the RA used by the LA. After all, every discourse has in LRA semantics the single meaning and the single sense for every Rational Agent used to interact with the Linguistic Agent. (shrink)

We show how to encode context-free string grammars, linear context-free tree grammars, and linear context-free rewriting systems as Abstract Categorial Grammars. These three encodings share the same constructs, the only difference being the interpretation of the composition of the production rules. It is interpreted as a first-order operation in the case of context-free string grammars, as a second-order operation in the case of linear context-free tree grammars, and as a third-order operation in the case of linear context-free rewriting systems. This (...) suggest the possibility of defining an Abstract Categorial Hierarchy. (shrink)

In this paper we present a logical system able to compute the semantics of both declarative and interrogative sentences. Our proposed analysis takes place at both the sentential and at the discourse level. We use syntactic inference on the sentential level for declarative sentences, while the discourse level comes into play for our treatment of questions. Our formalization uses a type logic sensitive to both the syntactic and semantic properties of natural language. We will show how an account of the (...) linguistic data follows naturally from the logical relations inherent in the type logic. (shrink)

This paper analyzes sluicing as anaphora to an anti-constituent (a continuation), that is, to the semantic remnant of a clause from which a subconstituent has been removed. For instance, in Mary said that [John saw someone yesterday], but she didn’t say who, the antecedent clause is John saw someone yesterday, the subconstituent targeted for removal is someone, and the ellipsis site following who is anaphoric to the scope remnant John saw ___ yesterday. I provide a compositional syntax and semantics on (...) which the relationship between the targeted subconstituent and the rest of the antecedent clause is one of scopability, not movement or binding. This correctly predicts that sluicing should be sensitive to scope islands, but not to syntactic islands. Unlike the currently dominant approaches to sluicing, there is no need to posit syntactic structure internal to the ellipsis site, nor is there any need for a semantic mutual-entailment requirement. Nevertheless, the fragment handles phenomena usually taken to suggest a close syntactic correspondence between the antecedent and the sluice, including case matching, voice matching, and verbal argument structure matching. In addition, the analysis handles phenomena exhibiting antecedent/sluice mismatches, including examples such as John remembers meeting someone, but he doesn’t remember who, , and especially so-called sprouting examples such as John left, but I don’t know when, in which there is no overt subconstituent to target for removal. In Sect. 5, I show how the analysis accounts for Andrews Amalgams such as Sally ate [I don’t know what] today, in which the antecedent surrounds the sluiced clause. Finally, in Sect. 6, I propose a new semantic constraint on sluicing: the Answer Ban, which says that the antecedent clause must not resolve, or even partially resolve, the issue raised by the sluiced interrogative. (shrink)

Abstract -/- Quantifier domain restriction (QDR) and two versions of nominal restriction (NR) are implemented as restrictions that depend on a previously introduced interpreter and interpretation time in a two-dimensional semantic framework on the basis of simple type theory and categorial grammar. Against Stanley (2002) it is argued that a suitable version of QDR can deal with superlatives like tallest. However, it is shown that NR is needed to account for utterances when the speaker intends to convey different restrictions for (...) multiple uses of the same quantifying determiner. We argue that NR generally fares better with such examples but also observe that examples like Every sailor waves at every sailor might be pragmatically anomalous. An account of contextual domain restriction is proposed that (i) excludes these anomalous readings (but it is shown how they could be included), (ii) makes it possible to express different contextual domain restrictions as long-range dependencies on an interpreter and an interpretation time, and (iii) additionally models restrictions based on locative constructions as general mereological constraints introduced by shifting the index. (shrink)

This paper argues for the idea that in describing language we should follow Haskell Curry in distinguishing between the structure of an expression and its appearance or manifestation . It is explained how making this distinction obviates the need for directed types in type-theoretic grammars and a simple grammatical formalism is sketched in which representations at all levels are lambda terms. The lambda term representing the abstract structure of an expression is homomorphically translated to a lambda term representing its manifestation, (...) but also to a lambda term representing its semantics. (shrink)

A method is described for inducing a type-logical grammar from a sample of bare sentence trees which are annotated by lambda terms, called term-labelled trees . Any type logic from a permitted class of multimodal logics may be specified for use with the procedure, which induces the lexicon of the grammar including the grammatical categories. A first stage of semantic bootstrapping is performed, which induces a general form lexicon from the sample of term-labelled trees using Fulop’s (J Log Lang Inf (...) 14(1):49–86, 2005) procedure. Next we present a two-stage procedure for performing distributional learning by unifying the lexical types that are initially discovered. The first structural unification algorithm in essence unifies the initial family of sets of types so that the resulting grammar will generate all term-labelled trees that follow the usage patterns evident from the learning sample. Further altering the lexical categories to generate a recursively extended language can be accomplished by a second unification. The combined unification algorithm is shown to yield a new type-logical lexicon that extends the learning sample to a possibly infinite (and possibly context-sensitive) language in a principled fashion. Finally, the complete learning strategy is analyzed from the perspective of algorithmic learning theory; the range of the procedure is shown to be a class of term-labelled tree languages which is finitely learnable from good examples (Lange et al in Algorithmic learning theory, Vol 872 of lecture notes in artificial intelligence, Springer, Berlin, pp 423–437), and so is identifiable in the limit as a corollary. (shrink)

The paper develops Lambda Grammars, a form of categorial grammar that, unlike other categorial formalisms, is non-directional. Linguistic signs are represented as sequences of lambda terms and are combined with the help of linear combinators.

This paper uses classical logic for a simultaneous description of the syntax and semantics of a fragment of English and it is argued that such an approach to natural language allows procedural aspects of linguistic theory to get a purely declarative formulation. In particular, it will be shown how certain construction rules in Discourse Representation Theory, such as the rule that indefinites create new discourse referents and definites pick up an existing referent, can be formulated declaratively if logic is used (...) as a metalanguage for English. In this case the declarative aspects of a rule are highlighted when we focus on the model theory of the description language while a procedural perspective is obtained when its proof theory is concentrated on. Themes of interest are Discourse Representation Theory, resolution of anaphora, resolution of presuppositions, and underspecification. (shrink)

This paper introduces λ-grammar, a form of categorial grammar that has much in common with LFG. Like other forms of categorial grammar, λ-grammars are multi-dimensional and their components are combined in a strictly parallel fashion. Grammatical representations are combined with the help of linear combinators, closed pure λ-terms in which each abstractor binds exactly one variable. Mathematically this is equivalent to employing linear logic, in use in LFG for semantic composition, but the method seems more practicable.

This paper uses a partially ordered set of syntactic categories to accommodate optionality and licensing in natural language syntax. A complex but well-studied data set pertaining to the syntax of quantifier scope and negative polarity licensing in Hungarian is used to illustrate the proposal. The presentation is geared towards both linguists and logicians. The paper highlights that the main ideas can be implemented in different grammar formalisms, and discusses in detail an implementation where the partial ordering on categories is given (...) by the derivability relation of a calculus with residuated and Galois-connected unary operators. (shrink)

The ‘syntax’ and ‘combinatorics’ of my title are what Curry (1961) referred to as phenogrammatics and tectogrammatics respectively. Tectogrammatics is concerned with the abstract combinatorial structure of the grammar and directly informs semantics, while phenogrammatics deals with concrete operations on syntactic data structures such as trees or strings. In a series of previous papers (Muskens, 2001a; Muskens, 2001b; Muskens, 2003) I have argued for an architecture of the grammar in which finite sequences of lambda terms are the basic data structures, (...) pairs of terms syntax, semantics for example. These sequences then combine with the help of simple generalizations of the usual abstraction and application operations. This theory, which I call Lambda Grammars and which is closely related to the independently formulated theory of Abstract Categorial Grammars (de Groote, 2001; de Groote, 2002), in fact is an implementation of Curry’s ideas: the level of tectogrammar is encoded by the sequences of lambda-terms and their ways of combination, while the syntactic terms in those sequences constitute the phenogrammatical level. In de Groote’s formulation of the theory, tectogrammar is the level of abstract terms, while phenogrammar is the level of object terms. (shrink)

Glue has evolved significantly during the past decade. Although the recent move to type-theoretic notation was a step in the right direction, basing the current Glue system on System F (second-order λ-calculus) was an unfortunate choice. An extension to two sorts and ad hoc restrictions were necessary to avoid inappropriate composition of meanings. As a result, the current system is unnecessarily complicated. A first-order Glue system is hereby proposed as its replacement. This new system is not only simpler and more (...) elegant, as it captures the exact requirements for Glue-style compositionality without ad hoc improvisations, but it also turns out to be more powerful than the current two-sorted (pseudo-) second-order system. First-order Glue supports all existing Glue analyses as well as more elegant alternatives. It also supports new, more demanding analyses. (shrink)

Using the programming-language concept of continuations, we propose a new, multimodal analysis of quantification in Type Logical Grammar. Our approach provides a geometric view of in-situ quantification in terms of graphs, and motivates the limited use of empty antecedents in derivations. Just as continuations are the tool of choice for reasoning about evaluation order and side effects in programming languages, our system provides a principled, type-logical way to model evaluation order and side effects in natural language. We illustrate with an (...) improved account of quantificational binding, weak crossover, wh-questions, superiority, and polarity licensing. (shrink)

I propose the first strictly compositional semantic account of same. New data, including especially NP-internal uses such as two men with the same name, suggests that same in its basic use is a quantificational element taking scope over nominals. Given type-lifting as a generally available mechanism, I show that this follows naturally from the fact that same is an adjective. Independently-motivated assumptions extend the analysis to standard examples such as Anna and Bill read the same book via a mechanism I (...) call PARASITIC SCOPE, in which the scope of same depends on the scope of some other scopetaking element in the sentence. Although I will initially discuss the analysis in terms of a familiar Quantifier Raising framework, I go on to implement the analysis within an innovative continuation-based Type-Logical Grammar. The empirical payoff for dealing in continuations is that a simple generalization of the basic analysis gives the first ever formal account of cases in which same distributes over objects other than NP denotations, as in the relevant interpretation of John hit and killed the same man. (shrink)

I argue that alternative-denoting expressions interact with their semantic context by taking scope. With an empirical focus on indefinites in English, I show how this approach improves on standard alternative-semantic architectures that use point-wise composition to subvert islands, as well as on in situ approaches to indefinites more generally. Unlike grammars based on point-wise composition, scope-based alternative management is thoroughly categorematic, doesn’t under-generate readings when multiple sources of alternatives occur on an island, and is compatible with standard treatments of binding. (...) Unlike all in situ treatments of indefinites, relying on a true scope mechanism prevents over-generation when an operator binds into an indefinite. My account relies only on function application, some mechanism for scope-taking, and two freely-applying type-shifters: the first is Karttunen’s :3–44, 1977. https://doi.org/10.1007/BF00351935) proto-question operator, aka Partee’s Studies in discourse representation theory and the theory of generalized quantifiers, Foris, Dordrecht, 1986) IDENT, and the second can be factored out of extant approaches to the semantics of questions in the tradition of Karttunen. These type-shifters form a decomposition of LIFT, the familiar function mapping values into scope-takers. Exceptional scope of alternative-generating expressions arises via scopal pied-piping: indefinites take scope over their island, which then itself takes scope. (shrink)

Involutive Nonassociative Lambek Calculus is a nonassociative version of Noncommutative Multiplicative Linear Logic, but the multiplicative constants are not admitted. InNL adds two linear negations to Nonassociative Lambek Calculus ; it is a strongly conservative extension of NL Logical aspects of computational linguistics. LNCS, vol 10054. Springer, Berlin, pp 68–84, 2016). Here we also add unary modalities satisfying the residuation law and De Morgan laws. For the resulting logic InNLm, we define and study phase spaces. We use them to prove (...) the cut elimination theorem for a one-sided sequent system for InNLm, introduced here. Phase spaces are also employed in studying auxiliary systems InNLm, assuming the k-cyclic law for negation. The latter behave similarly as Classical Nonassociative Lambek Calculus, studied in de Groote and Lamarche :355–388, 2002) and Buszkowski. We reduce the provability in InNLm to that in InNLm. This yields the equivalence of type grammars based on InNLm with -free) context-free grammars and the PTIME complexity of InNLm. (shrink)

Intertheoretic relations are an important topic in the philosophy of science. However, since their classical discussion by Ernest Nagel, such relations have mostly been restricted to relations between pairs of theories in the natural sciences. This paper presents a case study of a new type of intertheoretic relation that is inspired by Montague’s analysis of the linguistic syntax-semantics relation. The paper develops a simple model of this relation. To motivate the adoption of our new model, we show that this model (...) extends the scope of application of the Nagelian models and that it shares the epistemological advantages of the Nagelian model. The latter is achieved in a Bayesian framework. (shrink)

Nonassociative Lambek Calculus (NL) is a syntactic calculus of types introduced by Lambek [8]. The polynomial time decidability of NL was established by de Groote and Lamarche [4]. Buszkowski [3] showed that systems of NL with finitely many assumptions are decidable in polynomial time and generate context-free languages; actually the P-TIME complexity is established for the consequence relation of NL. Adapting the method of Buszkowski [3] we prove an analogous result for Nonassociative Lambek Calculus with unit (NL1). Moreover, we show (...) that any Lambek grammar based on NL1 (with assumptions) can be transformed into an equivalent context-free grammar in polynomial time. (shrink)

This paper investigates the learnability by positive examples in the sense of Gold of Pregroup Grammars. In a first part, Pregroup Grammars are presented and a new parsing strategy is proposed. Then, theoretical learnability and non-learnability results for subclasses of Pregroup Grammars are proved. In the last two parts, we focus on learning Pregroup Grammars from a special kind of input called feature-tagged examples. A learning algorithm based on the parsing strategy presented in the first part is given. Its validity (...) is proved and its properties are examplified. (shrink)

The paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s manifestation argument does not (...) obtain, and assertions are always warranted, having grounds of assertion. The proof system is shown to satisfy Dummett’s harmony property, justifying the ND rules as meaning conferring. The semantics is suitable for incorporation into computational linguistics grammars, formulated in type-logical grammar. (shrink)

While monadic second-order logic (MSO) has played a prominent role in model theoretic syntax, modal logics have been used in this context since its inception. When comparing propositional dynamic logic (PDL) to MSO over trees, Kracht (1997) noted that there are tree languages that can be defined in MSO that can only be defined in PDL by adding new features whose distribution is predictable. He named such features “inessential features”. We show that Kracht’s observation can be extended to other modal (...) logics of trees in two ways. First, we demonstrate that for each stronger logic, there exists a tree language that can only be defined in a weaker logic with inessential features. Second, we show that any tree language that can be defined in a stronger logic, but not in some weaker logic, can be defined with inessential features. Additionally, we consider Kracht’s definition of inessential features more closely. It turns out that there are features whose distribution can be predicted, but who fail to be inessential in Kracht’s sense. We will look at ways to modify his definition. (shrink)

The paper suggests a revision of the notion of harmony, a major necessary condition in proof-theoretic semantics for a natural-deduction proof-system to qualify as meaning conferring, when moving to a bilateral proof-system. The latter considers both forces of assertion and denial as primitive, and is applied here to positive logics, lacking negation altogether. It is suggested that in addition to the balance between introduction and elimination rules traditionally imposed by harmony, a balance should be imposed also on: negative introduction and (...) elimination rules, and positive and negative introduction rules. The paper suggests a proof-theoretical definition of duality, using which double harmony is defined. The paper proves that in a doubly-harmonious system, the coordination rule, typical to bilateral systems, is admissible. (shrink)

We look at two fundamental logical processes, often intertwined in planning and problem solving: inference and update. Inference is an internal process with which we uncover what is implicit in the information we already have. Update, on the other hand, is produced by external communication, usually in the form of announcements and in general in the form of observations, giving us information that might not have been available (even implicitly) before. Both processes have received attention from the logic community, usually (...) separately. In this work, we develop a logical language that allows us to describe them together. We present syntax, semantics and a complete axiom system; we discuss similarities and differences with other approaches and mention how the work can be extended. (shrink)

Action logic of Pratt [21] can be presented as Full Lambek Calculus FL [14, 17] enriched with Kleene star *; it is equivalent to the equational theory of residuated Kleene algebras (lattices). Some results on axiom systems, complexity and models of this logic were obtained in [4, 3, 18]. Here we prove a stronger form of *-elimination for the logic of *-continuous action lattices and the –completeness of the equational theories of action lattices of subsets of a finite monoid and (...) action lattices of binary relations on a finite universe. We also discuss possible applications in linguistics. (shrink)

Categorial grammar is well-known for its elegant analysis of coordination enabled by the flexible notion of constituency it entertains. However, to date, no systematic study exists that examines whether this analysis has any obvious empirical advantage over alternative analyses of nonconstituent coordination available in phrase structure-based theories of syntax. This paper attempts precisely such a comparison. We compare the direct constituent coordination analysis of non-canonical coordinations in categorial grammar with an ellipsis-based analysis of the same phenomena in the recent HPSG (...) literature. We provide a set of empirical evidence, consisting of cases in which non-canonical coordinations interact with scopal operators of various sorts, which systematically falsifies the predictions of the latter, ‘linearization-based’ ellipsis approach to coordination. We propose an alternative analysis in a variant of categorial grammar called Hybrid Type-Logical Categorial Grammar. The proposed framework builds on both the Lambek-inspired variants of categorial grammar and a more recent line of work modelling word order via a lambda calculus for the prosodic component. The flexible syntax–semantics interface of this framework straightforwardly captures the interactions between non-canonical coordinations and scopal expressions, demonstrating the broader empirical payoff of the direct constituent coordination analysis of non-canonical coordinations pioneered by Steedman :523–568, 1985; Linguist Philos 13:207–263, 1990) and Dowty hitherto not explicitly recognized in the literature. (shrink)

The paper suggests a revision of the notion of harmony, a major necessary condition in proof-theoretic semantics for a natural-deduction proof-system to qualify as meaning conferring, when moving to a bilateral proof-system. The latter considers both forces of assertion and denial as primitive, and is applied here to positive logics, lacking negation altogether. It is suggested that in addition to the balance between (positive) introduction and elimination rules traditionally imposed by harmony, a balance should be imposed also on: (i) negative (...) introduction and elimination rules, and (ii) positive and negative introduction rules. The paper suggests a proof-theoretical definition of duality (not referring to truthtables), using which double harmony is defined. The paper proves that in a doubly-harmonious system, the coordination rule, typical to bilateral systems, is admissible. (shrink)

We explore the power of type-logical grammar as a linguistic theory, specifically, of a new tentative development inside the framework—a “symmetricized” Lambek Calculus, due to [Moortgat2005]. The basis for our discussion is an account we give for constructions involving questions and—in particular—involving sluicing; it seeks to solve puzzles these constructions have been setting for linguistic theory. Two things in the organization of grammar are of interest here: first, a uniform system joining structures from the surface side (syntactic) and structures from (...) the “mind side” (discourse)—we call MERGE and co-MERGE the relations by which the former and the latter structures are arranged; second, a view on the circumstances of performing MOVE (by Syntax) from the type-logical perspective. As it is usual for type-logical grammars, the theory is conscious of semantics. We refer to examples from Japanese, on one side, and from English and Russian, on the other. (shrink)

The paper proposes a semantics for contextual (i.e., Temporal and Locative) Prepositional Phrases (CPPs) like during every meeting, in the garden, when Harry met Sally and where I’m calling from. The semantics is embodied in a multi-modal extension of Combinatory Categoral Grammar (CCG). The grammar allows the strictly monotonic compositional derivation of multiple correct interpretations for “stacked” or multiple CPPs, including interpretations whose scope relations are not what would be expected on standard assumptions about surfacesyntactic command and monotonic derivation. A (...) type-hierarchy of functional modalities plays a crucial role in the specification of the fragment. (shrink)

We show how to encode context-free string grammars, linear context-free tree grammars, and linear context-free rewriting systems as Abstract Categorial Grammars. These three encodings share the same constructs, the only difference being the interpretation of the composition of the production rules. It is interpreted as a first-order operation in the case of context-free string grammars, as a second-order operation in the case of linear context-free tree grammars, and as a third-order operation in the case of linear context-free rewriting systems. This (...) suggest the possibility of defining an Abstract Categorial Hierarchy. (shrink)

Glue semantics is a theory of the syntax–semantics interface according to which the syntactic structure of a sentence produces premises in a fragment of linear logic, and the semantic interpretation of the sentence correspond to the proof derivable from those premises. This paper describes how Glue can be connected to a Minimalist syntactic theory and compares the result with the more mainstream approach to the syntax–semantics interface in Minimalism, according to which the input to semantic interpretation is a syntactic structure (...) derived by covert movement operations. I argue that the Glue approach has advantages that make it worth exploring. (shrink)

We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.

We explore a computational algebraic approach to grammar via pregroups, that is, partially ordered monoids in which each element has both a left and a right adjoint. Grammatical judgements are formed with the help of calculations on types. These are elements of the free pregroup generated by a partially ordered set of basic types, which are assigned to words, here of English. We concentrate on the object pronoun who(m).

This chapter contains sections titled: Enriching Extensional Logic with Intensional Notions Changing Views of Modal Logic A Précis of Basic Modal Logic The Major Applications Fine‐Structure of Expressive Power System Combination: Action and Information Back to the Heartland Conclusion.

Geach’s rich paper ‘A Program for Syntax’ introduced many ideas into the arena of categorial grammar, not all of which have been given the attention they warrant in the thirty years since its first publication. Rather surprisingly, one of our findings (Section 3 below) is that the paper not only does not contain a statement of what has widely come to be known as “Geach’s Rule”, but in fact presents considerations which are inimical to the adoption of the rule in (...) question. With regard to at least some amongst the numerous other points extracted here from Geach’s discussion, we shall not be able to reach so definitive a conclusion, and content ourselves with giving the issues an airing. (shrink)

The aim of the present book is to give a comprehensive account of the ‘state of the art’ of substructural logics, focusing both on their proof theory and on their semantics (both algebraic and relational. It is for graduate students in either philosophy, mathematics, theoretical computer science or theoretical linguistics as well as specialists and researchers.

Lambek elegantly characterized part of natural language. As is well-known, his substructural logic L, and its non-associative version NL, handle basic function/argument composition well, but not scope taking and syntactic displacement—at least, not in their full generality. In previous work, I propose \, which is NL supplemented with a single structural inference rule.ion closely resembles the traditional linguistic rule of quantifier raising, and characterizes both semantic scope taking and syntactic displacement. Due to the unconventional form of the abstraction inference, there (...) has been some doubt that \ should count at a legitimate substructural logic. This paper argues that \ is perfectly well-behaved. In particular, it enjoys cut elimination and an interpolation result. In addition, perhaps surprisingly, it is decidable. Finally, I prove that it is sound and complete with respect to the usual class of relational frames. (shrink)

In this paper, we propose an extension of free pregroups with lower bounds on sets of pregroup elements. Pregroup grammars based on such pregroups provide a kind of an algebraic counterpart to universal quantification over type-variables. In particular, we show how our pregroup extensions can be used for pregroup grammars expressing natural-language coordination and extraction.