NEW FOUNDATIONS "NF"

Although new foundations was born from the womb of typed theories, and proofs of known fragments of it do rely upon typed theories, yet still one can do them in a fragment of the natural set theories of Z or ZFC, but with non standards models of them. Boffa's proof of NFU is an example. Here I will demonstrate that we can try to prove a finite axiomatization of NF from 5 axioms all not using ordered pairs, and then try to prove that an extension of Z or ZF can interpret that system and then proof consistency of NFU, and I think in a similar manner we can prove consistency of NF.

The 5 axiom system for NF is:

Logicality: for every x,y the set x|y exists (where | is the sheffer stroke)

Singletons: for all x exists y: y={x}

Union: for all x exists y: y=U(x)

Composition: for all x,y exists a set

{{a,b}| exists c ({a,c} e x ^ {c,b} e y)}

Intersection: Exists x: x={{a,b} exists c e a (c e b)}

/ Theory definition finished.

(Also one can decompose composition into three axioms:

A. The unordered Cartesian product exists

B. Frege 1 exists.

C: For every set the set of all Set union except set intersection of its members exist.

 I.e. for every set S the set S* exists defined as:

S*= {y=U\I (x) | x in S}

were U\I (x) = U(x)\I(x)

where I(x) is intersection x.)

In reality there are many ways to substitute the long formula in composition by acyclic formulas. Suggested axioms are:

1. Sub_Cartesian product:

AA AB EX AY (Y in X <-> Ea in A Eb in B( for all Z (Z in Y -> Z in a \/ or Z in b)))

i.e. for every sets A,B there exists a set of all subsets of unions of an element from A and an element from B.

2. Frege 1 exists.

From these two axioms we can prove Cartesian products, and every finite Frege numeral n.

Most related to the unordered relative products of sets R,S of unordered pairs, is the result of having a set of cyclic triplets {a,b,c} that are elements of 3 and each of their members is an element of 2 and every subset of that triplet that is an element of 2 then it is an element of the intersection set.  We take a in R, b in S and c is y (if we want to preserve having 3 types) or y={c} (if we want to preserve predicativity).

so this is:

3. AK AR AS Ex Ay (y in x <->

Ep in 3 [Am in P (m in 2) ^

Aq C p (q in 2 -> q in K) ^

Er in R Es in S Az in p (z=r or z=s or z=y)]

Now the predicative form in 3 types is:

3. AK AR AS Ex Ay (y in x <-> E!i (i in y) ^

Ep in 3 [Am in P (m in 2) ^

Aq C p (q in 2 -> q in K) ^

Er in R Es in S Ei in y Az in p (z=r or z=s or z=i)]

 Actually one only need the two axioms of Subcatesian products and Frege 1, and Composition can be fully proved in that system. See the proof at the pdf titled "acycmin-shortproof" at the end of this page.

for an older version of the proof with composition in it see:

http://zaljohar.tripod.com/sfmin.pdf

The fragment of Z or ZF in which the above can be interpreted is:

Take a set V that serves as a model of Zermelo (usually refered to as Va, but here I'll just call it V).

1. An external INJECTION j from P(V)  to V

so if x=j(y) then x is called as the j code of y, also y is said to be j coded by x.

2. for every x,y such that x is the j code of y there is a set of all sets that are j coded by elements of y.

3. For every set x of un-ordered pairs of elements of V there is a set of all j codes of elements of x.

We call an unordered pair {a,b} as "intersectional pair" if and only if a and b share at least one element.

Now we call the pair {j(a),j(b)} as: the j-image of {a,b}

4. There exists a set of all j-images of intersectional pairs of subsets of V.

In notation: { {j(a),j(b)} | a C V & b C V & Exist c (c in a ^ c in b)} exists.

---------------------------------------

The following theory of ZF+coding can interpret the above theory:

Here is the full formal exposition of the theory I spoke about in the last approach of mine to prove consistency

of NF. IF this theory is proved to be consistent, then the consistency of NF would follow. I call it ZF + Coding because this is the main theme about it, that of external coding over ZF, I consider the consistency of this theory to be an interesting question on its own, that Con(NF) can be proved from proving its consistency is better be seen as a corollary rather than as the main result.

EXPOSITION

ZF + Coding: is the first order theory defined in the language of set theory, i.e. first order logic with equality and membership, added to it a binary relation "Cd", standing of "the code of", so Cd(x,y) is read as: y is the code of x; also it can be read as x is coded by y, with the following axioms:

Axioms:

[1] All of ZF axioms with the restriction of Replacement to the language of set theory, i.e. the symbol Cd cannot be used in Replacement.

[2] Axioms asserting that Cd is a bijective map from Power of Vz to Vz, those are:

Vz is taken to be some set that serves as a model of Zermelo:

Cd(x,y) -> x subset_of Vz

Cd(x,y) -> y in Vz

For all y in Vz Exist x (Cd(x,y))

For all x subset_of Vz Exist y (Cd(x,y))

Cd(x,y) ^ Cd(z,u) -> [x=z <-> y=u]

[3] Exchange coding axioms: 

Define recursivly "n_th coded image" and "n_th coded inverse image" as:

y is the 0_th coded image of x <-> Cd(x,y)

y is the 0_th coded inverse image of x <-> Cd(y,x)

for n=0,1,2,3,...........

y is the n+1_th coded image of x <-> y={z|Exist m in x (z is the n_th coded image of m)}

y is the n+1_th coded inverse image of x <-> y={z|Exist m in x (z is the n_th coded inverse image of m)}

The axioms are:

For n=0,1,2,3,....

For all x in P_n+2(Vz) Exist y (y={z| Exist m in x (z is the n_th coded image of m)})

For all x in P_n+1(Vz) Exist y (y={z| Exist m in x (z is the n_th coded inverse image of m)})

/ Theory definition finished.

..................................................................

ABOUT AUTOMORPHISMS

The proof of NFU from the above theory is simple since any automorphism j will meet all conditions above and thus it wold prove NFU. However we need j to be a bijection from PV to V to prove NF, and it is here were it is provable j cannot be an automorphism.

Of note that j need not be an automorphism for Boffa's proof to run. It is automorphism of j in Boffa's proof that prevented its method from proving NF. But here there is no need for that so the door is still open to prove NF via that rout.

A proof that j need not be an automorphism is given here:

 I had once defined "pedigrees" on sets, it is something similar to the graph of membership relation on the transitive closure of a set but down to some end set, i.e. a set the membership of which is not elicited in the graph. For example The graph G_{} of set {{},{{}}} would be isomorphic to the graph H_{{}} of the set

{{{}},{{{}}}}. The notation X_i refers to the name of the Graph and the index i is the ending set.

Notice that graphs G_{} and H_{} for the above sets are NOT isomorphic.

So the pegdigree is a function of a set and some ending set. So G above is said to be: the pedigree of set {{},{{}}} down to {}.

Now it is easy to construct a cummulative hierarchy V* in which every set in it replace sets in ordinary cumulative hierarchy but ends with {{}} instead of {}, so the base set of V* is {{}}, the next tire is {{{}}}

the third tier is {{{}}, {{{}}} }, etc...

Now we take an automorphism j on this V* hierarchy (one that is a model of Z),

then we construct another function j* from V (the ordinary hierarchy of Z) to j(V*) after a replacement function F on dom(j) were each set is sent back into its isomorphic pedgree copy starting from {}. That is, we have:

j*(x)= j(F(x))

where F(x)=x*

where x* is the pedgree copy of x starting from {{}}

In this way j* is NOT an automorphism since j*({}) = {{}}

However j* does meet all minimal conditions to interpret NF(U).

Of course I'm not claiming here that the map j* is not subject to the ordinary parity problem involved

with the full automorphism j present in the ordinary Boffa proof, but I'm only illustrating an example

of a j map that is not an automorphism but yet can interpret NFU.

The nucleus theory:

The following is a description of what I call the "nucleus" theory, it is the simplest kind of theory belonging to my last approach of coding over ZF. This theory simply use a bijective function j between Vz and Vz union the set of all complementary sets of elements of Vz over Vz. Lets call the last set as Uz so:

Uz= Vz U {y' | y in Vz}

where y'={z| z in Vz ^ ~ z in y}

Now we have j: Uz -> Vz  and j is a bijection.

so j codes all elements of Uz by elements of Vz.

Where Vz is a set in ZF extended theory that can interpret ZF.

Here j is an "internal" function in ZF since it is provable "in" ZF to have a bijection between Uz and Vz, so

j is freely used in Replacement and Separation of ZF.

The nice thing is we can interpret "Extensionality+Complements+Boolean Union+Singletons+Set Union"

over Vz using a defined membership relation y E x <-> Exist z (x=j(z) ^ y in z). 

Proof: 

Extensionality is simply proved since j is a bijection.

Complements is simply proved because by definition the domain of j includes a complementary set for

each element in it, and this will be straightforwardly translated in terms of E.

Boolean union: The Boolean union of two elements of Vz then its Boolean union is in Vz and thus in Uz.

The Boolean union of x and y is provably the complementary set of the intersection of x' and y'

Now if x or y is a complementary set of an element of Vz, i.e x' or y' is in Vz, thus intersection x',y' would be a in Vz and thus in Uz.

Singletons: Every a in Vz has {a} in Vz also now let b=j({a}) and thus be would be a set that that b as its

sole E element. 

Set Union: of course it is meant to be "E-set union". We need to prove that for every element x in Uz

the set union of all sets coded by elements of x is in Uz also.

Proof: if x in Vz, then either all sets coded by elements of x are elements of Vz, by then their union would be in Vz also and thus in Uz; or there exist a set k that is coded by an element of x and k is not an element of Vz, i.e. k is a complementary set of an element of Vz, by then set union would be the complementary result of an intersection with an element k' in Vz, and so in Uz.

if x is not in Vz, then we prove that there MUST be a set q that is coded by one of the elements of x

were q is not in Vz. The proof goes by contradiction since the assumption that all elements of x

are only coding elements of Vz would mean that all complementary sets of elements of Vz would be coded

by elements of a subset of x', but x' is in Vz which would entail that there is an element of Vz that is equal in size to the whole of Vz itself (Since Vz is equal in size to the set of all complementary sets of its elements) which is impossible. Accordingly the set union of all sets coded by elements of x would be the complementary result of an intersection with an element in Vz, and so in Uz.

QED

What I like about the Nucleus theory is that it didn't mechanically force the axioms, it only did so for complements while all the other axioms followed spontaneously. I think such an approach can be used

to prove the whole of NF.

SKEW PAIRS:

there are some very strange and aukward findings about using skew pairs. A skew pair is a pair in which projections doesn't have the same type! 

Example: <a,b>= ({a}, b) 

where (,) is the Kuratwoski pair, or actually any pair with projections of equal type. 

You see here the first projection of the pair <,> is one type lower than the second.

One particular strange finding is that we can find a a skewed membership relation, and its domain, that is fulfilled by all axioms of NF, and so it's fulfilles any finite set of axioms that axiomatize NF, yet NF itself won't think of that as a model of it, while in reality its a model of it. So NF can construct of a model of it, yet it cannot see it as such.

There are other very strange and funny results related to cardinal comparisons using these skew pairs.

OLDER IDEAS

about proving NF, that failed in doing so, yet it proved some theories extending NF3. 

I just want to exposit on a simple approach whereby one can get fully extensional fragments of NF starting from NFU via some non-stratified membership relation. It will be shown that we can get a theory that extends NF3 in that way.

Start with NFU + |Ur|>|Set|, where Ur is the set of all Ur-elements and Set is the complementary set of Ur.

Fix some disjoint sets Ur1, Ur2 of Ur-elements such that Ur1 U Ur2= Ur, and such that |Ur1|=|Ur| and |Ur2|=|P*(Ur)|, where P*(Ur) is the set of all *set*s of Ur-elements (including the empty set).

Take a bijection j that sends each element of Ur1 to itself, and sends each element of Ur2

to a set of Ur-elements that is not a singleton subset of Ur1, in other words we have

j: Ur -> P(Ur)\{{x}| x in Ur1} & j is a bijection & for all x in Ur1 [j(x)=x] & for all x in Ur2 [j(x) in P(Ur)\{{x}| x in Ur1}]

where P is the true general power object operator.

That such a bijection j can exist is easily proven!

Define a new membership relation E as:

y E x <-> (y in j(x) & j(x) is a set) Or (y=j(x) & j(x) is an Ur-element)

This will enforce FULL Extensionality in the resultant E model! all of the Ur-elements in the original model 

would be seen as Quine atoms in the resultant model, also it would prove

Complements

Boolean Union

Sinlgetons

Set union

Relative Products (unordered)

for relation E (over domain Ur)

this is at least as strong as NF3, but not only that it also proves an intersection relation set over non Qunie atoms, i.e. it proves {{a,b}| exists c (c in a & c in b) & a is not a quine atom & b is not a quine atom}, where {} here is E defined. So mostly it is much stronger than NF3

Prospects for interpreting NF itself.

We know that the set {{a,{a,b}}| a,b in Ur, a=/=b} is not consistent with NFU+|Ur|>|Set|, so this must be a proper class, i.e. the formula x={a,{a,b}} doesn't define a set (we'll loosely say that it defines a proper class, although no variables for proper classes are presented here).

Now we need to overcome the deficient intersection relation set, but we cannot do that in a direct manner, so we need to define a NEW membership relation E* on top of the older membership relation E that makes for the missing of those pairs.

I'm not sure if this can be made by pure formulations, however I'll try, one possible strategy is what I call as a Gap filling strategy, the idea is to take the same membership relation E but bring back all singletons of elements of Ur1 to it, now we'll by then have a new intersectional relation set in which elements of the form 

{ {{a},y} | a in Ur1 & a in y} are new, while all old elements of the above intersectional relation set remains.

Now what we need to do is to replace those by {a,y} pairs where a in y and a in Ur1.

The idea is to define a new membership relation E* to do that replacement, a possible definition is

y E* x <->  exists y* (y* E x & \forall m (m E y* -> exists n E y (n ~~^E m)) & for all n (n E y -> exists m E y* ( m ~~^E n)

where ~~^E is coextensionality in terms of E.

so the pairs {a,y}, {{a},y} , where a in Ur1, and a in y, appear co-co-extensional with respect to relation E, i.e. we have a being E-coextensional with {a}, and of course y also E-coextensional with y, accordingly {a,y} will be in the intersectional relation set! 

Then we get rid of the replaced sets containing singleton subsets of Ur1, and we get our desired intersectional relation set with respect to relation E*.

We do that process for all axioms on the domain of this theory (which lacks singleton subsets of Ur1), so all sets are expected to remain the same.

Anyhow this is still premature, we need to be careful with the definitional replacements as to preserve the rest of the axioms and at the same time add the desired intersectional relation set under the new defined membership relation E*.

If we can do that, then we get to interpret NF, and thus prove its consistency.

I still doubt it so much.

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Thu, Sep 13, 2018 at 5:01 PM

the idea of gap analysis to patch up the difference between this theory and NF is still in its infancy, it needs a lot of refinements, it is like quick sand!

Show original message

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Thu, Sep 13, 2018 at 11:50 PM

I think it can be done (I'm not sure yet), we take 3 models, the smallest is the one without the singletons of elements of Ur1, the next is the one with those, and the third one is composed of the first one and the elements of the second model whom their translations under E* (with the membership restricted to the first model) doesn't result in sets existing the the first model!!!! Now we take our domain to be the third model, and use the E* where x E* y is restricted to x in the first model and y in the third model, and the ~~^E is to be provable in the second model! (so it is a non-transtive model)., that said it appears to me that all rules of NF would hold in terms of relation E* and domain being the third model. A complicated approach like a quick sand.

However I'm not sure of this yet, I need to check it many times.

Show original message

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Fri, Sep 14, 2018 at 1:15 AM

the first model is a model of the theory presented above.

the second model is a model of the theory in which the singletons of Ur-elements are not exempted from the range of j , with the same details otherwise

The third model is the first model plus sets in the second model whose translations under E* (where x E* y is the same definition of x E* y given above but with having x being restricted to the the first model and y an object present in the second model and ~~^E being provable in the second model) won't result in sets already existing in the first model.

Now we take the third model as our domain, and take the membership relation E* with x E* y restricted to x,y being elements of the THIRD and ~~^E part of the definition of E* being provable in the second model.

Im still not sure of this yet, I didn't check the details, it might fail badly really, I'll check

Show original message

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Fri, Sep 14, 2018 at 5:49 AM

still in the quick stand.

I think the addition of sets to the first model from the second model to form the third model, must be guided by extensionality over E* concerns, so if a set in the second model causes violation of E* over the second model, then it is not added to form the third model, this way all sets of the third model would be E* extensional!!!!

However the burden is to prove other axioms especially set union and relative products.

I'll see into that

Show original message

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Fri, Sep 14, 2018 at 3:46 PM

I was thinking outload, I need to re-think this gap analysis method.

Show original message

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Mon, Sep 17, 2018 at 2:00 AM

OK, I'll give a possible scenario, though I don't have a proof that it works.

We take the first model (a model of the theory NF-Intersection relation set+ intersection relation set over sets - singletons of Ur-elements) and then we take the second model, which is a model of the same above theory but without exempting singletons of Ur-elements. Now we arrange for matters so that the first model is a subset of the second. Then we start adding sets from the second model to the first in a stepwise manner. First we add the intersection relation set over sets of the second model, we add that to the first model, then we add complements, boolean union, singletons, set union and un-ordered relative products, to produce a new model, then iterate the same operations on that model, and so on, we can take the set ORD of all ordinals, and define the above stepwise process (since all steps are stratified!) such that for any pair (i, V), we get (i+1, V*) where V* is what is produced form V by all operators above, now when i is a limit ordinal, we take the union of all prior stages. Now we take the union of the range of this relation (which is a set in this theory), and hopefully that would be a model of NF with respect to relation E* defined in the above manner. Here extensionality, boolean union, complements, singletons and intersection relation set are easily provable, however what needs to be proved are set union and unordered relative products. My guess is that they would be provable.

Show original message

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Mon, Sep 17, 2018 at 12:34 PM

In order to be more precise the first model is of NFU-Intersection relation set (Unordered) - singletons of Ur-elements + intersection relation set over sets (Unordered).

The second model of is the above theory but without exempting singletons of Ur-elements.

(so it is not of NF as written above, it is of NFU).

However when we get the union of all stages (per ordinals as described above), this I think it would be a model of NFU also, it is here were we'll apply the definition of the new membership relations E and E* in order to get to NF.

Also to make a correction, if we denote the first model as V_0, then V_1 would be just the addition of two sets to V_0 that of the intersection relation set (over all SETs of the second model (which is labeled here as V_final)) and of the disjointness relation set over ALL sets of the second model.

So we have the first model V_0, then we create the other models per ordinals in a recursive manner, then we get V_ord where ord is the last ordinal in NFU model V_final, now V_ord is not the same as V_final, the latter is the model of NFU without exempting singletons of Ur-elements.

I think that V_ord would provide an interpretation of NF through relation E*.

Show original message

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Mon, Sep 17, 2018 at 9:42 PM

No we cannot get all the V_i because the singleton operator will cause type shifts and prevent the recursion. However I think we can get NF - Singletons of some sets. I'm not sure of the strength of such a theory though

Show original message

Zuhair

 <zaljohar@comed.uobaghdad.edu.iq>

To:

Zuhair

,

Randall Holmes

,

Thomas Forster

,

Nathan Bowler

Mon, Sep 17, 2018 at 11:03 PM

Anyhow it might be salvageable! because at the end we'll get a model of NF-Singletons of some sets, but the total number of sets that lacks singletons is just P(V), and since we do have P(V) of non quine sets that have singletons, then we can use the latterones to code both sets that have singletons and sets that do not have singletons, and let quine atoms code themselves, then under that coding we just define a new membership relation in the usual manner, and we simply get a model of NF.

So in nutshell we build a model N of "NFU-Singletons of Ur-elements-Intersection relation set + intersection relation set over sets that doesn't have singletons of Ur-elements in their transitive closures" call this the base theory.

After that we build a model M of NFU such that N subset and element of M.

We add to N the intersection relation set over all sets of M, and also add the disjointness relation set over all sets of M. All those sets use unordered pairs.

Now what we do now is to define a relation R that is full stratified such that for every X,Y such that X R Y the types of X and Y are equal! this would be closure under operators of (Boolean union, Complements, Unordered relative products and Set Union) this is full stratified and type preserving as required from R. So in reality R is a unary function, so we speak of that as Y=R(X)

Now we use transfinite recursion using relation R over the whole set of ALL ordinals in M, in the usual manner as N0=N, N1=N+ above two sets

and let Ni+1 = R(Ni), and Nj= U(Ni<j)

We take the union of all Ni for each ordinal i, and this set would most likely be closed under: Extensionality, Complements, Boolean union, Set Union, Unordered relative products, Intersection relation set. Under relation E* defined over relation E (the details of those are given above)

So in other words we have NF-Singletons + there is a set of sets (i.e. non quine atoms) that has singletons that is equal in size to the set of sets that do not have singletons.

The last step is to work in this theory and code all sets without singletons by a segment of sets that has singletons and code all the other sets with what is left of that sets that has singletons. And we get Singletons and thus full NF.

The details of models N, and M are as follows

we work in NFU+|Ur|>|P(Ur)|, take the set Ur of all Ur-elements, then fix a partition {Ur1, Ur2, Ur3} over Ur, let |Ur1|=|Ur| & |P(Ur)|=|Ur2| & |P(Ur)|=|Ur3|.

Now take j to be the bijection that sends each element of Ur1 to itself,

and each element of Ur2 to a subset of P(Ur)\{{x}| x in Ur1} in a bijective manner, and each element of Ur3 to a subset of P(Ur) in a bijective manner.

Now it is obvious that if we define E as x E y <-> x \in j(y), then clearly we'll have Ur1 U Ur2 serving as the model N of the the BASE theory (see above). written in terms of E, and Ur serving as a model M of NFU written in terms of E.

The successive additions of sets from complement of N relative to M is clear, and can be done in a full TYPE preserving Stratified manner, and thus can be iterated to the full extent of ORD.

The idea is that the union of all Ni's must be closed under those stratified operators that built the individual recursive stages, otherwise this would mean that we'll end up with a stage outside of all of those stages which is absurd.

since it would seem to entail the existence of an ordinal beyond all ordinals thus rising Burali-Forti. The question of extensionality is nice, but i think it would be full presevered over all stages.

I'm not full sure of this argument though, but if I got things right, then it seems to manage to interpret full NF.

It is important to understand definitions of E and E* that would make the final interpretation of NF-Singletons mentioned above

y E x <-> (y in j(x) & y is a set) or (y=j(x) & y in Ur1)

y E* x <->  exists y* (y* E x & \forall m (m E y* -> exists n E y (n ~~^E m)) & for all n (n E y -> exists m E y* ( m ~~^E n)

where ~~^E is coextensionality in terms of E.

the ~~^E would be provable in model M, while the domain of the model is Ui Ni

for all i in Ord.

A question that I've posed to MathOverflow:

The link is here: NF in terms of ZF

Best Regards