  Quantification and implication are introduced, or rather versions appropriate for the various types are introduced. \(\lambda\) abstraction notation is present. And finally, for each type \(\alpha\) it is assumed there is a relation that holds between a concept of something of type \(\alpha\) and the thing itself; this is a relation between members of type \(\alpha_{1}\) and members of type \(\alpha\). This is denoted \(\Delta\), with appropriate type-identifying subscripts.