 Before proceeding, we need to introduce some terminology. \(\cQ_0\) is an alternative formulation of Church’s type theory which will be described in  Section 1.4  and is equivalent to the system described above using Axioms (1)–(8). A type symbol is propositional if the only symbols which occur in it are \({o}\) and parentheses.