A new "si" theory is created as a child of "hol" and an axiom of strong infinity is asserted of type IND. Probably

This is a place holder.

The new theory is first created, together with a proof context which we will build up as we develop the theory. This is hung off "hol", but in an ideal world the axiom would live much higher, replacing the usual axiom of infinity in theory "init".

xl-sml open_theory "hol"; force_new_theory "si"; force_new_pc "si"; merge_pcs ["xl_cs_∃_conv"] "si"; set_merge_pcs ["hol", "si"];

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 proto-set-theory, an alternative axiom mentioned but not asserted talks as if the individuals were proto-ordinals. 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.

xl-sml declare_infix (240, "∈i"); val strong_infinity_axiom = new_axiom (["strong_infinity_axiom"], ⌜ ∃$∈i: IND → IND → BOOL• ∀p• ∃q• (p ∈i q ∧ (∀x• x ∈i q ⇒ ( (∃y• y ∈i q ∧ ∀Z• ∃z• z ∈i y ∧ ∀v• v ∈i z ≡ v ∈i x ∧ (Z v)) ∧ (∀f•(∀u• u ∈i x ⇒ (f u) ∈i q) ⇒ ∃y• y ∈i q ∧ ∀u• u ∈i x ⇒(f u) ∈i y)))) ⌝);

The following is the ordinal version, which is noted but not asserted.

xl-gft declare_infix (240, "<o");

xl-gft new_axiom (["strong_infinity_axiom_o"], ⌜ ∃$<o•∀p•∃q• (p <o q ∧ (∀x• x <o q ⇒ ( (∃y $∈i• y <o q ∧ (∀Z• ∃u• u <o y ∧ (∀v• v <o x ⇒ (v ∈i u ≡ Z v)))) ∧ (∀G•(∀u• u <o x ⇒ (G u) <o q) ⇒ ∃y• y <o q ∧ ∀u• u <o x ⇒ (G u) <o y)))) ⌝);

The infinity axiom does not distinguish any element to serve as an empty set or as the ordinal zero. The obvious thing to do is to take some element which has no members, but the axiom does not guarantee that there is one. In fact, any element will do, so we define zero as follows:

xl-holconst ∅i : IND

T

xl-tex It is convenient also to have a name for one of the relationships whose existence is asserted by the axiom of infinity.

xl-sml val _ = xl_set_cs_∃_thm strong_infinity_axiom;

xl-holconst $∈i : IND → IND → BOOL

∀p• ∃q• (p ∈i q ∧ (∀x• x ∈i q ⇒ ( (∃y• y ∈i q ∧ ∀Z• ∃z• z ∈i y ∧ ∀v• v ∈i z ≡ v ∈i x ∧ (Z v)) ∧ (∀f•(∀u• u ∈i x ⇒ (f u) ∈i q) ⇒ ∃y• y ∈i q ∧ ∀u• u ∈i x ⇒(f u) ∈i y))))

And then we alias the names without the subscripts:

xl-sml declare_alias ("∅", ⌜∅i⌝); declare_alias ("∈", ⌜$∈i⌝);

Next we define a successor relation.

xl-holconst suci : IND → IND

∀or:IND• suci or = εor':IND• ∀x• x ∈ or ∨ x = or ≡ x ∈ or'

xl-sml declare_alias ("suc", ⌜suci⌝);