A rule in the recursive clauses governing type formation in a higher order logic

Question

My question regards the theory of types, as augmented and formalised by Richard Montague.

On page 10 of Gallin's "Intensional and Higher order modal logic"

• https://www.elsevier.com/books/intensional-and-higher-order-modal-logic/gallin/978-0-7204-0360-2 [1975]

Gallin formulates thus the set of types of $IL$, Montague's intensional logic:

$Types$. Let $e , t , s$ be any three objects, none of which is an ordered pair. The set of types of $IL$ is the smallest set $T$ satisfying:

$(i) \hspace{0.4cm} e \thinspace, \hspace{0.2cm} t \in T ,$

$(ii) \hspace{0.4cm} \alpha, \beta \in T$ imply $(\alpha,\beta) \in T ,$

$(iii) \hspace{0.4cm} \alpha \in T$ implies $(s,a) \in T .$

Gallin remarks that "objects of type $e$ will be possible entities or individuals, objects of type $t$ will he truth-values, objects of type $(\alpha,\beta)$ will be functions from objects of type $\alpha$ to objects of type $\beta$, and objects of type $(s,a)$ will be functions from indices to objects of type $\alpha$".

Why does Gallin say that $e, t, s$ can be "any three objects", given that he specifies what objects belonging to these types are (as individuals, truth values and indices). What is achieved by saying that $e, t, s$ can be any objects? Why must they not be ordered pairs, as he requires?

Answer 1

Types are not sets of the "objects" that have those types, they are effectively symbols and pieces of syntax to which we have a relation, the typing judgment, that associates "objects" to these symbolic expressions. We often think of types as codes that can be interpreted as sets or more generally objects of an appropriately structured category. That is, since types are just (inductively defined) pieces of syntax, it's straightforward to write a recursive function that maps types to sets or into categories.

The restriction on $e$, $t$, and $s$ to not be ordered pairs is just so that they aren't confused with the function types. This is mostly an artifact of the set-theoretic encoding of the structure of types. The formulation "the smallest set such that the following closure conditions hold" is a set-theoretic way of describing an inductively defined structure. Nowadays, most descriptions of type theory would use a notation more like: $$\alpha, \beta ::= \mathtt{e}\mid\mathtt{t}\mid \alpha\to\beta\mid\mathtt{s}\to\alpha$$ where $\mathtt{e}$, $\mathtt{t}$, and $\mathtt{s}$ are intended to be symbols and the types are generated from this expression like you would generate sentences from a context-free grammar. In programming languages/proof assistants, an inductive type declaration would be used, e.g. in Haskell:

data Types = Entities              
           | TruthValues           
           | Functions Types Types 
           | Indexed Types         

Here Entities, and TruthValues are just symbols and the whole type is essentially just a tree with either binary or unary branching nodes with leaves labelled by Entities or TruthValues.

There's really nothing gained by allowing $e$, $t$, and $s$ to be "any" objects. (Presumably, they are also intended to be distinct...) You could require them to be the numbers $0$, $1$, and $2$ say. The point is that the only thing we require of them is that they are distinguishable from each other and from ordered pairs so that we can tell which "case" in the inductive structure we're in.