> 1. If P is a predicate of type 〈e<sup>n</sup>, t〉, and α[1], ... α<sub>n</sub> are terms of type e, then P(α[1], ... α<sub>n</sub>) is of type t.
> 2. If α and β are both of type e, then (α = β) and (α != β) are of type t.
> 3. If φ is of type t, then so is `-`φ.
> 4. If φ and ψ are of type t, then so are (φ `&` ψ), (φ `|` ψ), (φ `->` ψ) and (φ `<->` ψ).
> 5. If φ is of type t, and x is a variable of type e, then `exists x.`φ and `all x.`φ are of type t.