This posting is an attempt to clarify and further extend the method exposited at the posting present at:
I think it is more appropriate to present it at a separate post rather than modifying it there, since this would disturb the flow of the ideas that actually occurred there.
The basic idea is to define a class\set theory where rules governing sets are rules transferred from the hereditarily finite set realm of that theory, and then extend that principle itself to come from the hereditarily countable set realm, and so on...
So the core idea is the "Transfer Principles".
I just want to note that this idea is not new with me, it has been investigated long before by Harvey Friedman, see the links in his posting:
https://cs.nyu.edu/pipermail/fom/2016-August/020042.html
Although there is a difference between what I'm presenting here, however the general direction is the same.
I'll present here a formal line of capturing this principle. We'll work in an axiomatic class theory that extends first order logic with identity and membership, so to emphasize here: this theory is a FIRST order class theory, it only contains identity == and membership ∈∈ as its sole extra-logical primitives, and the language is MONO-SORTED, so the language of this theory is exactly the same language as that of Zermelo Frankle set theory.
We define the predicate "set" as:
Definition: set(x)⟺∃y(x∈y)set(x)⟺∃y(x∈y)
The axioms are the first order identity axioms, plus:
Extensionality: ∀a,b(∀x(x∈a↔x∈b)→a=b)∀a,b(∀x(x∈a↔x∈b)→a=b)
Class comprehension schema: if ϕ(y,x1,..,xn)ϕ(y,x1,..,xn) is a formula in which only y,x1,..,xny,x1,..,xn occur free, and all of those only occur free, then:
Define: x=V⟺∀y (set(y)→y∈x)x=V⟺∀y (set(y)→y∈x)
Empty set: ∃x∈V ∀y(y∉x)∃x∈V ∀y(y∉x)
Singletons: ∀a∈V ∃x∈V ∀y(y∈x↔y=a)∀a∈V ∃x∈V ∀y(y∈x↔y=a)
Boolean union: ∀a,b∈V ∃x∈V ∀y(y∈x↔y∈a∨y∈b)∀a,b∈V ∃x∈V ∀y(y∈x↔y∈a∨y∈b)
Define: finite(a)⟺∀k[∃m(m∈k)∧∀x,y,z(x∈a∧y∈k∧z∈k→∀u(∀n(n∈u→n=x∨n∈y∨n∈z)→u∈k))→a∈k]finite(a)⟺∀k[∃m(m∈k)∧∀x,y,z(x∈a∧y∈k∧z∈k→∀u(∀n(n∈u→n=x∨n∈y∨n∈z)→u∈k))→a∈k]
This will burn down to saying that: aa is finite if and only if it is an element of every class kk that has the empty set among its elements, that is closed under Boolean union, that has the singletons of all elements of aa among its elements.
Now this defining formula only contains 10 occurrences of atomic sub-formulas, and it is taken here to be the shortest expression defining finiteness in this theory. The length of a formula is meant to be of a formula that is written only using the customary four logical connectives as logical constants, and using the two customary quantifier symbols as logical primitive symbols, and of course the formula must not use any defined symbol.
Pure finite set world: ∀x(x is hereditarily finite →set(x))∀x(x is hereditarily finite →set(x))
Where "x is hereditarily finite" is defined as: x is finite and every element of the transitive closure of x is finite.
We shall denote the class of all hereditarily fintie sets by HFHF
Infinity: HF∈VHF∈V
Now the above axioms are the base theory and to it the transfer principles are to be added. It is important to note the axiom of FOUNDATION is NOT an axiom of this theory.
Now the first transfer principle is the "ternary" transfer principle which is:
The principle of ternary Transfer from the pure finite set world: if ϕ(y,x)ϕ(y,x) is a formula having no more than three occurrences of atomic formulas in it, in which only symbols ‘‘y,x"‘‘y,x"occur free, and those only occur free, then:
∀x∈HF [∀y(ϕ(y,x)→y∈HF)]→∀x∈V[∀y(ϕ(y,x)→y∈V)]∀x∈HF [∀y(ϕ(y,x)→y∈HF)]→∀x∈V[∀y(ϕ(y,x)→y∈V)]
I think this principle can be proved to be a theorem of MKMK class theory, and that it is consistent relative to ZFCZFC. Now this principle is strong enough to prove the consistency of Zermelo set theory!
The idea is that a formula composed of at most 3 atomic formulas is too small to mention the notion of "finiteness" whether in a direct or an indirect manner, so we can transfer it to sets beyond the pure finite set world, and here we actually generalize it over all 'sets' of that theory [but not over all classes!].
Now if we take as a criterion "the length of a formula being strictly shorter than the length of the shortest expression defining finiteness" to be an indicator of the inability of that formula to mention finiteness even at an indirect implicit level, then to outspeak this principle we'd state it as:
8'. The principle of Transfer from the pure finite world: if ϕ(y,x)ϕ(y,x) is a formula shorter than any formula defining finiteness, in which only symbols ‘‘y,x"‘‘y,x" occur free, and those only occur free, then:
∀x∈HF [∀y(ϕ(y,x)→y∈HF)]→∀x∈V[∀y(ϕ(y,x)→y∈V)]∀x∈HF [∀y(ϕ(y,x)→y∈HF)]→∀x∈V[∀y(ϕ(y,x)→y∈V)]
However replacement is not provable by this principle, now to modify this principle as to prove replacement we may try re-stating it relative only to subsets of HF, as follows:
8".The principle of Transfer from proximity of the pure finite world: if ϕ(y,x)ϕ(y,x) is a formula shorter than any formula defining finiteness, in which only symbols ‘‘y,x"‘‘y,x" occur free, and those only occur free, then:
∀x∈HF [∀y⊆HF(ϕ(y,x)→y∈HF)]→∀x∈V[∀y (ϕ(y,x)→y∈V)]∀x∈HF [∀y⊆HF(ϕ(y,x)→y∈HF)]→∀x∈V[∀y (ϕ(y,x)→y∈V)]
However this also fails to prove replacement over sets! we see that the shortest formula to prove replacement is:
∃F[∀m(m∈F→∃a,b(a∈A∧b∈B∧a∈m∧b∈m))∧∀m,n(m∈F∧n∈F∧∃k(k∈m∧k∈n)→n=m)∧∀b(b∈B→∃m(m∈F∧b∈m))]∃F[∀m(m∈F→∃a,b(a∈A∧b∈B∧a∈m∧b∈m))∧∀m,n(m∈F∧n∈F∧∃k(k∈m∧k∈n)→n=m)∧∀b(b∈B→∃m(m∈F∧b∈m))]
Which entails that B has 1-1 relation with a subset of A, now this formula uses 13 occurrences of atomic subformulas, and so it is strictly longer than the shortest formula defining finiteness. So it cannot be used in any of the transfer principles given above.
It needs to be addressed that FOUNDATION is hostile to this method, for if we axiomatize it, then the shortest formula defining "finite(a)" would be:
having 6 occurrences of atomic subformulas, while the following formula (originally presented by Joel David Hamkins) comprised of just 5 atomic subformulas would be enough to violate the transfer principle:
That occurred because Foundation itself seeps a lot of information about finiteness into the buildup of sets, so it would act in a subtle manner to indirectly mention finiteness which should be avoided in this method. However it is to be noted that this won't touch the ternary transfer principle, so we can have Foundation without any problem! Also the argument about foundation won't affect the method presented here, since Foundation is not axiomatized, and this method can interpret theories that can have fragments of them being consistent with Foundation, so it is not that big deal after all.
Now in this posting I'll consider more the idea of extending the transfer principles themselves to come not just from the herediarily finite set world, but rather to extend it to come from the herediarily countable world, and even from any herediarily subnumerous to ℶiℶi world. So instead of "finiteness" we use "subnumerous to ℶiℶi", and carry on the same process. For example for countable transfer, the principle would look like:
The principle of Transfer from proximity of the pure countable world: if ϕ(y,x)ϕ(y,x) is a formula shorter than any formula defining countability, in which only symbols ‘‘y,x"‘‘y,x" occur free, and those only occur free, then:
∀x∈HC [∀y⊆HC(ϕ(y,x)→y∈HC)]→∀x∈V[∀y (ϕ(y,x)→y∈V)]∀x∈HC [∀y⊆HC(ϕ(y,x)→y∈HC)]→∀x∈V[∀y (ϕ(y,x)→y∈V)]
where HCHC is the "set" of all hereditarily countable sets.
I think the shortest expression defining "countable class" is of being in 1-1 relation with a set of zermelo naturals. The formulas are:
natural(a)⟺∀k(∃m(m∈k)∧∀a(a∈k→∀b(∀n(n∈b→n=a)→b∈k))→a∈k)natural(a)⟺∀k(∃m(m∈k)∧∀a(a∈k→∀b(∀n(n∈b→n=a)→b∈k))→a∈k)
countable(x)⟺∃y(∀m(m∈y→countable(m))∧x subnumerous to y)countable(x)⟺∃y(∀m(m∈y→countable(m))∧x subnumerous to y)
but the shortest expression of x subnumerous to yx subnumerous to y is already the formula of the shortest expression of Replacement! which would contain the above mentioned 13 atomic subformulas, so the total formula defining countability would always be bigger than the formula defining replacement (here it is 20 atomic subformula versus 13), and by then Replacement over sets would be a theorem of the theory with this extended form of the transfer principle, because the 13 atomic subformula formula mentioned above would generalize over the whole set world.
The basic idea is that the extended transfer principles would allow for longer and longer formulas to be included among the rules governing sets in this theory, and by then we can have virtually no limit to the length of the transfer formulas, this will tremendously boost the transfer concept, as to allow stronger and stronger transfers from initial subsets of the theory to the whole theory.
So the base theory plus the ternary transfer principle + the countable transfer principle, would interpret the whole of ZFCZFC.
I personally think that the hereditarily finite set world and the hereditarily countable set world are the ones we have the strongest intuitive grasps about, and so defining a set theory whose rules are transfers from those two sub-worlds would be in some sense highly motivated from the intuitive perspective. And to me if there is no clear inconsistency involved with the above, then this would in some sense boost the consistency of ZFCZFC.
The main questions are:
Can that be done?
What would be the power of it in terms of extending the customary set theory ZFCZFC?
Are there known arguments against the general line of these transfer principles and the line of extending them to higher cardinalities?
Another more recent posting is:
This posting is an attempt to raise some technical corrections and further extend the method exposited at the posting present at
The core idea is the "Transfer Principles".
I just want to note that this idea is not new with me, it has been investigated long before by Harvey Friedman, see the links in his posting:
https://cs.nyu.edu/pipermail/fom/2016-August/020042.html
Although there is a difference between what I'm presenting here, however the general direction is the same.
First I'll present the corrected abbreviated background, and then raise the technical and conceptual questions below.
FORMAL BACKGROUND:
I'll present here a formal line of capturing this principle. We'll work in an axiomatic class theory that extends first order logic with identity and membership, so to emphasize here: this theory is a FIRST order class theory, it only contains identity == and membership ∈∈ as its sole extra-logical primitives, and the language is MONO-SORTED, so the language of this theory is exactly the same language as that of Zermelo Frankle set theory.
We define the predicate "set" as:
Definition: set(x)⟺∃y(x∈y)set(x)⟺∃y(x∈y)
The axioms are the first order identity axioms, plus:
Extensionality: ∀a,b(∀x(x∈a↔x∈b)→a=b)∀a,b(∀x(x∈a↔x∈b)→a=b)
Class comprehension schema: if ϕ(y,x1,..,xn)ϕ(y,x1,..,xn) is a formula in which only y,x1,..,xny,x1,..,xn occur free, and all of those only occur free, then:
Define: x=V⟺∀y (set(y)→y∈x)x=V⟺∀y (set(y)→y∈x)
Empty set: ∃x∈V ∀y(y∉x)∃x∈V ∀y(y∉x)
Singletons: ∀a∈V ∃x∈V ∀y(y∈x↔y=a)∀a∈V ∃x∈V ∀y(y∈x↔y=a)
Boolean union: ∀a,b∈V ∃x∈V ∀y(y∈x↔y∈a∨y∈b)∀a,b∈V ∃x∈V ∀y(y∈x↔y∈a∨y∈b)
Define: any class aa is said to be finitefinite if and only if:
This will burn down to saying that: aa is finite if and only if it is an element of every class kk that has the empty set among its elements, that is closed under Boolean union, that has the singletons of all elements of aa among its elements.
Now this defining formula only contains 8 occurrences of atomic sub-formulas, and it is taken here to be the shortest expression defining finiteness in this theory. The length of a formula is meant to be of a formula that is written only using the customary four logical connectives as logical constants, and using the two customary quantifier symbols as logical primitive symbols, and of course the formula must not use any defined symbol.
Pure finite set world: ∀x(x is hereditarily finite →set(x))∀x(x is hereditarily finite →set(x))
Where "x is hereditarily finite" is defined as: x is finite and every element of the transitive closure of x is finite.
We shall denote the class of all hereditarily fintie sets by HFHF
Infinity: HF∈VHF∈V
Now the above axioms are the base theory and to it the transfer principles are to be added. It is important to note the axiom of FOUNDATION is NOT an axiom of this theory.
8.The principle of Transfer from proximity of the pure finite world: if ϕ(y,x)ϕ(y,x) is a formula shorter than any formula defining finiteness, in which only symbols ‘‘y,x"‘‘y,x" occur free, and those only occur free, then:
∀x∈HF [∀y⊆HF(ϕ(y,x)→y∈HF)]→∀x∈V[∀y (ϕ(y,x)→y∈V)]∀x∈HF [∀y⊆HF(ϕ(y,x)→y∈HF)]→∀x∈V[∀y (ϕ(y,x)→y∈V)]
Up till this point we can prove all axioms of Zermelo over sets of this world.
However this fails to prove replacement over sets! we see that the shortest formula to prove replacement is:
∃F[∀mn(m∈F∧n∈F→∃ab(a∈A∧b∈B∧a∈m∧b∈m∧∀r(r∈m→r=a∨r=b))∧[∃k(k∈m∧k∈n)→n=m])∧∀b(b∈B→∃p(p∈F∧b∈p))]∃F[∀mn(m∈F∧n∈F→∃ab(a∈A∧b∈B∧a∈m∧b∈m∧∀r(r∈m→r=a∨r=b))∧[∃k(k∈m∧k∈n)→n=m])∧∀b(b∈B→∃p(p∈F∧b∈p))]
Which entails that B has 1-1 relation with a subset of A, now this formula uses 15 occurrences of atomic subformulas, and so it is strictly longer than the shortest formula defining finiteness. So it cannot be used in the above transfer principle.
The principle of Transfer from proximity of the pure countable world: if ϕ(y,x)ϕ(y,x) is a formula shorter than any formula defining countability, in which only symbols ‘‘y,x"‘‘y,x" occur free, and those only occur free, then:
∀x∈HC [∀y⊆HC(ϕ(y,x)→y∈HC)]→∀x∈V[∀y (ϕ(y,x)→y∈V)]∀x∈HC [∀y⊆HC(ϕ(y,x)→y∈HC)]→∀x∈V[∀y (ϕ(y,x)→y∈V)]
where HCHC is the "set" of all hereditarily countable sets.
I think the shortest expression defining "countable class" is of being in 1-1 relation with a set of Zermelo naturals. The formulas are:
Define: kk is a set containing all naturals iff:
Define: x is countable iff:
but the shortest expression of x subnumerous to kx subnumerous to k is already the formula of the shortest expression of Replacement! which would contain the above mentioned 15 atomic subformulas, so the total formula defining countability would always be bigger than the formula defining replacement (here it is 20 atomic subformula versus 15), and by then Replacement over sets would be a theorem of the theory with this extended form of the transfer principle, because the 15 atomic subformula formula mentioned above would generalize over the whole set world.
The basic idea is that the extended transfer principles would allow for longer and longer formulas to be included among the rules governing sets in this theory, and by then we can have virtually no limit to the length of the transfer formulas, this will tremendously boost the transfer concept, as to allow stronger and stronger transfers from initial subsets of the theory to the whole theory. /
QUESTIONS:
Now that was the background which the following technical and conceptual questions are meant to be raised about.
How we make sure that the formula defining finiteness present here is the SHORTEST possible formula defining finiteness, given the axioms of this theory and the language specifications mentioned above?
I mean can we check for that using computer programs, or is it the case that we can be fairely content with the assumption that no formula can define finiteness and contain for example less than half occurrences of atomic formulas contained in that formula, so for this case we can say that no formula containing less than four atomic subformulas can express finitenss given the above conditions? and by then we can explicitly mention that a formula need at most 3 occurrences of atomic subformulas to be used in the transfer principle from the pure finite world? would this approach be reasonable? I mean as far as the sake of not mentioning finiteness is concerned.
Do anyone know of a formula defining finiteness (in the language of this theory with these axioms) that can contain less number of atomic subformulas than 8?
Same as the above question but for the case of shortest formula defining "countability", is there a shorter approach to define "x is a countable class" than defining it as being injective to the intersectional class of all classes containing all Zermelo naturals? or in general by being of the same size of a class of naturals? if that size approach proves to be the shortest, then replacement over sets would immediately be a theorem.
Since the shortest formula defining countability seems to be longer than that defining finiteness, is there a way to decide on the shortest number of occurrences of atomic subformulas that a formula need in order to define countability? [given axioms and langauge specifications of this theory]. Can that be done by brute force, I mean by computer? or it would be more plausible to try that ourselves, and then assume that the shortest formula defining countability cannot contain half of the atomic subformulas in the formula we've reached, and then use that half value in the transfer principle from the pure countable world much as it the case with the above definition of finiteness example?
The intuitive underlying idea of this approach is to concur the infinite set world in a step-wise comprehension rule manner, by transferring rules from prior stages, to overall sets, then from the next stage, to overall sets, etc.. this is a step-wise comprehension process, rather than by the known step-wise structural manner that governs set construction into a cumulative hierarchy, like that of Von Neumann's VV, or of Godel's LL. Joel David Hamkins had raised the point that the transfer method presented here is fraud and not reflecting a robust foundational principle. There is a step-wise process made here, though more difficult to attain if we go up stages because of difficulty in verifying the shortest definition principle when formulas get long, but I think it can be reasonably done for the initial stages and it might result in defining extensions to set theory???
ANOTHER POSTING IS THIS
The Generalized Transfer principle: for n=1,2,3,...n=1,2,3,...; m=1,2,3,...m=1,2,3,...; if {ϕn1(y),..,ϕnm(y)}{ϕ1n(y),..,ϕmn(y)}is the set of ALL formulas of atomic length ≤n≤n in which only the symbol ‘‘y"‘‘y" occur free, and only free, and if ψn(y,x)ψn(y,x) is a formula of atomic length ≤n≤n in which both and only symbols ‘‘y,x"‘‘y,x"occur free, and only free, then:
∀α[α∈ω0∧¬[∀y (ϕn1(y)↔y∈Hℵα) ∨...∨ ∀y(ϕnm(y)↔y∈Hℵα)]∧∀x∈Hℵα(∀y⊆Hℵα[ψn(y,x)→y∈Hℵα])→∀x∈V(∀y [ψn(y,x)→y∈V])],∀α[α∈ω0∧¬[∀y (ϕ1n(y)↔y∈Hℵα) ∨...∨ ∀y(ϕmn(y)↔y∈Hℵα)]∧∀x∈Hℵα(∀y⊆Hℵα[ψn(y,x)→y∈Hℵα])→∀x∈V(∀y [ψn(y,x)→y∈V])],
is an axiom.
Where HℵαHℵα is the class of all sets that are hereditarily strictly subnumerous to ℵαℵα.
In English: for every natural αα, any property that cannot define "x is strictly subnumerous to ℵαℵα", that is closed over the hereditarily strictly subnumerous to ℵαℵα world (i.e. closed on HℵαHℵα), then that property is closed on the class VV of all sets.
The "closure" property is restricted to subsets of the respective HℵαHℵα, so it means that all such subsets yy fulfilling ψ(y,x)ψ(y,x) would be elements of HℵαHℵα for every element xx of HℵαHℵα. The "inability to define" strict subnumerousity to ℵαℵα, is taken here to mean that ψ(y,x)ψ(y,x) is shorter than any formula that can define that subnumerousity.
Now this principle when added to the following fragment of Morese-Kelley class theoryMorese-Kelley class theory sufficient to prove the existence of the set Hℵ0Hℵ0, then it would prove all axioms of ZFC−Reg.ZFC−Reg.
Language: first order logic
Primitives: equality ‘‘="‘‘=", membership ‘‘∈"‘‘∈"
Define: set(x)⟺∃y (x∈y)set(x)⟺∃y (x∈y)
Axioms: ID axioms +
Extensionality: ∀x,y[∀z(z∈x↔z∈y)→x=y]∀x,y[∀z(z∈x↔z∈y)→x=y]
Class comprehension scheme: if ϕϕ is a formula in which x is not free, then all closures of [∃x∀y(y∈x↔set(y)∧ϕ)][∃x∀y(y∈x↔set(y)∧ϕ)] are axioms.
Define (VV): x=V⟺∀y[set(y)→y∈x]x=V⟺∀y[set(y)→y∈x]
Define (finitefinite): finite(x)⟺¬∃y [x∈y ∧ ∀a∈y ∃b∈y b ⊊a]finite(x)⟺¬∃y [x∈y ∧ ∀a∈y ∃b∈y b ⊊a]
Define (HFHF): HF(y)⟺∃x[y∈x∧ ∀a,b(a∈x∧b∈a→finite(a)∧b∈x)]HF(y)⟺∃x[y∈x∧ ∀a,b(a∈x∧b∈a→finite(a)∧b∈x)]
Infinity: ∀x[∀y∈x(HF(y))→x∈V]∀x[∀y∈x(HF(y))→x∈V]
4. pairing: for all ain V ,b in Vfor all x for all y (y in x -> y=a or y=b) -> x in V
5. the closure transfer principle which is outlined below
Now this theory is effectively generated, since the class of all formulas up to a specific length is decidable; it proves all axioms of ZFC-RegularityZFC-Regularity, including CHOICE! Though the antecedent of the transfer schema is very extensive, yet still one can manage to derive theorems concerning properties that are invariant under this principle, like the property of being subnumerous to a class, this takes a fixed number of atomic formulas, and is invariant under that principle, i.e. whatever is the value of αα in the schema, the last condition of the antecedent of the schema would ALWAYS hold for that property! Now the prior condition of the antecedent must be satisfied for some formula length nn, then according to that principle it would generalize to all sets, this would be sufficient to prove both Replacement and Choice axioms over sets. That axioms of Z−Reg.Z−Reg. are provable over sets is trivial, take n=3n=3 and all axioms of pairing, union, power and separation would generalize to all sets, and this ternary transfer principle is most likely consistent! And so ZZ can indeed be visualized as a transfer from the Hereditarily finite realm to the beyond.
Now this principle had been deemed as ad-hoc by many commentators in MOMO, and indeed it DOESshed this appearance! now being so ad-hoc would it be expected to have an easy way of proving it inconsistent? and hence my next question:
IS there a clear counter-example to this principle?
This would clearly falsify this principle. Yet apart from that, is there a clear argument against this principle? other than just saying that it is ad-hoc, I mean what other parameters are present in the arsenal of foundation that goes against this principle and can knock it down, even before investigating its consistency?
The general concept of this principle had been investigated before [see links below], truly not in that exact form, but the form given here do abide by the general lines of that concept. Here I've presented a flagrant extension of it. So if it is ad-hoc then indeed it must be easy to figure out a counter-example to it.
Prior studies: https://cs.nyu.edu/pipermail/fom/2016-August/020042.html
http://www.cs.nyu.edu/pipermail/fom/2006-February/009997.htmlhttp://www.cs.nyu.edu/pipermail/fom/2006-February/010063.htmlhttp://www.cs.nyu.edu/pipermail/fom/2008-April/012800.htmlhttp://www.cs.nyu.edu/pipermail/fom/2008-April/012802.htmlhttp://www.cs.nyu.edu/pipermail/fom/2009-January/013343.html
ANOTHER POSTING TO MO:
Is the following closure transfer schema provable in MKM?
∀α(ordinal(α)∧α∈V→∀x∈Hℵα[∀y⊆Hℵα(ϕHℵα(x,y)→y∈Hℵα)])→∀x∈V ∀y[ϕV(x,y)→y∈V]
Where V is the class of all sets in MK; and Hℵαis the set of all sets hereditarily strictly subnumerous to ℵα; and ϕb means the formula ϕ with all of its quantifiers bounded by b, i.e., all of its quantifiers are of the form ∀x∈b;∃x∈b.
I think this might be the equivalent of the above in ZFC?
∀α(ordinal(α)→∀x∈Hℵα∃y∈Hℵα(ϕHℵα(x,y)))→∀x∃y(ϕ(x,y))
This is the posting that should have been written above:
Extensionality: ∀x,y(∀z(z∈x↔z∈y)→x=y)
Class comprehension schema: if ϕϕ is a formula in which x doesn't occur free, then (∃x∀y(y∈x↔∃z(y∈z)∧ϕ)) is an axiom.
Define (V): x=V⟺∀y(∃z(y∈z)→y∈x)
Pairing: ∀a,b∈V∃x∈V ∀y(y∈x↔y=a∨y=b)
Infinity: ∀x∈V[∀y∈x(y<<x)→x∈V]
Where "<<" signifies "hereditarily strictly subnumerous to", defined as:
Where "<" is "strictly subnumerous to" defined in the usual manner.
Closure schema: If ϕ(x,y) is a formula in which only symbols ‘‘x,y" appear free, and only appear free, then:
∀α(ordinal(α)∧α∈V→∀x∈Hℵα[∀y⊆Hℵα(ϕHℵα(x,y)→y∈Hℵα)])→
∀x∈V ∀y[ϕV(x,y)→y∈V]
Where HℵαHℵαis the set of all sets hereditarily strictly subnumerous to ℵαℵα; and ϕbϕb means the formula ϕwith all of its quantifiers bounded by b, i.e., all of its quantifiers are of the form ∀x∈b;∃x∈b
Of course we need an axiom to assert sex exists: \exists x \in V.
/ theory definition finished.
∀x[∃m(m∈x)∧∀y(y∈x→y∈a)→∃z(z∈x∧∀m(m∈x→z∉m))]∀x[∃m(m∈x)∧∀y(y∈x→y∈a)→∃z(z∈x∧∀m(m∈x→z∉m))]
∃m(m∈x)∧[∃z(z∈x∧∀m(m∈x→z∉m))→y∈x]∃m(m∈x)∧[∃z(z∈x∧∀m(m∈x→z∉m))→y∈x]
∃m(m∈k)∧∀a[a∈k→∀b(∀n(n∈b→n=a)→b∈k)]∃m(m∈k)∧∀a[a∈k→∀b(∀n(n∈b→n=a)→b∈k)]
∀k(k is a set containing all naturals →x subnumerous to k)∀k(k is a set containing all naturals →x subnumerous to k)
y<<x⟺∃z[y∈z∧∀a,b(a∈z∧b∈a→b∈z∧a<x)]
∀k[∃m(m∈k)∧∀x,y(x∈a∨y∈k→∀z(∀m(m∈z→m=x∨m∈y)→z∈k))→a∈k]∀k[∃m(m∈k)∧∀x,y(x∈a∨y∈k→∀z(∀m(m∈z→m=x∨m∈y)→z∈k))→a∈k]
∀x1,..,xn ∃x ∀y(y∈x↔set(y)∧phi(y,x1,...,xn))∀x1,..,xn ∃x ∀y(y∈x↔set(y)∧phi(y,x1,...,xn))
∀x1,..,xn ∃x ∀y(y∈x↔set(y)∧phi(y,x1,...,xn))∀x1,..,xn ∃x ∀y(y∈x↔set(y)∧phi(y,x1,...,xn))