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

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

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

Автор: Stergios Chatzikyriakidis

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

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

Серия:

isbn: 9781119489214

isbn:

СКАЧАТЬ Γ ├ A type, which means that A is a type under context Γ;

       – Γ ├ a : A, which means that a is an object of type A under context Γ;

       – Γ ├ P true, which means that P is a true formula under context Γ.

      Inference rules. Besides the context validity rules given above, C has the following rules:

       – Assumption rules: one can prove what have been assumed in valid contexts.

       – Rules for function types: The formation rule (of function types), introduction rule (of λ-abstraction) and elimination rule (for applications) are as follows, where the terms in the forms of λ-abstractions and applications are related to each other computationally by the relation of β-conversion.10

       – Rules for logical formulae formed by implication and universal quantification: their formation, introduction and elimination rules.

      where, in the last rule, P (a) is obtained by substituting a for x in P (x).

      – Conversion rule for truth of formulas (see footnote 10 for the conversion relation ≈):

      Logical operators. The other usual logical operators can be defined by means of ⇒ and ∀. For example, the operators for conjunction and existential quantification can be defined as follows. Other operators such as disjunction and negation can be defined similarly (see Appendix A1.2).

      (1.3) P ∧ Q = ∀X : t. (P ⇒ Q ⇒ X) ⇒ X

      (1.4) ∃x : A.P (x) = ∀X : t. (∀x : A.(P (x) ⇒ X)) ⇒ X

      Table 1.1. Examples in Montague semantics

Montague semantics
CN man, human man, human : e → t
IV talk talk : e → t
ADJ handsome handsome : (e → t) → (e → t)
ADVVP quickly quickly : (e → t) → (e → t)
Modified CN handsome man handsome(man) : e → t
Quantifier some some : (e → t) → (e → t) → t
S A man talks x : e. man(x) & talk(x) : t

       1.3.2. Montague semantics: examples and intensionality

      A remark we should make is that, in type theories, typing judgments and logical formulas are different. In particular, a typing judgment is not a logical formula: (1.5) is a typing judgment stating that talk is of type et, while (1.6) is a logical formula of type t. With such examples, the difference seems to be apparent and there is no need to be emphasized. However, this becomes more important in the setting of modern type theories where much richer typing mechanisms are employed (see, for example, Chapter 2).

      A notational convention is adopted in this book: we shall use a different font to represent semantics of a natural language phrase. For instance, for the natural language words “man” and “talk”, we shall use man and talk for their semantics (as in Table 1.1).