Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis
Чтение книги онлайн.

Читать онлайн книгу Formal Semantics in Modern Type Theories - Stergios Chatzikyriakidis страница 10

Название: Formal Semantics in Modern Type Theories

Автор: Stergios Chatzikyriakidis

Издательство: John Wiley & Sons Limited

Жанр: Языкознание

Серия:

isbn: 9781119489214

isbn:

СКАЧАТЬ we are going to discuss.

      In this section, some simple examples in formal semantics in modern type theories (MTT-semantics) are sketched for illustrations. Then, we shall describe the historical developments and some of the major merits for MTTs to be employed as foundational semantic languages.

       1.4.1. A glance at MTT-semantics

      In appearance, the MTT-interpretation (1.8) seems to be the same as the Montagovian interpretation (1.2). However, although similar, they have subtle differences, as summarized in Table 1.2.

      Table 1.2. Semantics of “John talks”

Type in MTT-semantics
j e Human
talk e → t HumanProp
talk(j) t Prop

      In particular, the typings of these interpretations are different:

       – In MTT-semantics, the sentence (1.7) is interpreted as the proposition talk(j) : Prop where Prop is the type of all logical propositions – an internal totality that only exists in impredicative type theories such as UTT.13

       – In MTT-semantics, talk(j) is a well-typed proposition because the semantics of “talk” is a predicate talk : Human → Prop, whose domain is the type Human, the collection of humans to which talk can be meaningfully applied and to which j belongs as well. Note that, different from Montague semantics, the domain of talk is Human, rather than the type e of all entities.14

      Table 1.3. Examples in MTT-semantics

Example MTT-semantics
CN man, human Man, Human : Type
IV talk talk : Human → Prop
ADJ handsome handsome : Man → Prop
ADVVP quickly quickly : ΠA:CN. (A → Prop) → (A → Prop)
Modified CN handsome man Σm : Man. handsome(m) : Type
Quantifier some some : ΠA:CN. (A → Prop) → Prop
S A man talks ∃m : Man. talk(m) : Prop

       – A common noun (CN) can be interpreted as a type and the interpretations of CNs form a universe called CN, the type of the types that interpret CNs.

       – A verb (IV) or an adjective (ADJ) can be interpreted as a predicate over a type D that interprets the domain of the verb or adjective, i.e. a function of type D → Prop.

       – A verb-modifying adverb (ADVVP) can be interpreted as a polymorphic function from predicates of type A → Prop to predicates of the same type, where A ranges over CNs in the universe CN.

       – Modified common nouns (modified CN), when the adjectives are intersective, can be interpreted by means of Σ-types of pairs.

       – A quantifier is interpreted as a polymorphic function that takes a type A that interprets a common noun and a predicate over A, and returns a proposition.

       – A sentence (S) can be interpreted as a proposition of type Prop.15

      Please note that the semantic interpretations in Table 1.3 are only indicative with typical examples. In some cases, there are further elaborations or completely different ways of interpretation. For example, although CNs modified by intersective adjectives can be interpreted by Σ-types, adjectival modifications by means of other classes of adjectives may better be interpreted with the help of other type constructors (see section 3.3).