The axiom of infinity

1. The natural numbers and induction

The axiom of foundation, combined with extensionality, pair set and sum set, tells us there is a definable operation of sets, s ( x ) = x x , called the successor operation which is 1-1 and does not contain 0 (i.e. ) in its range.

Definition.

A set x is inductive if 0 x and y x s ( y ) x .

An inductive set is therefore infinite.

Axiom of infinity: there is an inductive set, x ( 0 x y x s ( y ) x ) .

The axiom says there is one such inductive set, but in fact we can find a very special one, the least such.

Proposition.

If x , y are inductive then so is x y = { u x : u y } .

Proof.

Easy exercise.

Definition.

If x is a non-empty set, x denotes { u : y x ( u y ) } . This is easily seen to be a set by separation as for any z x we have x = { u z : y x ( u y ) } .

Definition.

Let x be inductive. The set ω is the set { u x : u   is inductive } . This is a set by power set and separation, and is independent of the choice of x by the previous proposition. We also see that ω is definable by a formula of L , u = ω holds if and only if x ( x   is inductive   u x ) .

Proposition.

ω is inductive.

Proof.

Easy exercise.

The simplicity of the results her bely their power. What we have done is to define a set ω = 0 s ( 0 ) s ( 1 ) and prove it is the least inductive set. (Be careful, as the is not precise and sets cannot be defined in this way except through special means such as those above.) What this is is in fact an induction principle, and ω is a copy of the natural numbers. To ephasise this we shall write 1 for s ( 0 ) , 2 for s ( 1 ) , 3 for s ( 2 ) , and so on.

Principle of induction on ω : If ϕ ( x ) is a first order L formula, possibly with parameters, and suppose ϕ ( 0 ) holds and also x ( ϕ ( x ) ϕ ( s ( x ) ) ) . Then x ω ϕ ( x ) .

Proof.

The set { x ω : ϕ ( x ) } exists by separation and is inductive by hypothesis. Hence it equals ω .

2. Examples of induction on the natural numbers

Proposition.

Every nonempty set x ω contains 0 .

Proof.

Induction on x .

Definition.

A set t is transitive if for all sets x , y we have x y t implies x t .

Proposition.

Every set x ω is transitive.

Proof.

Induction on x .

3. Recusion on the natural numbers

Going hand-in-hand with induction is recursion, also sometimes called inductive definitions. We need to explain and justify these.

Set theory has many notions of function. One is function as a definable first order formula. A formula ϕ ( x _ , y ) behaves like a function if x _ y ( ϕ ( x _ , y ) z ( ϕ ( x _ , z ) y = z ) ) . (This is usually abbreviated to x _ ∃! y ϕ ( x _ , y ) .) Sometimes this is true when restricted to x _ from a particular set or satisfying a partucular formula. Functions defined by formulas are called class functions.

The other kind of function is a function as a set.

Definition.

x , y is the set x x y .

This exists by the pair set axiom.

Proposition.

If x , y = x , y then x = x and y = y .

Proof.

Easy case-by-case argument.

Definition.

A set function is a set f such that every element of f is x , y for some sets x , y and x , y , z ( x , y f x , z f x = z ) . For such an f we write dom ( f ) for { u : v u , v f } and f ( u ) for the unique v such that u , v f when u dom ( f ) .

Theorem.

Suppose ϕ ( x , a _ ) and ψ ( x , y , z , a _ ) are first order formulas such that ∃! x ϕ ( x , a _ ) and x y ∃! z ψ ( x , y , z , a _ ) . Then there is a formula θ ( x , y , a _ ) such that x ω ∃! y θ ( x , y , a _ ) and

  • θ ( 0 , y , a _ ) ϕ ( y , a _ )
  • θ ( x , y , a _ ) ψ ( x , y , z , a _ ) θ ( s ( x ) , z , a _ )

This shows that we can define a function f ( x , a _ ) by f ( 0 , a _ ) = g ( a _ ) and f ( x + 1 , a _ ) = h ( x , f ( x , a _ ) , a _ ) . In the statement of this theorem we have used class functions, but set functions take part in the proof.

Proof.

We say a set-function f is an attempt if dom ( f ) is x x for some x ω such that

  • ϕ ( y , a _ ) f ( 0 ) = y
  • u dom ( f ) y z ( u x f ( u ) = y ψ ( u , y , z , a _ ) f ( s ( x ) ) = z )

Our formula θ ( x , y , a _ ) is the formula stating there is an attempt f with x dom ( f ) and y = f ( x ) .

The rest is an exercise. You need to prove by induction on ω that for all x ω attempts exist with x dom ( f ) and that any two attempts f , g agree on the values they give for f ( x ) , g ( x ) .