Axiom of Infinity

The axiom of infinity asserts the existence of a Successor Set

We can then show that there’s a smallest successor set,
i.e. we can prove:

To prove it,
In a model, pick a successor set using (Inf).
Form the set

Since we can form .
It’s easy to check that is the smallest successor set,
which we denote by .

Every successor set contained in is i.e.

where is a shorthand for
for any formula

So inside we have true induction! We call this -induction
But still, from the outside there may be subsets of that are not sets in