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

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

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

Автор: Stergios Chatzikyriakidis

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

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

Серия:

isbn: 9781119489214

isbn:

СКАЧАТЬ proposition are the same); however, such an imposition is only OK for type theories that distinguish logical propositions from other types (as in UTT), not when they are identified (as in Martin-Löf’s type theory). With proof irrelevance in UTT, where both ordinary existential quantifier and Σ-types exist, a satisfactory semantics can be given to a sentence with both anaphora and counting.26 Such a solution is also available for predicative type theories as well: for example, as proposed and studied in Luo (2019b), we can employ MLTTh, an extension of Martin-Löf’s type theory with the h-logic studied by Voevodsky in the HoTT project (HoTT 2013), to obtain an adequate foundational semantic language, which accommodates both strong and weak quantifiers in a similar fashion.

       1.4.3. Merits of MTT-semantics

      We contend that, as foundational semantic languages, MTTs are advantageous and MTT-semantics has unique merits, as compared with simple type theory and Montagovian semantics. Here, we outline some of its merits, organized below into two respects, which are further elaborated in the following chapters (and related papers). Please note that this is in no way to cover all, or even most, attractive aspects of MTT-semantics and it only serves the purpose of highlighting some notable features, hopefully making it easier to understand the following pages of the book.

A, B
, in a traditional notation), there are many ways to form types including, for example, dependent types (e.g. Π-types and Σ-types), inductive types (e.g. types of numbers/lists/vectors/trees and disjoint union types), logical types for propositions (under the propositions-as-types principle) and type universes (types that contain types as objects).29 As we mentioned briefly earlier, the typing judgments of the form a : A, intuitively saying that a is an object of type A, are very different from the set-theoretical membership statements of the form sS: for example, the typing judgment a : A is mechanically decidable, while the membership relation sS (expressing that s satisfies predicate S) is a formula in the first-order logic and its truth is undecidable. Among other things, this decidability property is essential for any type theory to have a logic based on the propositions-as-types principle.