A strong axiom of infinity for HOL
A strong axiom of infinity is asserted to enable conservative development of classical set theory and its metatheory, and other foundational work for which a strong metalanguage is convenient.
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.
A new "si" theory is created as a child of "hol" and an axiom of strong infinity is asserted of type IND. Probably
The Theory si
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".
open_theory "hol";
force_new_theory "si";
force_new_pc "si";
merge_pcs ["xl_cs_∃_conv"] "si";
set_merge_pcs ["hol", "si"];

Strong Infinity Axioms

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.

declare_infix (240, "∈i");
val strong_infinity_axiom = new_axiom (["strong_infinity_axiom"], ⌜
fttab∃$∈i: IND → IND → BOOL• ∀p• ∃q• (p ∈i q ∧ (∀x• x ∈i q ⇒ (
ftbr (∃y• y ∈i q ∧ ∀Z• ∃z• z ∈i y ∧ ∀v• v ∈i z ≡ v ∈i x ∧ (Z v))
ftbr ∧ (∀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.
declare_infix (240, "<o");

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

Representation of Ordinals
A subset of the individuals is defined to serve as ordinals.
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:
fttabi : IND

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

val _ = xl_set_cs_∃_thm strong_infinity_axiom;

fttab$∈i : IND → IND → BOOL
∀p• ∃q•
fttab(p ∈i q
fttab∧ (∀x• x ∈i q ⇒ (
fttabfttab(∃y• y ∈i q ∧ ∀Z• ∃z• z ∈i y ∧ ∀v• v ∈i z ≡ v ∈i x ∧ (Z v))
fttabfttab∧ (∀f•(∀u• u ∈i x ⇒ (f u) ∈i q)
fttabfttabfttab⇒ ∃y• y ∈i q
fttabfttabfttab∧ ∀u• u ∈i x ⇒(f u) ∈i y))))
And then we alias the names without the subscripts:
declare_alias ("∅", ⌜∅i⌝);
declare_alias ("∈", ⌜$∈i⌝);

Next we define a successor relation.
fttabsuci : IND → IND
fttab∀or:IND• suci or = εor':IND• ∀x• x ∈ or ∨ x = or ≡ x ∈ or'

declare_alias ("suc", ⌜suci⌝);

Proof Context
This is a place holder.
Proof Context

up quick index © RBJ

privacy policy


$Id: strong_infinity.xml,v 1.3 2008/04/15 18:21:36 rbj01 Exp $