I believe a more standard approach is to say 0 := {} 1 := {{}} (= {0}) 2 := {{}, {{}}} (= {0, 1}) 3 := {{}, {{}}, {{}, {{}}}} (= {0, 1, 2}) n+1 := {0, 1, 2

I believe a more standard approach is to say 0 := {} 1 := {{}} (= {0}) 2 := {{}, {{}}} (= {0, 1}) 3 := {{}, {{}}, {{}, {{}}}} (= {0, 1, 2}) n+1 := {0, 1, 2, ... n} This has the advantage that the numbers are equal to the cardinality of the sets that define them. In the construction you gave (which I agree is conceptually easier), the cardinality of 1 is 0, and then the cardinality of every greater integer is 1. A cool feature of this version is x < y := x ∈ y