Since their introduction by Partee and Rooth (1983) into linguistic theory, type shifting principles have been extensively employed in various linguistic domains, including nominal predicates (Partee 1987), kind denoting NPs (Chierchia 1998), interrogatives (Groenendijk and Stokhof 1989), scrambled definites (De Hoop and Van der Does 1998) and plurals (Winter 2001,2002). Most of the accounts that use type shifting principles employ them as ``last resort'' mechanisms, which apply only when other compositional mechanisms fail. This failure is often sloppily referred to as (...) type mismatch . The motivation for introducing type mismatch into the compositional mechanism is twofold: on the one hand it allows lexical items to be assigned the minimal types that are needed for describing their denotation; on the other hand, it has been argued that the ``last resort'' strategy of type shifting prevents derivation of undesired meanings. The first goal of this paper is to define a simple notion of type mismatch, which will rather closely follow Partee and Rooth's original proposal but will be expressed within more familiar terms of categorial semantics. After introducing this implementation of traditional type mismatch, it will be argued that in fact, it covers only one possible kind of trigger for type shifting principles. Partee and Rooth's notion of mismatch is ``external'' in that the type of an expression is changed only when it combines with another type to which it cannot compose using the ``normal'' compositional mechanism. It will be argued that, within an appropriate type system, another notion of mismatch is also useful. This is the kind of mismatch in which the semantic type of an expression does not match its syntactic category. Two such cases will be explored: mismatch between morpho-syntactic number (singular or plural) and semantic number (a denotation ranging over atoms or sets), and mismatch between syntactic category (noun, DP, adjective etc.) and semantic role (predicate, quantifier, predicate modifier etc.).. (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)

A two-stage procedure is described which induces type-logical grammar lexicons from sentences annotated with skeletal terms of the simply typed lambda calculus. First, a generalized formulae-as-types correspondence is exploited to obtain all the type-logical proofs of the sample sentences from their lambda terms. The resulting lexicons are then optimally unified. The first stage constitutes the semantic bootstrapping (Pinker, Language Learnability and Language Development, Harvard University Press, 1984), while the unification procedure of Buszkowski and Penn represents a first attempt (...) at structure-dependent distributional learning of the syntactic and semantic categories. This effort extends earlier induction procedures (Buszkowski and Penn, 1990, Studia Logica 49, 431–454; Kanazawa, 1998, CSLI Publications and the European Association for Logic, Language and Information) for classical categorial grammar to at first the non-associative Lambek calculus, and then to a large class of type logics enriched by modal operators and structural rules. (shrink)

A two-stage procedure is described which induces type-logical grammar lexicons from sentences annotated with skeletal terms of the simply typed lambda calculus. First, a generalized formulae-as-types correspondence is exploited to obtain all the type-logical proofs of the sample sentences from their lambda terms. The resulting lexicons are then optimally unified. The first stage constitutes the semantic bootstrapping (Pinker, Language Learnability and Language Development, Harvard University Press, 1984), while the unification procedure of Buszkowski and Penn represents a first attempt (...) at structure-dependent distributional learning of the syntactic and semantic categories. This effort extends earlier induction procedures (Buszkowski and Penn, 1990, Studia Logica 49, 431–454; Kanazawa, 1998, CSLI Publications and the European Association for Logic, Language and Information) for classical categorial grammar to at first the non-associative Lambek calculus, and then to a large class of type logics enriched by modal operators and structural rules. (shrink)

In this paper I discuss a certain kind of 'type confusion' which involves use of expressions of the wrong grammatical category, as in the string 'runs eats'. It is (nearly) universally accepted that such strings are meaningless. My purpose in this paper is to question this widespread assumption (or as I call it, 'the last dogma'). I discuss a range of putative reasons for accepting the last dogma: in §II, semantic and metaphysical reasons; in §III, logical reasons; and in (...) §IV, syntactic reasons. I argue that none of these reasons is conclusive, and that consequently we should be willing to question this last dogma of type confusions. (shrink)

We give a formal interpretation of Martin-Löf's Constructive Theory of Types in Elementary Topos Theory which is presented as a formalised theory with intensional equality of objects. Types are interpreted as arrows and variables as sections of their types. This is necessary to model correctly the working of the assumption x ∈ A. Then intensional equality interprets equality of types. The normal form theorem which asserts that the interpretation of a type is intensional equal to the (...) pullback of its “alignment” along some “base” arrow relates this interpretation to categorical semantic of types. (shrink)

We started from the fact that type theory, in the way it was implemented in IL, makes it costly to deal with nominalization processes. We have also argued that the type hierarchy as such doesn't play any real role in a grammar; the classification it provides for different semantic objects is already contained, in some sense, in the categorial structure of the grammar itself. So, on the basis of a theory of properties (Cocchiarella's HST*) we have tried to (...) build a language (IL*) whose syntax does not contain any explicit typing of expressions. Some of the consequences that this move brings about in the overall organization of the grammar can be summarized as follows:it allows for a simple treatment of infinitives, gerunds, factives and, in general, all those phenomena which might be analyzed as cases of nominalization;it provides a simpler and more constrained semantics than IL, since IL* doesn't go beyond second order, and its non-modal basis is axiomatizable;it suggests that the role of logical form in a theory of grammar could be that of a family of theories of semantic objects;it eliminates the extrinsic limitations of a type hierarchy on the choice of the system of syntactic categories.I think that it is interesting to notice how having an explicit semantic framework helps to provide a sense in which it is legitimate to regard the syntax of a language as ‘autonomous’. (shrink)

This volume is a tribute to Roger Schwarzschild's immense contributions in the formal semantics of nouns, focus, degrees and space, and tense and aspect. Collectively, the papers in the volume reveal parallels across ontological domains, in particular in the context of elements with internal structure, like plural sets, alternative sets, degree intervals, temporal intervals, and vectors. This research suggests that the structure of an entity could inform the semantic behavior of that entity just as much than its semantic (...) type or lexical category. And because these structures dictate the formation of semantic alternatives, it can help inform focus semantics and scalar implicature as well. Old questions on plurals, focus and degree expressions get new answers in this collection of papers in honor of Roger Schwarzchild. Roger Schwarzschild is one of the leading scholars in semantics, and the editors have been highly successful in requesting contributions by his teachers, peers and former students. Some papers have circulated in draft form for many years, and find their final home in this edited volume, which well reflects the state of the art in the field. Prof. dr. Henriëtte de Swart, Utrecht University, The Netherlands. (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)

This article discusses New Confucian views on individuality and related philosophical problems. Special emphasis is given to the position of Tu Wei-Ming, a foremost living New Confucian thinker. It is pointed out that many New Confucian philosophers share a vision of a Confucian 'ideal' individuality or selfhood based on social integration - as opposed to a Western type of individuality sometimes portrayed as an individuality by isolation. These patterns of individuality are further examined on the basis of Niklas Luhmann's historical (...) analysis of the semantics of individuality and his categories of 'individuality by inclusion' and 'individuality by exclusion'. Finally, some parallels and differences between Confucian and the Luhmannian viewpoints are pointed out, and a suggestion on how a Luhmannian perspective might contribute to reformulations of New Confucian thought is attempted. (shrink)

Body part terms (BPTs) are used extensively in Mesoamerican languages to name object parts. The process through which BPTs might be extended to refer to a part of an object and further serve as a relator in describing the relation between objects in space has often been attributed to metaphorical processes. This study proposes an alternative analysis following a Structure–Mapping Theory approach (Gentner, 1983, inter alia), based on data from Diidxazá (Isthmus Zapotec, Otomanguean) obtained through elicitation and experimental tasks. The (...) data show that structure mapping does not depend on a 1:1 match of attributes; frequency of use shed light on principles that constrain the semantic extension of most BPTs; a core set of six BPTs are extended by abstraction of the set of intersecting axes of the body. The detailed nature of this study enables an analysis of the mental representations underlying the semantic extension of BPTs. This in turn elucidates on aspects of the relation between spatial language and spatial cognition. In addition, this study allows us to address questions about the categorial status of BPTs in Diidxazá and their lexicographic representation. (shrink)

The thesis is an attempt to give a precise formal semantics for various time-referential linguistic categories of English such as tense, perfect, progressive and Aktionsart or "action type", with the ultimate goal of explaining why with a verb phrase such as walk the inference from, for instance, John is walking to John has walked is intuitively valid, while with a verb phrase such as build a house the even weaker inference from John is building a house to John will have (...) built a house is intuitively invalid. The difference is seen as one of the Aktionsart of the sentences involved. ;Accordingly, a theory of Aktionsarten is developed in chapter 2. Four different Aktionsarten are formally distinguished. In chapter 3 a theory of the tenses and their interaction with temporal adverbials is worked out. Chapter 4 is about the perfect. The so-called "extended now" theory of the perfect is given a precise treatment. Finally, chapter 5 deals with some problems of the English progressive. Especially the so-called "imperfective paradox" is given a solution. ;The method I use is that of model-theoretic semantics applied to natural languages, as it was first developed by the logician, Richard Montague. (shrink)

The relevance of the research is defined by the need to create a set of linguistic means, which would contribute to effective communication with the general public, and the need to study different functional-semantic categories, including appeals, for the competent formation of public opinion in the political context. The research aims to comprehend the functioning of linguistic means used as appeals in the example of political propaganda texts in the English media field. The methodology is based on the theoretical (...) study of the works of modern linguists, linguistic, structural, and communicative analysis of appeal linguistic units and contexts. The research considered the linguistic means that form the functional-semantic category of the appeal, examples of political contexts from the British and American media were presented, the functions of appeal were presented using specific examples, an idea of the communicative side of political propaganda texts and audience participation in this process was formed, emphasis was placed on different types of propaganda (white, black, gray), the following groups of appeals were characterized: imperatives (volitional and involuntary). The materials presented in this research can be used to form an idea of the functional-semantic category of appeal, the choice of linguistic means for the purpose of information promotion in the media or social networks, the study of communicative strategies in linguistics and their successful implementation, consideration of political propaganda texts, increasing efficiency when influencing the audience, further implementation of means of appeal in machine learning. (shrink)

Sortally incorrect sentences have traditionally been referred to as "category mistakes" (Ryle ()) or "type crossings" (Drange ()). Sortal incorrectness is a ...

We use the category of presheaves over PTIME-functions in order to show that Cook and Urquhart's higher-order function algebra PV ω defines exactly the PTIME-functions. As a byproduct we obtain a syntax-free generalisation of PTIME-computability to higher types. By restricting to sheaves for a suitable topology we obtain a model for intuitionistic predicate logic with ∑ 1 b -induction over PV ω and use this to re-establish that the provably total functions in this system are polynomial time computable. Finally, (...) we apply the category-theoretic approach to a new higher-order extension of Bellantoni-Cook's system BC of safe recursion. (shrink)

The chapter outlines an abstract theoretical framework that is currently (re-)emerging in the course of a theoretical convergence of several disciplines. In the first section, the fundamental problem of perception theory is formulated, namely, the generation, by the perceptual system, of meaningful categories from physicogeometric energy patterns. In the second section, it deals with basic intuitions and assumptions underlying what can be regarded as the current Standard Model of Perceptual Psychology and points out why this model is profoundly inadequate for (...) dealing with the fundamental problem of perception theory. In the third section, it discusses a level of analysis that promises to be fruitful for dealing, in conformity with established procedures of the natural sciences, with the problem of perceptual “meaning” and the problem of what constitutes a “perceptual object.” In the fourth section, it outlines a theoretical perspective on basic principles of the perceptual system which centers on the notions of complex data types and conceptual forms, and draws an entirely different theoretical picture of the role of the sensory input than traditional accounts. The final section focusses on the issue of material qualities and discusses, within the general theoretical framework outlined, some observations and results on the perception of certain material properties, namely, lustrous and glassy appearances. (shrink)

Recent developments in the semantics of natural language seem to lead to a genuine synthesis of ideas from linguistics and logic, producing novel concepts and questions of interest to both parent disciplines. This book is a collection of essays on such new topics, which have arisen over the past few years. Taking a broad view, developments in formal semantics over the past decade can be seen as follows. At the beginning stands Montague's pioneering work, showing how a rigorous semantics can (...) be given for complete fragments of natural language by creating a suitable fit between syntactic categories and semantic types. This very enterprise already dispelled entrenched prejudices concerning the separation of linguistics and logic. Having seen the light, however, there is no reason at all to stick to the letter of Montague's proposals, which are often debatable. Subsequently, then, many improvements have been made upon virtually every aspect of the enterprise. More sophisticated grammars have been inserted (lately, lexical-functional grammar and generalized phrase structure grammar), more sensitive model structures have been developed (lately, 'partial' rather than 'total' in their com position), and even the mechanism of interpretation itself may be fine-tuned more delicately, using various forms of 'representations' mediating between linguistic items and semantic reality. In addition to all these refinements of the semantic format, descriptive coverage has extended considerably. (shrink)

There is growing support for the view that social categories like men and women refer to “objective types” (Haslanger 2000, 2006, 2012; Alcoff 2005). An objective type is a similarity class for which the axis of similarity is an objective rather than nominal or fictional property. Such types are independently real and causally relevant, yet their unity does not derive from an essential property. Given this tandem of features, it is not surprising why empirically-minded researchers interested in fighting (...) oppression and marginalization have found this ontological category so attractive: objective types have the ontological credentials to secure the reality (and thus political representation) of social categories, and yet they do not impose exclusionary essences that also naturalize and legitimize social inequalities. This essay argues that, from the perspective of these political goals of fighting oppression and marginalization, the category of objective types is in fact a Trojan horse; it looks like a gift, but it ends up creating trouble. I argue that objective type classifications often lack empirical adequacy, and as a result they lack political adequacy. I also provide, and in reference to the normative goals described above, several arguments for preferring a social ontology of natural kinds with historical essences. (shrink)

It is the aim of INDICES to document recent explorations in the various fields of philosophical logic and formal linguistics and their applications in other disciplines. The main emphasis of this series is on self-contained monographs covering particular areas of recent research and surveys of methods, problems, and results in all fields of inquiry where recourse to logical analysis and logical methods has been fruitful. INDICES will contain monographs dealing with the central areas of philosophical logic (extensional and intensional systems, (...) indexical logics, non-classical logics, philosophy of logic, etc.) as well as studies in which these systems are applied to specific issues in philosophy, in the formal semantics of natural languages, the foundations of linguistic theory, in computational linguistics, and in theoretical computer science. Constructive type theory was first presented in 1970, by the Swedish logician Per Martin-Lof. It has become one of the main approaches used in the foundations of mathematics and computer science. But it has remained relatively unknown among linguists and philosophers, although it provides a considerable extension of the concepts and techniques of logic. The book first gives an introduction to type theory from the point of view of linguistics and the philosophy of language. Type theory is then applied in the areas of quantification, anaphora, temporal reference, and the structure of text and discourse. By virtue of the type-theoretical concepts of proof object and context, various phenomena of dependence and progression in language can be discussed in precise terms, and several well-known problems can be solved. A categorial grammar is presented togenerate formally a fragment of English, together with an example of a computer implementation. (shrink)

Recent investigations and theorising about category-specific deficits have begun to focus upon patients with progressive brain disease such as semantic dementia and Alzheimer's disease. In this commentary we briefly review what insights have been gained from studying patients of this type. We concentrate on four specific issues: the sensory/functional distinction, correlation between features, neuroanatomical considerations, and confounding factors.

We introduce a typed version of the intuitionistic epsilon calculus. We give a categorical semantics of it introducing a class of categories which we call \-categories. We compare our results with earlier ones of Bell :323–337, 1993).

Many arguments for flexible type assignment to syntactic categories have to do with the need to account for the various scopings resulting from the interaction of quantified DPs with other quantified DPs or with intensional or negated verb contexts. We will define a type for arbitrary arity relations in polymorphic type theory. In terms of this, we develop the Boolean algebra of relations as far as needed for natural language semantics. The type for relations is flexible: it can do duty (...) for the whole family of types t, e → t, e → e → t, and so on. If we use this flexible type for the interpretations of verbs, we can perform a ‘flexible lift’ on DP interpretations, so that DPs get interpreted as operations on verb meanings. This leads to an elegant implementation of Keenan’s proposal for polyadic quantification in natural language (‘Beyond the Frege Boundary’). It turns out that scope reorderings are particularly easy to implement in this framework. (shrink)

This paper gives a simple method for providing categorial brands of feature-based unification grammars with a model-theoretic semantics. The key idea is to apply the paradigm of fibred semantics (or layered logics, see Gabbay (1990)) in order to combine the two components of a feature-based grammar logic. We demonstrate the method for the augmentation of Lambek categorial grammar with Kasper/Rounds-style feature logic. These are combined by replacing (or annotating) atomic formulas of the first logic, i.e. the basic syntactic (...) types, by formulas of the second. Modelling such a combined logic is less trivial than one might expect. The direct application of the fibred semantics method where a combined atomic formula like np (num: sg & pers: 3rd) denotes those strings which have the indicated property and the categorial operators denote the usual left- and right-residuals of these string sets, does not match the intuitive, unification-based proof theory. Unification implements a global bookkeeping with respect to a proof whereas the direct fibring method restricts its view to the atoms of the grammar logic. The solution is to interpret the (embedded) feature terms as global feature constraints while maintaining the same kind of fibred structures. For this adjusted semantics, the anticipated proof system is sound and complete. (shrink)

One well known problem regarding quantifiers, in particular the 1st order quantifiers, is connected with their syntactic categories and denotations.The unsatisfactory efforts to establish the syntactic and ontological categories of quantifiers in formalized first-order languages can be solved by means of the so called principle of categorial compatibility formulated by Roman Suszko, referring to some innovative ideas of Gottlob Frege and visible in syntactic and semantic compatibility of language expressions. In the paper the principle is introduced for (...) class='Hi'>categorial languages generated by the Ajdukiewicz’s classical categorial grammar. The 1st-order quantifiers are typically ambiguous. Every 1st-order quantifier of the type k > 0 is treated as a two-argument functor-function defined on the variable standing at this quantifier and its scope (the sentential function with exactly k free variables, including the variable bound by this quantifier); a binary function defined on denotations of its two arguments is its denotation. Denotations of sentential functions, and hence also quantifiers, are defined separately in Fregean and in situational semantics. They belong to the ontological categories that correspond to the syntactic categories of these sentential functions and the considered quantifiers. The main result of the paper is a solution of the problem of categories of the 1st-order quantifiers based on the principle of categorial compatibility. (shrink)

Kosta Došen argued in his papers Inferential Semantics (in Wansing, H. (ed.) Dag Prawitz on Proofs and Meaning, pp. 147–162. Springer, Berlin 2015) and On the Paths of Categories (in Piecha, T., Schroeder-Heister, P. (eds.) Advances in Proof-Theoretic Semantics, pp. 65–77. Springer, Cham 2016) that the propositions-as-types paradigm is less suited for general proof theory because—unlike proof theory based on category theory—it emphasizes categorical proofs over hypothetical inferences. One specific instance of this, Došen points out, is that the Curry–Howard (...) isomorphism makes the associativity of deduction composition invisible. We will show that this is not necessarily the case. (shrink)

One well known problem regarding quantifiers, in particular the 1storder quantifiers, is connected with their syntactic categories and denotations. The unsatisfactory efforts to establish the syntactic and ontological categories of quantifiers in formalized first-order languages can be solved by means of the so called principle of categorial compatibility formulated by Roman Suszko, referring to some innovative ideas of Gottlob Frege and visible in syntactic and semantic compatibility of language expressions. In the paper the principle is introduced for (...) class='Hi'>categorial languages generated by the Ajdukiewicz’s classical categorial grammar. The 1st-order quantifiers are typically ambiguous. Every 1st-order quantifier of the type k > 0 is treated as a two-argument functorfunction defined on the variable standing at this quantifier and its scope (the sentential function with exactly k free variables, including the variable bound by this quantifier); a binary function defined on denotations of its two arguments is its denotation. Denotations of sentential functions, and hence also quantifiers, are defined separately in Fregean and in situational semantics. They belong to the ontological categories that correspond to the syntactic categories of these sentential functions and the considered quantifiers. The main result of the paper is a solution of the problem of categories of the 1st-order quantifiers based on the principle of categorial compatibility. (shrink)

Lawvere hyperdoctrines give categorical algebraic semantics for intuitionistic predicate logic. Here we extend the hyperdoctrinal semantics to a broad variety of substructural predicate logics over the Typed Full Lambek Calculus, verifying their completeness with respect to the extended hyperdoctrinal semantics. This yields uniform hyperdoctrinal completeness results for numerous logics such as different types of relevant predicate logics and beyond, which are new results on their own; i.e., we give uniform categorical semantics for a broad variety of non-classical predicate logics. (...) And we introduce an analogue of Lawvere–Tierney topology and cotopology in the hyperdoctrinal setting, which gives a unifying perspective on different logical translations, in particular allowing for a uniform treatment of Girard’s exponential translation between linear and intuitionistic logics and of Kolmogorov’s double negation translation between intuitionistic and classical logics. In the hyerdoctrinal conception, type theories are categories, logics over type theories are functors, and logical translations between them, then, are natural transformations, in particular Lawvere–Tierney topologies and cotopologies on hyperdoctrines. The view of logical translations as hyperdoctrinal Lawvere–Tierney topologies and cotopologies has not been elucidated before, and may be seen as a novel contribution of the present work. From a broader perspective, this work may be regarded as taking first steps towards interplay between algebraic and categorical logics; it is, technically, a combination of substructural algebraic logic and hyperdoctrinal categorical logic, as the hyperdoctrinal completeness theorem is shown via the integration of the Lindenbaum–Tarski algebra construction with the syntactic category construction. As such this work lays a foundation for further interactions between algebraic and categorical logics. (shrink)

We present an analysis of the game semantics of general references introduced by Abramsky, Honda and McCusker which exposes the algebraic structure of the model. Using the notion of sequoidal category, we give a coalgebraic definition of the denotational semantics of storage cells of arbitrary type. We identify further conditions on the model which allow an axiomatic presentation of the proof that finite elements of the model are definable by programs, in the style of Abramsky’s Axioms for Definability.

DP hypothesis of Abney (1987), the syntactic unit that had formerly been known as noun phrase should in fact be analyzed as a phrase headed by a determiner, hence the label DP. Quite independently of this syntactic development, Partee (1987) proposed a type shifting paradigm for the semantic analysis of nominals (now called DPs). In Partee's proposal DPs are ambiguous between a referential reading of type e, a predicative reading of type et and a quantificational reading of type (et)t. (...) DP meanings can flexibly move between their different readings due to covert application of semantic operators. The present paper proposes some strong relationships between these syntactic and semantic paradigms. It is argued that the structure of the DP affects its semantics in that the NP level within the DP is purely predicative and the DP level itself is purely quantificational. However, the intermediate D' level is flexible between the predicate/quantifier semantic categories, due to the covert application of semantic operators at this level. Partee's assumption, adopted from Discourse Representation Theory and more traditional approaches in philosophical logic, that some DPs need to have a (discourse) referential reading, is withdrawn. Instead of Partee's type shifting operators between the three semantic categories she assumes, two operators are used between predicates and quantifiers. The choice function operation of Reinhart (1997) and Winter (1997) is used as a general operator from predicates to quantifiers. The minimum operator of Winter (1996) is used as a general operator from quantifiers to predicates. These two operations, referred to as category shifting operators , account for most of the Partee data and substantially extend the theory of flexibility to treat some intricate phenomena in the domains of coordination, plurality and scope. (shrink)

The paper contains an overview of the most important results presented in the monograph of the author "Teorie Językow Syntaktycznie-Kategorialnych" ("Theories of Syntactically-Categorial Languages" (in Polish), PWN, Warszawa-Wrocław 1985. In the monograph four axiomatic systems of syntactically-categorial languages are presented. The first two refer to languages of expression-tokens. The others also takes into consideration languages of expression-types. Generally, syntactically-categorial languages are languages built in accordance with principles of the theory of syntactic categories introduced by S. Leśniewski (...) [1929,1930]; they are connected with- the Ajdukiewicz’s work [1935] which was a continuation of Leśniewski’s idea and further developed and popularized in the research on categorial grammars, by Y. Bar-Hillel [1950,1953,1964]. To assign a suitable syntactic category to each word of the vocabulary is the main idea of syntactically-categorial approach to language. Compound expressions are built from the words of the vocabulary and then a suitable syntactic-category is assigned to each of them. A language built in this way should be decidable, which means that there should exist an algorithm for deciding about each expression of it, whether it is well-formed or is syntactically connected . The traditional, originating from Husserl, understanding of the syntactic category confronts some difficulties. This notion is defined by abstraction using the concept of affiliation of two expressions to the same syntactic category. (shrink)

Three different styles of foundations of mathematics are now commonplace: set theory, type theory, and category theory. How do they relate, and how do they differ? What advantages and disadvantages does each one have over the others? We pursue these questions by considering interpretations of each system into the others and examining the preservation and loss of mathematical content thereby. In order to stay focused on the “big picture”, we merely sketch the overall form of each construction, referring to the (...) literature for details. Each of the three steps considered below is based on more recent logical research than the preceding one. The first step from sets to types is essentially the familiar idea of set theoretic semantics for a syntactic system, i.e. giving a model; we take a brief glance at this step from the current point of view, mainly just to fix ideas and notation. The second step from types to categories is known to categorical logicians as the construction of a “syntactic category”; we give some specifics for the benefit of the reader who is not familiar with it. The third step from categories to sets is based on quite recent work, but captures in a precise way an intuition from the early days of foundational studies. With these pieces in place, we can then draw some conclusions regarding the differences between the three schemes, and their relative merits. In particular, it is possible to state more precisely why the methods of category theory are more appropriate to philosophical structuralism. (shrink)

Mitchell, J.C. and E. Moggi, Kripke-style models for typed lambda calculus, Annals of Pure and Applied Logic 51 99–124. The semantics of typed lambda calculus is usually described using Henkin models, consisting of functions over some collection of sets, or concrete cartesian closed categories, which are essentially equivalent. We describe a more general class of Kripke-style models. In categorical terms, our Kripke lambda models are cartesian closed subcategories of the presheaves over a poset. To those familiar with Kripke models of (...) modal or intuitionistic logics, Kripke lambda models are likely to seem adequately ‘semantic’. However, when viewed as cartesian closed categories, they do not have the property variously referred to as concreteness, well- pointedness or having enough points. While the traditional lambda calculus proof system is not complete for Henkin models that may have empty types, we prove strong completeness for Kripke models. In fact, every set of equations that is closed under implication is the theory of a single Kripke model. We also develop some properties of logical relations over Kripke structures, showing that every theory is the theory of a model determined by a Kripke equivalence relation over a Henkin model. We discuss cartesian closed categories but present the main definitions and results without the use of category theory. (shrink)

Language in Action demonstrates the viability of mathematical research into the foundations of categorial grammar, a topic at the border between logic and linguistics. Since its initial publication it has become the classic work in the foundations of categorial grammar. A new introduction to this paperback edition updates the open research problems and records relevant results through pointers to the literature. Van Benthem presents the categorial processing of syntax and semantics as a central component in a more (...) general dynamic logic of information flow, in tune with computational developments in artificial intelligence and cognitive science. Using the paradigm of categorial grammar, he describes the substructural logics driving the dynamics of natural language syntax and semantics. This is a general type-theoretic approach that lends itself easily to proof-theoretic and semantic studies in tandem with standard logic. The emphasis is on a broad landscape of substructural categorial logics and their proof-theoretical and semantic peculiarities. This provides a systematic theory for natural language understanding, admitting of significant mathematical results. Moreover, the theory makes possible dynamic interpretations that view natural languages as programming formalisms for various cognitive activities. (shrink)

The chapter looks at an aspect of David Lewis’s work on language that has been important for the foundation and history of formal semantics as a discipline practiced by both linguists and philosophers of language: a referential semantics over possible worlds that is connected to linguistically plausible syntactic structures. Lewis’s original contributions are placed within their historical context: Church’s typed lambda calculus, Carnapian intensions, the categorial grammars of Ajdukiewicz, and Chomsky’s theories of the relation between syntax and semantics. Relying (...) on Lewis’s letters, the chapter identifies the works of Stenius, Davidson, and Katz as triggering Lewis’s interest in formal theories of natural language semantics and clarifies the relation between his and Montague’s contributions to the foundation of the discipline. (shrink)

The Lambek-Grishin calculus is a symmetric version of categorial grammar obtained by augmenting the standard inventory of type-forming operations (product and residual left and right division) with a dual family: coproduct, left and right difference. Interaction between these two families is provided by distributivity laws. These distributivity laws have pleasant invariance properties: stability of interpretations for the Curry-Howard derivational semantics, and structure-preservation at the syntactic end. The move to symmetry thus offers novel ways of reconciling the demands of natural (...) language form and meaning. (shrink)

Category mistakes are sentences such as ‘Colourless green ideas sleep furiously’ or ‘The theory of relativity is eating breakfast’. Such sentences are highly anomalous, and this has led a large number of linguists and philosophers to conclude that they are meaningless (call this ‘the meaninglessness view’). In this paper I argue that the meaninglessness view is incorrect and category mistakes are meaningful. I provide four arguments against the meaninglessness view: in Sect. 2, an argument concerning compositionality with respect to category (...) mistakes; in Sect. 3 an argument concerning synonymy facts of category mistakes; in Sect. 4 concerning embeddings of category mistakes in propositional attitude ascriptions; and in Sect. 5 concerning the uses of category mistakes in metaphors. Having presented these arguments, in Sect. 6 I briefly discuss some of the positive motivations for accepting the meaninglessness view and argue that they are unconvincing. I conclude that the meaninglessness view ought to be rejected. (shrink)

Barendregt gave a sound semantics of the simple type assignment system λ → by generalizing Tait’s proof of the strong normalization theorem. In this paper, we aim to extend the semantics so that the completeness theorem holds.

Homotopy Type Theory (HoTT) is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might (...) be expected to answer, and find that many of them are not answered by the standard formulation of HoTT as presented in the ‘HoTT Book’. More importantly, the presentation of HoTT given in the HoTT Book is not autonomous since it explicitly depends upon other fields of mathematics, in particular homotopy theory. We give an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory (but is compatible with the homotopy interpretation), and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on a new interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory. 1 Introduction2 What Is a Foundation for Mathematics? 2.1 A characterization of a foundation for mathematics 2.2 Autonomy3 The Basic Features of Homotopy Type Theory 3.1 The rules 3.2 The basic ways to construct types 3.3 Types as propositions and propositions as types 3.4 Identity 3.5 The homotopy interpretation4 Autonomy of the Standard Presentation?5 The Interpretation of Tokens and Types 5.1 Tokens as mathematical objects? 5.2 Tokens and types as concepts6 Justifying the Elimination Rule for Identity7 The Foundations of Homotopy Type Theory without Homotopy 7.1 Framework 7.2 Semantics 7.3 Metaphysics 7.4 Epistemology 7.5 Methodology8 Possible Objections to this Account 8.1 A constructive foundation for mathematics? 8.2 What are concepts? 8.3 Isn’t this just Brouwerian intuitionism? 8.4 Duplicated objects 8.5 Intensionality and substitution salva veritate9 Conclusion 9.1 Advantages of this foundation. (shrink)

In this paper, we shall present a generalization of phrase structure grammar, in which all functional categories have type restrictions, that is, their argument types are specific domains. In ordinary phrase structure grammar, there is just one universal domain of individuals. The grammar does not make a distinction between verbs and adjectives in terms of domains of applicability. Consequently, it fails to distinguish between sentences like every line intersects every line, which is well typed, and every line intersects every (...) point, which is ill typed.Our generalization relates to ordinary phrase structure grammar in the same way as the higherlevel constructive type theory of Martin-Löf relates to the simple type theory of Church . Simple type theory has been used in linguistics and related with phrase structure grammar, especially in the tradition based on the work of Montague .Our definition of the grammar will be more formal than Montague's in the sense that we shall use a formal metalanguage, that of constructive type theory, for defining both the object language and its interpretation. The grammar, both syntax and semantics, is thus readily implementable in the type-theoretical proof system ALF . Inside type theory, a distinction can be made between the object language and the model, in other words, between syntactic and semantic types. It will turn out that the object language cannot be defined independently of the model, as in ordinary Tarski semantics. This is a direct consequence of introducing the typing restrictions.The grammar presented here can be seen as a formal linguistic elaboration of the work presented in Ranta 1991 and 1994. The organization of generative grammar as categorial grammar followed by sugaring should now look more familiar to the linguist, as the grammatical formalism on which sugaring operates is no longer full type theory but a set of phrase structure trees. (shrink)

We discuss the semantical categories of base and object implicit in the Curry-Howard theory of types and we derive derive logic and, in particular, the comprehension principle in the classical version of the theory. Two results that apply to both the classical and the constructive theory are discussed. First, compositional semantics for the theory does not demand ‘incomplete objects’ in the sense of Frege: bound variables are in principle eliminable. Secondly, the relation of extensional equality for each type is (...) definable in the Curry-Howard theory. (shrink)

We extend to the exponential connectives of linear logic the study initiated in Bucciarelli and Ehrhard 247). We define an indexed version of propositional linear logic and provide a sequent calculus for this system. To a formula A of indexed linear logic, we associate an underlying formula of linear logic, and a family A of elements of , the interpretation of in the category of sets and relations. Then A is provable in indexed linear logic iff the family A is (...) contained in the interpretation of some proof of . We extend to this setting the product phase semantics of indexed multiplicative additive linear logic introduced in Bucciarelli and Ehrhard , defining the symmetric product phase spaces. We prove a soundness result for this truth-value semantics and show how a denotational model of linear logic can be associated to any symmetric product phase space. Considering a particular symmetric product phase space, we obtain a new coherence space model of linear logic, which is non-uniform in the sense that the interpretation of a proof of !A−B contains informations about the behavior of this proof when applied to “chimeric” arguments of type A . In this coherence semantics, an element of a web can be strictly coherent with itself, or two distinct elements can be “neutral”. (shrink)

In this paper, I intend to reconstruct Ockham’s semantics of the categories in order to prove first that his semantics is consistent. Second, Ockham is not skeptical about the possibility to derive the categories from primitives. According to Ockham, one must accept two principles in order to derive the categories. The first is the principle of ‘in quid’ predication, according to which a name of category can be predicated ‘in quid’ of a determined class of terms. The second is the (...) principle of the transitivity of predication, according to which A is predicated of C if A is predicated of B and B is predicated of C. I will show that Ockham’s semantics of the categories makes two assumptions. According to the first assumption, there exist only two types of things, substances and qualities. According to the second, the categories are mutually exclusive. Ockham’s semantics of the categories implies that the categories are both ontological and conceptual and that it is not possible to prove that there is a determined number of categories. (shrink)

This paper introduces some of the main components of a novel type theoretical semantics for quantifi- cation with plural noun phrases. This theory, unlike previous ones, sticks to the standard generalized quantifier treatment of singular noun phrases and uses only one lifting operator per semantic category (predicate, quantifier and determiner) for quantification with plurals. Following Bennett (1974), plural individuals are treated as functions of type ¢¡ . Plural nouns and other plural predicates accordingly denote £ ¢¡¥¤¦¡ functions. Such predicates (...) do not match the standard £ ¢¡¥¤ £§£ ¢¡¨¤©¡¥¤ type of determiners. Following Partee and Rooth (1983), type mismatches are resolved using type shifting operators. These operators derive collectivity with plurals, keeping the analysis of singular noun phrases, where no type mismatch arises, as in Barwise and Cooper (1981). A single type shifting operator for determiners combines into one reading the existential shift and the counting (neutral) shift of Scha (1981) and Van der Does (1993). This operator combines the conservativity principle of generalized quantifier theory with Szabolcsi’s (1997) existential quantification over witness sets. The unified lift prevents unmotivated ambiguity as well as the monotonicity ill of existential lifts pointed out by Van Benthem.. (shrink)

A model of metaphor processing is suggested based on the application of pragmatic principles to the type of semantic information easy to access. It is argued that, with metaphor, higher-order categorical knowledge is given processing preference over instance-specific knowledge in an attempt to recover likely intended meaning. Instance-specific information is used more often when the higher-order knowledge is taken to violate conversational postulates. One such violation occurs when the categories implicated by metaphor topic and vehicle are similar, and thus (...) unlikely to provide new or relevant information. It is argued further that these differences could, in part, explain at least one condition that produces the asymmetry observed in metaphor when topic and vehicle are reversed. Predictions supportive of the model were obtained in three studies, employing different methodologies: feature listing, recognition memory and a vehicle choice task. (shrink)

This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to view such models as full subcategories of categorical models of intuitionistic set theory. It is shown that the existence of solutions to recursive domain equations depends upon the strength of the set theory. We observe that the internal set theory of an elementary topos is not strong enough to guarantee their existence. In (...) contrast, as our first main result, we establish that solutions to recursive domain equations do exist when the category of sets is a model of full intuitionistic Zermelo–Fraenkel set theory. We then apply this result to obtain a denotational interpretation of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. By exploiting the intuitionistic logic of the ambient model of intuitionistic set theory, we analyse the relationship between operational and denotational semantics. We first prove an “internal” computational adequacy theorem: the model always believes that the operational and denotational notions of termination agree. This allows us to identify, as our second main result, a necessary and sufficient condition for genuine “external” computational adequacy to hold, i.e. for the operational and denotational notions of termination to coincide in the real world. The condition is formulated as a simple property of the internal logic, related to the logical notion of 1-consistency. We provide useful sufficient conditions for establishing that the logical property holds in practice. Finally, we outline how the methods of the paper may be applied to concrete models of FPC. In doing so, we obtain computational adequacy results for an extensive range of realizability and domain-theoretic models. (shrink)

Embodied cognitive theories predict that linguistic conceptual representations are grounded and continually represented in real world, sensorimotor experiences. However, there is an on-going debate on whether this also holds for abstract concepts. Grammar is the archetype of abstract knowledge, and therefore constitutes a test case against embodied theories of language representation. Former studies have largely focussed on lexical-level embodied representations. In the present study we take the grounding-by-modality idea a step further by using reaction time (RT) data from the linguistic (...) processing of nominal classifiers in Chinese. We take advantage of an independent body of research, which shows that attention in hand space is biased. Specifically, objects near the hand consistently yield shorter RTs as a function of readiness for action on graspable objects within reaching space, and the same biased attention inhibits attentional disengagement. We predicted that this attention bias would equally apply to the graspable object classifier but not to the big object classifier. Chinese speakers (N = 22) judged grammatical congruency of classifier-noun combinations in two conditions: graspable object classifier and big object classifier. We found that RTs for the graspable object classifier were significantly faster in congruent combinations, and significantly slower in incongruent combinations, than the big object classifier. There was no main effect on grammatical violations, but rather an interaction effect of classifier type. Thus, we demonstrate here grammatical category- specific effects pertaining to the semantic content and by extension the visual and tactile modality of acquisition underlying the acquisition of these categories. We conclude that abstract grammatical categories are subjected to the same mechanisms as general cognitive and neurophysiological processes and may therefore be grounded. (shrink)

Types are a crucial concept in conceptual modelling, logic, and knowledge representation as they are an ubiquitous device to un- derstand and formalise the classification of objects. We propose a logical treatment of types based on a cognitively inspired modelling that ac- counts for the amount of information that is actually available to a cer- tain agent in the task of classification. We develop a predicative modal logic whose semantics is based on conceptual spaces that model the ac- (...) tual information that a cognitive agent has about objects, types, and the classification of an object under a certain type. In particular, we ac- count for possible failures in the classification, for the lack of sufficient information, and for some aspects related to vagueness. (shrink)

It’s generally assumed that a compositional semantic theory will have to recognise a semantic category of expressions which serve simply to pick out some one object: e-type expressions. Kripke’s views about names, Kaplan’s about indexicals and demonstratives, the standard Tarskian semantics for bound variables, Heim and Kratzer’s Strawsonian view about definites, even an analysis of indefinites, assume as much. In this thesis, I argue that recent advances in the semantics of names and of quotation, and in metaphysics, give (...) good reason to doubt there is such a category. I do so in two parts. In the first part, comprising about two thirds of the thesis, I combine two recent views, one from semantics and one from metaphysics. From semantics, I take over predicativism about names, the view, as one might have guessed, that names are predicates. From metaphysics, I take over the doctrine that there are temporal parts. Putting them together, I hold that the semantic contribution of the name ’Joan’, in a sentence like ’Joan is a barrister’, is a predicate, and in particular a predicate the extension of which is Joan’s temporal parts. Names are not, as is commonly thought, e-type expressions. In the second part, building on the first, I further undermine the existence of a semantically important category of e-type expressions by arguing that a construction which might be thought to mandate such a category, namely de re attitude ascriptions, in fact, when properly analysed, does not do so. I argue this by considering the nature of transparent occurrences of expressions in opaque contexts in general, and in particular by considering the phenomenon of mixed quotation. I present a new theory of it, and show how it can be parlayed into a new Fregean theory of de re attitude ascriptions. The thesis overall, then, will provide strong evidence against the semantic importance of e-type expressions either in language, or in thought. (shrink)

The aim of the paper is to show that topoi are useful in the categorial analysis of the constructive logic with strong negation. In any topos ϵ we can distinguish an object Λ and its truth-arrows such that sets ϵ have a Nelson algebra structure. The object Λ is defined by the categorial counterpart of the algebraic FIDEL-VAKARELOV construction. Then it is possible to define the universal quantifier morphism which permits us to make the first order predicate calculus. (...) The completeness theorem is proved using the Kripke-type semantic defined by THOMASON. (shrink)

This 1994 book develops a way of representing the meanings of linguistic expressions which is independent of any particular language, allowing the expressions to be manipulated in accordance with rules related to their meanings which could be implemented on a computer. It begins with a survey of the contributions of linguistics, logic and computer science to the problem of representation, linking each with a particular type of formal grammar. A system of graphs is then presented, organized by scope relations in (...) which linguistic constituents are sub-graphs whose configuration is determined by their categories. In developing this system, the author extends the notion of scope and argues that anaphoric and relative pronouns are structural signs not linguistic constituents. Certain count nouns are made the basis of this system and an account of proper names relating the count nouns, is given. (shrink)