Formal Semantics in Modern Type Theories

Appendix 1Simple Type Theory C

A1.1. Inference rules of C

The following are inference rules of Church’s simple type theory C, the extensional core of Montague’s IL, introduced and explained in section 1.3.1. The below inference rules were given in Luo and Soloviev (2017).¹

Rules for contexts, base types and λ-calculus:

Rules for truth of logical formulae:

Conversion rules for formulae’s truth:²

A1.2. Logical operators in C

In Church’s simple type theory C, logical operators can be defined by means of ⇒ and ∀ as follows, where in the definition of equality (the last line), a and b are of the same type A.

1. 1 The presentation of C in (Luo and Soloviev 2017) was based on (Luo 1990b) where, however, Church’s simple type theory was called HOL and presented by means of a formulae-as-types formulation.
2. 2 See footnote 10 on p.8 for the explanation of the β-conversion relation .