Читать книгу Formal Semantics in Modern Type Theories - Stergios Chatzikyriakidis - Страница 14

Here, we sketch some simple examples of MTT-semantic interpretations, which give some ideas of what it is like, although a full-scale introduction to MTT-semantics (in Chapter 3) will not be possible until after the introduction to MTTs in Chapter 2. Let us start by considering the simple example (1.1), repeated here as (1.7), whose MTT-semantics is given in (1.8):

(1.7) John talks.

(1.8) talk(j)

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 Montague semantic	Type in MTT-semantics
j	e	Human
talk	e → t	Human → Prop
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.¹³

 – 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.¹⁴

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

MTT-semantic interpretations for various basic linguistic categories are exemplified in Table 1.3, where the natural language examples are the same as those in Table 1.1 for their Montague semantics. This makes it possible for a quick comparison in order for one to approach MTT-semantics more easily, albeit the understanding can be sketchy and imprecise at this stage. Here are brief explanations of the example interpretations in Table 1.3: some type-theoretical concepts are used without explanation, including polymorphism, Σ-type and universe which will only be introduced in Chapter 2.

 – 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.¹⁵

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).

A semantic interpretation may be refined. For instance, the semantics of the word “man” may be defined as a Σ-type (1.9). In other words, Man does not have to be a constant type; instead, in (1.9), it is defined by means of type Human and a predicate male : Human → Prop: a man is a human who is male.

(1.9) Man = Σx:Human.male(x)

Similarly, although we have only showed in Table 1.3 the semantic typing of “some”, generalized quantifiers can be defined in type theory (Sundholm 1989). In simple cases, they can be defined by existing quantifiers in type theory: for example, in UTT, some can be defined by means of the existential quantifier as shown in (1.10), where A : CN, P : A → Prop and ∃ is the existential quantifier (see section 2.3.1 and Appendix A3.2 for its definition).

(1.10) some(A, P) = ∃x:A.P (x)

The type of some as defined in (1.10) is that as shown in Table 1.3.