The idea is, to make HOL stronger so that more things, in particular so that quite strong set theories, can be developed in
HOL by conservative extension.
This is intended to allow me to assert just one axiom of strong infinity and then use definitions for working with foundational
systems rather than axiomatising each foundational system.
It is intended to enable the replacement of the axiomatic development for "GST" for example, with a convervative development.
This is done by instead of (though in fact it is as well as) asserting that there are infinitely many individuals, we assert
that the cardinality of the individuals is at least as large as the smallest cardinal which is greater than infinitely many
inacessible cardinals, or by a similar kind of effect in terms of ordinals.
The axiom asserted talks as if the individuals were a kind of protosettheory, an alternative axiom mentioned but not asserted
talks as if the individuals were protoordinals.
The "proto" but means that they have no properties which are not essential to being able to state that there are sufficiently
many of them (e.g. there is no mention of extensionality), and also that there may also be lots of other individuals of wholly
mysterious character.
The idea is to get expression of cardinality down to its simplest form.
The following is the ordinal version, which is noted but not asserted.
xlgft
declare_infix (240, "<_{o}");
