  Another, equivalent, coding structure for the first-order language of arithmetic is the structure[5] ⟨H(ω), ∈ ⨡  H(ω)⟩ of hereditarily finite sets, where a set x is hereditarily finite if x, its members, its members of members, etc., are all finite. This coding structure takes account of the fact that first-order formulas are naturally regarded as finite sets.