An intensional type theory: Motivation and cut-elimination (Q2732287)

Intensional type theory, ITT, has relevance to computer science and philosophy. The author cites an example in databases: the predicates Employee and MaleEmployee may have the same extension but certainly not the intension. He also cites the use/mention distinction: in `Yellow is a colour-word.' the predicate `Yellow' is mentioned and `colour word' is used. So these belong to different levels. ITT is designed to handle these. On the technical side, this paper is straightforward. ITT is formulated, its syntax and semantics are defined, and consistency and completeness theorems are proved. More in detail, the type structure is formulated in the predicate form. So starting from 1, the type of individuals, and [ ], the type of the truth values, the higher type \([\sigma,\dots,\tau]\) is assigned to predicates with arguments of types \(\sigma,\dots,\tau\). Due to use/mention, a term of higher type also has type 1, if its free variables are of type 1. (So, if a constant \(C\) is of type [1], \(C(C)\) is well-formed and of type [ ], i.e. a sentence.) An object of a model is an ordered pair of the intension and a possible extension of a formal term. Consequently, valuations become a bit complicated. Completeness is shown for a cut-free system in the manner of Takahashi-Prawitz. So, the cut-elimination theorem is a corollary. In an appendix, the author discusses uses of Russell's set.