Theory of Definable Sets

This theory remind's me of Cantor's original definition of a "Menge" (i.e. "set") as a collection of "separate" entities. Here this captures this separateness by "definability"! Only definable sets [in the language of set theory] can be explicitly distinguished (thereby separated) from each other using the language of set theory. This theory blatantly express this. It appears to me that this principle is strong enough to capture most of ordinary mathematics in a formal manner! 

Lets introduce a new primitive one place predicate "Def" to signify "parameter free definable in the language of set theory". To capture that add an omega inference rule of definability to the underlying logic:

Definability ω-inference rule: if ϕ1,ϕ2,ϕ3,.... are all formulas in the language of set theory in which only x appear free [and only free], and if φ is a one place predicate symbol, then:

i=1,2,3,...;φ({x|ϕi})____________________

∀ Def y:φ(y)

Axiom schema of definability: if ϕ is a formula in the language of set theory in which only y occurs free, and only free; then:

Set axioms:

• 1. Extensionality: ∀z(z∈x↔z∈y)⟹x=y

  2. Comprehension: if ϕ is a formula in which x doesn't occur free, then all closures of the following are axioms:

  3. Foundation: ∃xϕ⟹∃x:ϕ∧∀y[ϕ(y)→y∉x];                             for any formula ϕ.

Now the above theory can easily prove closure of the realm of definable sets of definable sets under under adjunction and thereby closure of the definable naturals of definable naturals under succession. This can be proved without the need for foundation, so this theory minus foundation can interpret second order arithmetic! However by adding foundation we get infinity!!! Also this theory would prove closure of the world of definable sets of definable sets under both pairing and boolean union. To get rid of resorting to double definability levels mentioned above, it appears plausible to add an axiom of Membership: that is:

1. Membership: y∈x⟹Def(y)

However this theory cannot prove existence of full power sets, it can only assert existence of definable power sets, i.e. sets of all definable subsets of sets. So it appears that all elements it can prove the existence of are countable!

Important questions raised about this theory includes:

• 1. Can this theory prove the existence of an uncountable element?

  2. Is this theory equi-consistent with 3rdorder arithmetic?

See:

https://math.stackexchange.com/questions/3713806/is-definable-set-theory-equi-consistent-with-third-order-arithmetic