Always a pleasure to see interesting ideas from those so dedicated to topics of interest to this forum. Are you open to suggestions and critique?
1. Does this contribute to any existing problem that has been identified regarding set theory or for that matter mathematical logic in general?
2. Can you formally define Hereditarily Finite Set i.e. without use of "etc." ?
3. Do you know of any rules that are not closed over those Hereditarily Finite Sets that provably exist in ZF?
On Saturday, November 21, 2015 at 1:59:13 PM UTC-5, Zuhair wrote:
> Here I'll post this principle in full, just in case the link won't work. A link to this full work is presented below:
> 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 stronge 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 Q+ would be called an elevated formula of Q if and only if Q+ is obtained from just replacing each occurrence of "HF" in Q 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 Q and Q+ as follows:
> Q is existentially equivalent to Q+ <-> for every subformula pi(y,x1,..,xn) of Q: Ax1 e HF,.., Axn e HF[Ey (pi(y,x1,..,xn))] <-> Ax1 e V,.., Axn e V [Ey (pi+(y,x1,..,xn))].
> Where n is the total number of parameters in pi.
> (notation: "A" denotes "for all", while "E" denotes "exists", and "e" denotes membership)
> In English every subformula pi of Q with all of its parameters being relativised to hereditarily finite sets must hold of an object if and only if its elevated form pi+ with all of its parameters being relativised to 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 "<-E->".
> 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 Q(y,x1,..,xn) is a formula in which only y,x1,..,xn occur free, then:
> (Q <-E-> Q+) & (Ax1 e HF .. Axn e HF [Ay (Q(y,x1,..,xn) -> y e HF)]) -> (Ax1 e V .. Axn e V [Ay (Q+(y,x1,..,xn) -> y e 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".
> To run an example of this method lets try to prove Singletons.
> So here we take Q(y,x) to be
> Az (z e 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 subformas are their elevated
> Now we check the subformula z=x
> first take x to be the paramter and check whether
> Ax e HF Ez (z=x) <-> Ax e V Ez (z=x)
> which is true.
> Now take z to be the paramter and check whether
> Az e HF Ex (z=x) <-> Az e V Ex (z=x)
> Which is true.
> Now we check the subformula z e y:
> Az e HF Ey (z e y) <-> Az e V Ey (z e y)
> Ay e HF Ez (z e y) <-> Ay e V Ez (z e y)
> which are true.
> Now we check the formula z e y <-> z=x:
> Az,x e HF Ey (z e y <-> z=x) <-> Az,x e V Ey (z e y <->z=x)
> Az,y e HF Ex (z e y <-> z=x) <-> Az,y e V Ex (z e y <->z=x)
> Ay,x e HF Ez (z e y <-> z=x) <-> Ay,x e V Ez (z e y <->z=x)
> which are true.
> At last we need to check the formula: Az (z e y <-> z=x) itself:
> Ax e HF Ey (Az (z e y <-> z=x)) <-> Ax e V Ey (Az(z e y <-> z=x))
> Ay e HF Ex (Az (z e y <-> z=x)) <-> Ay e V Ex (Az(z e y <-> z=x))
> which are true.
> So Q is existentially equivalent to its elevated form.
> So we can apply the generalization principle, and since we have:
> Q <-E-> Q+ & Ax e HF: Ay [Az(z e y <-> z=x) -> y e HF]
> then it follows
> Ax e V Ay [Az(z e y <-> z=x) -> y e V]
> which is Singletons!
> Another example is to prove Separation:
> So Q would be the formula Az (z e y -> z e x)
> The checks are:
> Az e HF Ex (z e x) <-> Az e V Ex (z e x)
> Ax e HF Ez (z e x) <-> Ax e V Ez (z e x)
> Same checks would apply to z e y
> Az,y e HF Ex (z e y -> z e x) <-> Az,y e V Ex (z e y -> z e x)
> Az,x e HF Ey (z e y -> z e x) <-> Az,x e V Ey (z e y -> z e x)
> Ax,y e HF Ez (z e y -> z e x) <-> Ax,y e V Ez (z e y -> z e x)
> And at last:
> Ax e HF Ey Az (z e y -> z e x) <-> Ax e V Ey Az (z e y -> z e x)
> Ay e HF Ex Az (z e y -> z e x) <-> Ay e V Ex Az (z e y -> z e x)
> Clearly all above checks hold. And since we have:
> Q <-E-> Q+ & Ax e HF: Ay [Az(z e y -> z e x) -> y e HF]
> Then by Generalization principle it would follow that:
> Ax e V: Ay [Az(z e y -> z e x) -> y e V]
> Which is Separation.
> For clearer veiw see: