 The theorems of elementary type theory are those theorems which can be derived, using the rules of inference, from Axioms (1)–\((6^{\alpha})\) (for all type symbols \(\alpha)\). We shall sometimes refer to elementary type theory as \(\cT\). It embodies the logic of propositional connectives, quantifiers, and λ-conversion in the context of type theory.