The extensional well founded hereditarily finite set (abbreviated as hereditarily finite sets in the rest of this account) realm appears to be the most natural set realm, and so if we can figure out some way of generalizing some kinds of results from it to the whole realm of sets, then this might be of help in both understanding sets and possibly guides derivation of some strong set principles that have a natural look.
The naive idea is that some properties that are closed over the class of all hereditarily finite sets would also close over the class of all sets. We need to define a theory that helps us decide on some of these properties.
To tackle this I'll define a notion of "elevation" on formulas:
A formula ∅+ would be called an elevated formula of ∅ if and only if ∅+ is obtained from just replacing each occurrence of "HF" in ∅ by V, where HF is the symbol given to the class of all hereditarily finite sets, and V is the symbol denoting the class of all sets.
Now the development is to define a notion of "existential equivalence" between formulas ∅ and ∅+ as follows:
∅ is existentially equivalent to ∅+ ⇔ for every subformula ψ(y,x1 ,..,xn) of ∅:
∀x1∈ HF,.., ∀xn∈ HF[∃y ψ(y,x1 ,..,xn)] ⇔ ∀x1∈ V,.., ∀xn∈ V [∃y ψ+(y,x1 ,..,xn)].
Where n is the total number of parameters in ψ.
In English every subformula ψ of ∅ with all of its parameters being relativised to the class HF of all hereditarily finite sets must hold of an object if and only if its elevated form ψ+ with all of its parameters being relativised to the class V of all sets must hold of an object.
HF is defined as the union of the intersectional class of all power-inductive classes (classes containing the empty set among their elements, that are closed under existence of power sets).
I'll denote existential equivalence by "⇐∃⇒".
My holding assumption is that existentially equivalent formulas can generalize results from the hereditarily finite set realm to the whole realm of sets.
So to formally capture that, we write:
Principle of Generalization: for n=1,2,3,..; if ∅(y,x1 ,..,xn) is a formula in which only y,x1 ,..,xn occur free, then:
(∅ ⇐∃⇒ ∅+) ∨ (∀x1∈ HF .. ∀xn ∈ HF [∀y (∅(y,x1 ,..,xn) ⇒ y ∈ HF)])
⇒ (∀x1 ∈ V .. ∀xn ∈ V [∀y (∅+(y,x1 ,..,xn) ⇒ y ∈ V)])
is an axiom.
Now this principle when added to Extensionality, Impredicative class comprehension of MK, and an axiom of existence of a power-inductive class and an axiom of infinity, then the result is a theory that can interpret ZF over the realm of sets (members of classes) of it.
A nice corollary of this is that any formula using no more than three subformulas that is closed on the hereditarily finite set realm would also close on the whole realm of sets, and just using those formulas one can prove all axioms of Zermelo set theory "Z".
EXAMPLES:
To run an example of this method let's try to prove Singletons.
So here we take ∅(y,x) to be
∀z (z ∈ y ⇔ z=x)
Now for this case the formula is itself its elevated form since
it contains no HF symbol, and so all of its subformulas are their elevated
forms.
Now we check the subformula z=x
first take x to be the parameter and check whether
∀x ∈ HF ∃z (z=x) ⇔ ∀x ∈ V ∃z (z=x)
which is true.
Now take z to be the parameter and check whether
∀z ∈ HF ∃x (z=x) ⇔ ∀z ∈ V ∃x (z=x)
Which is true.
Now we check the subformula z ∈ y:
∀z ∈ HF ∃y (z ∈ y) ⇔ ∀z ∈ V ∃y (z ∈ y)
∀y ∈ HF ∃z (z ∈ y) ⇔ ∀y ∈ V ∃z (z ∈ y)
which are true.
Now we check the formula z ∈ y ⇔ z=x:
∀z,x ∈ HF ∃y (z ∈ y ⇔ z=x) ⇔ ∀z,x ∈ V ∃y (z ∈ y ⇔z=x)
∀z,y ∈ HF ∃x (z ∈ y ⇔ z=x) ⇔ ∀z,y ∈ V ∃x (z ∈ y ⇔z=x)
∀y,x ∈ HF ∃z (z ∈ y ⇔ z=x) ⇔ ∀y,x ∈ V ∃z (z ∈ y ⇔z=x).
which are true.
At last we need to check the formula: ∀z (z ∈ y ⇔ z=x) itself:
∀x ∈ HF ∃y (∀z (z ∈ y ⇔ z=x)) ⇔ ∀x ∈ V ∃y (∀z(z ∈ y ⇔ z=x))
∀y ∈ HF ∃x (∀z (z ∈ y ⇔ z=x)) ⇔ ∀y ∈ V ∃x (∀z(z ∈ y ⇔ z=x))
which are true.
So ∅ is existentially equivalent to its elevated form.
So we can apply the generalization principle, and since we have:
(∅ ⇐∃⇒ ∅+) ∨ ∀x ∈ HF: ∀y [∀z(z ∈ y ⇔ z=x) ⇒ y ∈ HF]
then it follows
∀x ∈ V: ∀y [∀z(z ∈ y ⇔ z=x) ⇒ y ∈ V]
which is Singletons!
Another example is to prove Separation:
So ∅ would be the formula ∀z (z ∈ y ⇒ z ∈ x)
The checks are:
∀z ∈ HF ∃x (z ∈ x) ⇔ ∀z ∈ V ∃x (z ∈ x)
∀x ∈ HF ∃z (z ∈ x) ⇔ ∀x ∈ V ∃z (z ∈ x)
Same checks would apply to z ∈ y
∀z,y ∈ HF ∃x (z ∈ y ⇒ z ∈ x) ⇔ ∀z,y ∈ V ∃x (z ∈ y ⇒ z ∈ x)
∀z,x ∈ HF ∃y (z ∈ y ⇒ z ∈ x) ⇔ ∀z,x ∈ V ∃y (z ∈ y ⇒ z ∈ x)
∀x,y ∈ HF ∃z (z ∈ y ⇒ z ∈ x) ⇔ ∀x,y ∈ V ∃z (z ∈ y ⇒ z ∈ x)
And at last:
∀x ∈ HF ∃y ∀z (z ∈ y ⇒ z ∈ x) ⇔ ∀x ∈ V ∃y ∀z (z ∈ y ⇒ z ∈ x)
∀y ∈ HF ∃x ∀z (z ∈ y ⇒ z ∈ x) ⇔ ∀y ∈ V ∃x ∀z (z ∈ y ⇒ z ∈ x)
Clearly all above checks hold. And since we have:
(∅ ⇐∃⇒ ∅+) ∨ ∀x ∈ HF: ∀y [∀z(z ∈ y ⇒ z ∈ x) ⇒ y ∈ HF]
Then by Generalization principle it would follow that:
∀x ∈ V: ∀y [∀z(z ∈ y ⇒ z ∈ x) ⇒ y ∈ V]
Which is Separation.
Zuhair Al-Johar
20/11/2015
ADDENDUM! The definition of existential equivalence is not correct, since the formula
∀z (z ∈ y ⇔ ∃u (u ∈ x1 ^ u is infinite ^ u ⊃ z)) would pass the above check
and this is obviously problematic.
CORRECTION: ∅ <=∃=> ∅+ ⇔ for every subformula ψ(y,x1 ,..,xn) of ∅ the followings are true:
∀x1∈ HF ... ∀xn∈ HF ∃y ψ(y,x1 ,..,xn) ⇔ ∀x1∈ V ... ∀xn∈ V ∃y ψ+(y,x1 ,..,xn)
∀x1∈ HF ... ∀xn∈ HF ~∃y ψ(y,x1 ,..,xn) ⇔ ∀x1∈ V ... ∀xn∈ V ~∃y ψ+(y,x1 ,..,xn)
All checks present in the above examples would hold for this definition. However
in order to reduce the size of checking it's better to fix the order of quantification over variables
in each tested subformula ψ to be the same as the order of quantification over them in ∅.
A possible simplification of the above method is to just demand existential equivalence between a formula and itself in the generalization principle, so this would be:
Define: ∅ <=∃=> ∅ ⇔ for every subformula ψ(y,x1 ,..,xn) of ∅ the followings are true:
∀x1∈ HF ... ∀xn∈ HF ∃y ψ(y,x1 ,..,xn) ⇒ ∀x1∈ V ... ∀xn∈ V ∃y ψ(y,x1 ,..,xn)
∀x1∈ HF ... ∀xn∈ HF ~∃y ψ(y,x1 ,..,xn) ⇒ ∀x1∈ V ... ∀xn∈ V ~∃y ψ(y,x1 ,..,xn)
And then we substitute ∅ <=∃=> ∅ in the generalization principle instead of ∅ <=∃=> ∅+.
I'd conjecture that the resulting theory would interpret ZF.
See subpage: Naive Explanation for some informal account on this method
Zuhair Al-Johar
December 4, 2015