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

Montague’s IL (Montague 1973; Gallin 1975) consists of an extensional core, which is Church’s simple type theory (Church 1940) (we call it C in this book, with C standing for “Church”), and a part concerning intensionality.⁷ We shall focus on describing the former and then briefly comment on the part about intensionality.

Our description of Church’s simple type theory C follows that by Luo and Soloviev (2017), where it is described by means of natural deduction rules that derive judgments – sentences in the type theory. For instance, a judgment may be of the form Γ ├ a: A, which means that a is of type A under the assumptions described in context Γ. We shall first explain what contexts and judgments are in C, and then describe its rules.⁸ (All of C’s inference rules are listed in Appendix A1.1.)

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 (the rules of deriving context validity are given above);

 – Γ ├ 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:

– Rules for base types: e and t are the types of entities and logical formulae, respectively.⁹

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

 – 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

	Example	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