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

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

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

Автор: Stergios Chatzikyriakidis

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

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

Серия:

isbn: 9781119489214

isbn:

СКАЧАТЬ its set-theoretical interpretation from the semantics of IL in set theory (see, Henkin’s (1950) model). The intermediate language IL makes the task of semantic description easier and clearer. In fact, as Gallin (1975) shows, although IL only formulates the syntax of logical operators and gives their meanings semantically in set theory, an alternative system TY2 can be axiomatized as a variant of Church’s simple type theory (Church 1940), of which we shall give a presentation below and discuss its use in Montague semantics.4

      In MTTs, the correctness of typing judgments of the form a: A, stating that a is of type A, is decidable in the sense that we can mechanically decide whether such a judgment can be correctly made. For computer scientists, this is equivalent to saying that a computer system can automatically decide whether a is of type A. Thanks to this decidability result and because of the rich typing mechanisms in MTTs, the Curry–Howard principle of propositions-as-types (Curry and Feys 1958; Howard 1980) gives us an embedded logical mechanism for semantic interpretations – the second requirement above. In this book, we shall elaborate this in detail to illustrate how the logical mechanisms work and how the typing mechanisms facilitate semantic formalizations.

      This then gives the set-theoretical interpretation of (1.1), i.e. the interpretation of (1.2) in set theory (according to, for example, Henkin’s model interpretation), which says that the set-theoretic interpretation of j is a member of the set that interprets the predicate talk.

      Contexts and Judgments. A context is a sequence of entries either of the form x: A or of the form P true. Informally, the former assumes that the variable x be of type A and the latter that the proposition P be true. Only valid contexts are legal and context validity is governed by the following rules:

      where

is the empty sequence and FV (Γ) is the set of free variables in Γ, defined as: (1) FV (
) = ∅; (2) FV (Γ,x:A) = FV (Γ) ∪{x}; (3) FV (Γ,P true) = FV (Γ).

      Judgments are sentences of C, whose correctness is governed by the inference rules below. In C, there are four forms of judgments:

       – Γ valid, which means that Γ is a valid context СКАЧАТЬ