Add axiomatic for cardinal function.
Add definition of set induction.