Type-Theoretic Semantics

This paper applies homotopy type theory to formal semantics of natural languages and proposes a new model for the linguistic phenomenon of copredication. Copredication refers to sentences where two predicates which assume different requirements for their arguments are asserted for one single entity, e.g., "the lunch was delicious but took forever". This paper is particularly concerned with copredication sentences with quantification, i.e., cases where the two predicates impose distinct criteria of quantification and individuation, e.g., "Fred picked up and mastered three (...) books." In our solution developed in homotopy type theory and using the rule of existential closure following Heim analysis of indefinites, common nouns are modeled as identifications of their aspects using HoTT identity types, e.g., the common noun book is modeled as identifications of its physical and informational aspects. The previous treatments of copredication in systems of semantics which are based on simple type theory and dependent type theories make the correct predictions but at the expense of ad hoc extensions (e.g., partial functions, dot types and coercive subtyping). The model proposed here, also predicts the correct results but using a conceptually simpler foundation and no ad hoc extensions. (shrink)

This is a review of "Properties and Propositions: The Metaphysics of Higher-Order Logic" by Robert Trueman. Following an overview of the main themes of the book, I discuss the metaphysical presuppositions of Trueman's Fregean notation for predicate abstraction and evaluate his argument for strict typing.

This paper investigates the connection between two recent trends in philosophy: higher-orderism and conceptual engineering. Higher-orderists use higher-order quantifiers (in particular quantifiers binding variables that occupy the syntactic positions of predicates) to express certain key metaphysical doctrines, such as the claim that there are properties. I argue that, on a natural construal, the higher-orderist approach involves an engineering project concerning, among others, the concept of existence. I distinguish between a modest construal of this project, on which it aims at engineering (...) higher-order analogues of the familiar notion of first-order existence, and an ambitious construal, on which it additionally aims at engineering a broadened notion of existence that subsumes first-order and higher-order existence. After identifying a substantial problem for the ambitious project, I investigate a possible response which is based on adopting a cumulative type theory as the background higher-order logic. While effective against the problem at hand, this strategy turns out to undermine a major reason to embrace higher-orderism in the first place, namely the idea that higher-orderism dissolves a range of otherwise intractable debates in metaphysics. Higher-orderists are therefore best advised to pursue their engineering project on the modest variant and against the background of standard type theory. (shrink)

Universals are putative objects like wisdom, morality, redness, etc. Although we believe in properties (which, we argue, are not a kind of object), we do not believe in universals. However, a number of ordinary, natural language constructions seem to commit us to their existence. In this paper, we provide a fictionalist theory of universals, which allows us to speak as if universals existed, whilst denying that any really do.

Can conjunctive propositions be identical without their conjuncts being identical? Can universally quantified propositions be identical without their instances being identical? On a common conception of propositions, on which they inherit the logical structure of the sentences which express them, the answer is negative both times. Here, it will be shown that such a negative answer to both questions is inconsistent, assuming a standard type-theoretic formalization of theorizing about propositions. The result is not specific to conjunction and universal quantification, but (...) applies to any binary operator and propositional quantifier. It is also shown that the result essentially arises out of giving a negative answer to both questions, as each negative answer is consistent by itself. (shrink)

Transparent intensional logic (TIL) is a well-explored type-theoretical framework for semantics of natural language. However, its treatment of polymorphic functions, which are essential for the analysis of various natural language phenomena, is still underdeveloped. In this paper, we address this issue and propose an extension of TIL that introduces polymorphism via type variables ranging over types and generalized variables ranging over constructions and types. Furthermore, we offer an analysis of sentences involving non-specific notional attitudes of the general form ‘_A_ considers (...) (believes, desires, wants, seeks,...) something’. (shrink)

Standard Type Theory, STT, tells us that b^n(a^m) is well-formed iff n=m+1. However, Linnebo and Rayo have advocated the use of Cumulative Type Theory, CTT, has more relaxed type-restrictions: according to CTT, b^β(a^α) is well-formed iff β > α. In this paper, we set ourselves against CTT. We begin our case by arguing against Linnebo and Rayo’s claim that CTT sheds new philosophical light on set theory. We then argue that, while CTT ’s type-restrictions are unjustifiable, the type-restrictions imposed by (...) STT are justified by a Fregean semantics. What is more, this Fregean semantics provides us with a principled way to resist Linnebo and Rayo’s Semantic Argument for CTT. We end by examining an alternative approach to cumulative types due to Florio and Jones; we argue that their theory is best seen as a misleadingly formulated version of STT. (shrink)

In this paper I will explore the question whether the Trivialization construction of transparent intensional logic (TIL) can be understood in terms of the Execution construction, specifically, in terms of its degenerate case known as the 0-Execution. My answer will be positive and the apparent contrast between the intuitive understanding of Trivialization and 0-Execution will be explained as a matter of distinct yet related informal perspectives, not as a matter of technical or conceptual differences.

Semantic theories based on a hierarchy of types have prominently been used to defend the possibility of unrestricted quantification. However, they also pose a prima facie problem for it: each quantifier ranges over at most one level of the hierarchy and is therefore not unrestricted. It is difficult to evaluate this problem without a principled account of what it is for a quantifier to be unrestricted. Drawing on an insight of Russell’s about the relationship between quantification and the structure of (...) predication, we offer such an account. We use this account to examine the problem in three different type-theoretic settings, which are increasingly permissive with respect to predication. We conclude that unrestricted quantification is available in all but the most permissive kind of type theory. (shrink)

In a series of papers Ladyman and Presnell raise an interesting challenge of providing a pre-mathematical justification for homotopy type theory. In response, they propose what they claim to be an informal semantics for homotopy type theory where types and terms are regarded as mathematical concepts. The aim of this paper is to raise some issues which need to be resolved for the successful development of their types-as-concepts interpretation.

In this paper, I utilise the growing literature on scientific modelling to investigate the nature of formal semantics from the perspective of the philosophy of science. Specifically, I incorporate the inferential framework proposed by Bueno and Colyvan : 345–374, 2011) in the philosophy of applied mathematics to offer an account of how formal semantics explains and models its data. This view produces a picture of formal semantic models as involving an embedded process of inference and representation applying indirectly to linguistic (...) phenomena. The final aim of the paper is directed at proposing a novel account of the syntax–semantics interface while shedding light on empty categories, semantically null forms, underspecified content and compositionality as a whole. (shrink)

In this paper, we investigate the possibility of translating a fragment of natural deduction system (NDS) for natural language semantics into modern type theory (MTT), originally suggested by Luo (2014). Our main goal will be to examine and translate the basic rules of NDS (namely, meta-rules, structural rules, identity rules, noun rules and rules for intersective and subsective adjectives) to MTT. Additionally, we will also consider some of their general features.

This paper introduces Richard Montague's theory of determiner phrases to the philosophically oriented readers who are familiar with Russell's traditional treatment. Determiner phrases include not only quantifier phrases in the narrow sense, such as every man, some woman, and nothing, but also DP conjunctions such as Adam and Betty and Adam or Betty, and even proper names such as Adam and Betty. Montague treats all determiner phrases as belonging to type t, i.e., the type of functions from properties of individuals (...) to truth values. This paper also introduces the simply typed lambda-calculus for the explication of Montague's theory. Two major problems with Montague's theory, one more philosophical and the other more linguistic, are discussed. (shrink)

Vector models of language are based on the contextual aspects of language, the distributions of words and how they co-occur in text. Truth conditional models focus on the logical aspects of language, compositional properties of words and how they compose to form sentences. In the truth conditional approach, the denotation of a sentence determines its truth conditions, which can be taken to be a truth value, a set of possible worlds, a context change potential, or similar. In the vector models, (...) the degree of co-occurrence of words in context determines how similar the meanings of words are. In this paper, we put these two models together and develop a vector semantics for language based on the simply typed lambda calculus models of natural language. We provide two types of vector semantics: a static one that uses techniques familiar from the truth conditional tradition and a dynamic one based on a form of dynamic interpretation inspired by Heim’s context change potentials. We show how the dynamic model can be applied to entailment between a corpus and a sentence and provide examples. (shrink)

I articulate and defend a necessary and sufficient condition for predication. The condition is that a term or term-occurrence stands in the relation of ascription to its designatum, ascription being a fundamental semantic relation that differs from reference. This view has dramatically different semantic consequences from its alternatives. After outlining the alternatives, I draw out these consequences and show how they favour the ascription view. I then develop the view and elicit a number of its virtues.

Category mistakes are sentences such as 'Green ideas sleep furiously' or 'Saturday is in bed'. They strike us as highly infelicitous but it is hard to explain precisely why this is so. Ofra Magidor explores four approaches to category mistakes in philosophy of language and linguistics, and develops and defends an original, presuppositional account.

We discuss a previously unnoticed resemblance between the theory of relations and predicates in The Philosophy of Logical Atomism [TPLA] by Russell and the theory of objects and names in the Tractatus Logico-Philosophicus [TLP] by Wittgenstein. Points of likeness are detected on three levels: ontology, syntax, and semantics. This analogy explains the prima facie similarities between the informal presentation of the theory of types in TPLA and the sections of the TLP devoted to this same topic. Eventually, we draw some (...) consequences concerning both sides of the analogy: for what concerns Russell, the contextual pertinence of this surprising fragment of Tractarian metaphysics and semantics is questioned on several grounds; about Wittgenstein, the interpreters who do not identify Tractarian objects with particulars are in a better position to make sense of the analogy here discovered. (shrink)

This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version of a (...) type theory, in which we show the embedding of the modal operators into standard group knowledge operators. (shrink)

The analysis of atomic sentences and their subatomic components poses a special problem for proof-theoretic approaches to natural language semantics, as it is far from clear how their semantics could be explained by means of proofs rather than denotations. The paper develops a proof-theoretic semantics for a fragment of English within a type-theoretical formalism that combines subatomic systems for natural deduction [20] with constructive (or Martin-Löf) type theory [8, 9] by stating rules for the formation, introduction, elimination and equality of (...) atomic propositions understood as types (or sets) of subatomic proof-objects. The formalism is extended with dependent types to admit an interpretation of non-atomic sentences. The paper concludes with applications to natural language including internally nested proper names, anaphoric pronouns, simple identity sentences, and intensional transitive verbs. (shrink)

The Generalized Quantifiers Theory, I will argue, in the second half of last Century has led to an important rapprochement, relevant both in logic and in linguistics, between logical quantification theories and the semantic analysis of quantification in natural languages. In this paper I concisely illustrate the formal aspects and the theoretical implications of this rapprochement.

This paper concerns two points of intersection between de se attitudes and the study of natural language: attitude ascription and communication. I first survey some recent work on the semantics of de se attitude ascriptions, with particular attention to ascriptions that are true only if the subject of the ascription has the appropriate de se attitude. I then examine – and attempt to solve – some problems concerning the role of de se attitudes in linguistic communication.

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)

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)

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.

We give a new characterization of the class of completely representable cylindric algebras of dimension 2 #lt; n w via special neat embeddings. We prove an independence result connecting cylindric algebra to Martin''s axiom. Finally we apply our results to finite-variable first order logic showing that Henkin and Orey''s omitting types theorem fails for L n, the first order logic restricted to the first n variables when 2 #lt; n#lt;w. L n has been recently (and quite extensively) studied as a (...) many-dimensional modal logic. (shrink)

This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs (...) of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification. (shrink)

The paradox of propositions, presented in Appendix B of Russell's The Principles of Mathematics (1903), is usually taken as Russell's principal motive, at the time, for moving from a simple to a ramified theory of types. I argue that this view is mistaken. A closer study of Russell's correspondence with Frege reveals that Russell carne to adopt a very different resolution of the paradox, calling into question not the simplicity of his early type theory but the simplicity of his early (...) theory of propositions. (shrink)

Crosslinguistically, causative constructions conform to the following generalization: If the causal relation is syntactically concealed, then it is semantically direct. Concealed causatives span a wide syntactic spectrum, ranging from resultative complements in English to causative subjects in Miskitu. A unified type-driven theory is proposed which attributes the understood causal relation—and other elements of constructional meaning—to type lifting operations predictably licensed by type mismatch at LF. The proposal has far-reaching theoretical implications not only for the theory of compositionality and causation, but (...) also for the underlying theory of events, space, and time, in natural language discourse. (shrink)

This book radically simplifies Montague Semantics and generalizes the theory by basing it on a partial higher order logic. The resulting theory is a synthesis of Montague Semantics and Situation Semantics. In the late sixties Richard Montague developed the revolutionary idea that we can understand the concept of meaning in ordinary languages much in the same way as we understand the semantics of logical languages. Unfortunately, however, he formalized his idea in an unnecessarily complex way - two outstanding researchers in (...) the field even compared his work to a `Rube Goldberg machine.' Muskens' work does away with such unnecessary complexities, obtains a streamlined version of the theory, shows how partialising the theory automatically provides us with the most central concepts of Situation Semantics, and offers a simple logical treatment of propositional attitude verbs, perception verbs and proper names. (shrink)

In this paper it is shown how the DRT (Discourse Representation Theory) treatment of temporal anaphora can be formalized within a version of Montague Semantics that is based on classical type logic.

In a lengthy review article, C. Anthony Anderson criticizes the approach to property theory developed in Quality and Concept (1982). That approach is first-order, type-free, and broadly Russellian. Anderson favors Alonzo Church’s higher-order, type-theoretic, broadly Fregean approach. His worries concern the way in which the theory of intensional entities is developed. It is shown that the worries can be handled within the approach developed in the book but they remain serious obstacles for the Church approach. The discussion focuses on: (1) (...) the fine-grained/coarse-grained distinction, (2) proper names and definite descriptions, (3) the paradox of analysis and Mates’ puzzle, and (4) the logical, semantical, and intentional paradoxes. (shrink)

Rooth & Partee (1982) and Rooth (1985) have shown that the English-specific rule-by-rule system of PTQ can be factored out into function application plus two transformations for resolving type mismatch (type lifting and variable binding). Building on these insights, this article proposes a universal system for type-driven translation, by adding two more innovations: local type determination for gaps (generalizing Montague 1973) and a set of semantic filters (extending Cooper 1983). This system, dubbed Cross-Linguistic Semantics (XLS), is shown to account for (...) various phenomena — including scope relations in English and Greenlandic Eskimo, internally headed relative clauses in Lakhota, serial verbs in Yoruba and VP ellipsis in English. (shrink)

In this paper it is shown how simple texts that can be parsed in a Lambek Categorial Grammar can also automatically be provided with a semantics in the form of a Discourse Representation Structure in the sense of Kamp [1981]. The assignment of meanings to texts uses the Curry-Howard-Van Benthem correspondence.

INTENSIONAL LOGIC §1. Natural Language and Intensional Logic When we speak of a theory of meaning for a natural language such as English, we have in mind an ...

This reissue, first published in 1971, provides a brief historical account of the Theory of Logical Types; and describes the problems that gave rise to it, its ...

I reject the contention that an important theoretical difference exists between formal and natural languages.

We present an approach to anaphora and ellipsis resolution in which pronouns and elided structures are interpreted by the dynamic identification in discourse of type constraints on their semantic representations. The content of these conditions is recovered in context from an antecedent expression. The constraints define separation types in Property Theory with Curry Typing, an expressive first-order logic with Curry typing that we have proposed as a formal framework for natural language semantics.

The paper presents Property Theory with Curry Typing (PTCT) where the language of terms and well-formed formulæ are joined by a language of types. In addition to supporting fine-grained intensionality, the basic theory is essentially first-order, so that implementations using the theory can apply standard first-order theorem proving techniques. Some extensions to the type theory are discussed, type polymorphism, and enriching the system with sufficient number theory to account for quantifiers of proportion, such as “most.”.