This theory introduces the primitive vocabulary for this variant of higher order logic. There are just three constants and three type constructors.

The definitions of logical constants in terms of the primitive (undefined) constants. The ones defined are those which are needed to state the axioms.

The five axioms for the primitive logic.

Miscellaneous low level definitions (local definitions, conditionals, unique existence) and theorems.

The theory of ordered pairs, including Curry and Uncurry.

The theory of Natural numbers.

The theory of lists.

The theory of characters (of which there are only 256).

No content, parent is char. This is the highest point at which a new theory can be attached.

The theory of sets.

No content, parents are sets, sum and one.

The theory of binary relations.

The theory of integers.

The theory of real numbers.

The theory of real numbers.