Can you do this in a formal proof using ZFC?

[Dan Christensen]

I have just written a formal proof in my own non-ZFC set theory (that the power set of S is never a subset of S). At one point, I have to assume X is an element of X for some set X. Would this be allowed in a formal proof using ZFC?


Dan

Download my DC Proof 2.0 software at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Rupert]

On Tuesday, June 2, 2015 at 8:27:09 PM UTC+2, Dan Christensen wrote:
> I have just written a formal proof in my own non-ZFC set theory (that the power set of S is never a subset of S). At one point, I have to assume X is an element of X for some set X. Would this be allowed in a formal proof using ZFC?

In ZFC the sets are well-founded, you are not allowed to have a set which is a member of itself.

[Justin Thyme]

Dan Christensen wrote:
> I have just written a formal proof in my own non-ZFC set theory (that
> the power set of S is never a subset of S). At one point, I have to
> assume X is an element of X for some set X. Would this be allowed in
> a formal proof using ZFC?

No, regularity forbids X in X for all X.


--
Shall we only threaten and be angry for an hour?
When the storm is ended shall we find
How softly but how swiftly they have sidled back to power
By the favour and contrivance of their kind?

From /Mesopotamia/ by Rudyard Kipling

[Dan Christensen]

Interesting. Then, is it possible to prove in ZFC that a power set of any set S is never a subset of S?

[Dan Christensen]

On Tuesday, June 2, 2015 at 2:35:26 PM UTC-4, Justin Thyme wrote:

> Dan Christensen wrote:
> > I have just written a formal proof in my own non-ZFC set theory (that
> > the power set of S is never a subset of S). At one point, I have to
> > assume X is an element of X for some set X. Would this be allowed in
> > a formal proof using ZFC?
>
> No, regularity forbids X in X for all X.
>

Does that mean you could infer X not in X for any X? My proof would work in that case.

[Justin Thyme]

Dan Christensen wrote:
> On Tuesday, June 2, 2015 at 2:35:26 PM UTC-4, Justin Thyme wrote:
>> Dan Christensen wrote:
>>> I have just written a formal proof in my own non-ZFC set theory (that
>>> the power set of S is never a subset of S). At one point, I have to
>>> assume X is an element of X for some set X. Would this be allowed in
>>> a formal proof using ZFC?
>>
>> No, regularity forbids X in X for all X.
>>
>
> Does that mean you could infer X not in X for any X?

Yes.

> My proof would work in that case.

[Arturo Magidin]

On Tuesday, June 2, 2015 at 1:38:35 PM UTC-5, Dan Christensen wrote:
> On Tuesday, June 2, 2015 at 2:35:26 PM UTC-4, Justin Thyme wrote:
> > Dan Christensen wrote:
> > > I have just written a formal proof in my own non-ZFC set theory (that
> > > the power set of S is never a subset of S). At one point, I have to
> > > assume X is an element of X for some set X. Would this be allowed in
> > > a formal proof using ZFC?
> >
> > No, regularity forbids X in X for all X.
> >
> >
> > --
> > Shall we only threaten and be angry for an hour?
> > When the storm is ended shall we find
> > How softly but how swiftly they have sidled back to power
> > By the favour and contrivance of their kind?
> >
> > From /Mesopotamia/ by Rudyard Kipling
>
> Interesting. Then, is it possible to prove in ZFC that a power set of any set S is never a subset of S?

If you include regularity, yes, since S in P(S). Since S not in S for all S (which follows from regularity), then P(S) is not a subset of S for any S.

--
Arturo Magidin

[Justin Thyme]

Dan Christensen wrote:
> On Tuesday, June 2, 2015 at 2:35:26 PM UTC-4, Justin Thyme wrote:
>> Dan Christensen wrote:
>>> I have just written a formal proof in my own non-ZFC set theory (that
>>> the power set of S is never a subset of S). At one point, I have to
>>> assume X is an element of X for some set X. Would this be allowed in
>>> a formal proof using ZFC?
>>
>> No, regularity forbids X in X for all X.
>>
>>
>> --
>> Shall we only threaten and be angry for an hour?
>> When the storm is ended shall we find
>> How softly but how swiftly they have sidled back to power
>> By the favour and contrivance of their kind?
>>
>> From /Mesopotamia/ by Rudyard Kipling
>
> Interesting. Then, is it possible to prove in ZFC that a power set of any set S is never a subset of S?

Let P(X) be the power set of X. If P(X) subset X then, for all x in
P(X), x in X. But X in P(X), so X in X. Since regularity forbids X in
X, not-(P(X) subset X).

[William Elliot]

On Tue, 2 Jun 2015, Dan Christensen wrote:

> I have just written a formal proof in my own non-ZFC set theory (that the
> power set of S is never a subset of S). At one point, I have to assume X is
> an element of X for some set X. Would this be allowed in a formal proof
> using ZFC?

Assume P(S) subset S. Then S in P(S); S in S, a contradiction.
Thus P(S) not subset S.

Within NBG set theory, let V = { x | x = x }.
P(V) subset V. Proof. If A in P(V), then A is a set and A = A, thus A in V.

[graham...@gmail.com]

Yes it does!

AXIOM OF REGULARITY
A(Z)
E(Y) YeZ -> E(Y)( YeZ ^ !E(X)( XeZ ^ XeY ) )

Z is a subset of the universe of sets V

V = { s1 , s2 , s3 , s4 , s5 }

Z = { s1 , s2 , s3 }

there must exist a starting set Y in any groups of sets Z
that is not a superset of any member of the group

Y = s1
s1 = a
s2 = {a,b}
s3 = { 7 , {a,b} }

s1 e s2 e s3

No element of Z can be an element of Y



This version of regularity uses a recursively defined transitive membership t

A(X) A(Z) X t Z <-> (X e Z) v E(Y) (X e Y) ^ (Y t Z)

AXIOM OF REGULARITY
A(X) A(Z) (X t Z) -> ~(X e Z)


which also breaks any circular membership train

[Charlie-Boo]

Which is stupid because you can certainly ask if {} is a member of itself and the answer is simply no. (This is recognized by the officials BTW so if you attack this then you attack your Gods, heaven forbid.)

Let f(x)={x(x)}. Then f(f)={f(f)} and f(f) is a set that contains itself. This is in general. If a set theory admits applying a function to a function (which differential calculus does) and mapping to a set of sets, then it has a quine atom.

Disallowing a set to be in itself is throwing the baby out with the bath water. Theoretical computer science and logic is all about self-reference, and the above uses the same principle applied to sets, so to disallow it is self-defeating, which is not the kind of self-reference you want.

Russell wrote that the way to fix his paradox is to not allow self-reference. Even before Godel and Turing, Peano said that the set of natural numbers is defined in terms of itself (and any infinite set contains a subset that is 1-to-1 with itself) so he certainly should have known better himself.

C-B

[graham...@gmail.com]

On Friday, June 5, 2015 at 9:47:47 AM UTC+10, Charlie-Boo wrote:
> On Tuesday, June 2, 2015 at 2:33:47 PM UTC-4, Rupert wrote:
> > On Tuesday, June 2, 2015 at 8:27:09 PM UTC+2, Dan Christensen wrote:
> > > I have just written a formal proof in my own non-ZFC set theory (that the power set of S is never a subset of S). At one point, I have to assume X is an element of X for some set X. Would this be allowed in a formal proof using ZFC?
> >
> > In ZFC the sets are well-founded, you are not allowed to have a set which is a member of itself.
>
> Which is stupid because you can certainly ask if {} is a member of itself and the answer is simply no. (This is recognized by the officials BTW so if you attack this then you attack your Gods, heaven forbid.)

Axiom of Regularity could be weakened to allow reflexive membership.

A e B e C e D

A appears nowhere on the right of the membership chain


However self membership isn't necessarily a cycle

AeA e B e CeC e D




You could modify the axiom of regularity to only test membership chains greater than 1

A(X) A(Z) X t Z <-> (X e Z) v E(Y) (X e Y) ^ (Y t Z)

AXIOM OF REGULARITY

A(X) A(Z) (X t Z) -> ~(Z e X)

[George Greene]

On Tuesday, June 2, 2015 at 2:27:09 PM UTC-4, Dan Christensen wrote:
> At one point, I have to assume X is an element of X for some set X.
> Would this be allowed in a formal proof using ZFC?

ZFC has nothing to do with it.
This is always allowed, period. You can always assume anything you want.
You just have to be careful about what you conclude from it.
Anything you derive from it could still be false; the true things you can
prove after deriving some Q's from P are of the form P->Q, *not* Q
by itself.

[George Greene]

On Tuesday, June 2, 2015 at 2:33:47 PM UTC-4, Rupert wrote:

> In ZFC the sets are well-founded,
> you are not allowed to have a set which is a member of itself.

He was assuming it toward a contradiction as part of a (partially) indirect
proof of a lemma, DUH.

[George Greene]

On Tuesday, June 2, 2015 at 2:38:35 PM UTC-4, Dan Christensen wrote:
> Interesting.

No it isn't.

> Then, is it possible to prove in ZFC
> that a power set of any set S is never a subset of S?

Of course it is. What USE did you make of your assumption that there was
some X for which X in X? Assuming something that leads to a contradiction
happens all the time; it's the usual way of proving Cantor's theorem (you
assume there is a bijection, even though you are proving that there isn't).

[Dan Christensen]

On Friday, June 5, 2015 at 3:33:16 PM UTC-4, George Greene wrote:
> On Tuesday, June 2, 2015 at 2:27:09 PM UTC-4, Dan Christensen wrote:
> > At one point, I have to assume X is an element of X for some set X.
> > Would this be allowed in a formal proof using ZFC?
>
> ZFC has nothing to do with it.
> This is always allowed, period. You can always assume anything you want.

As I would have expected, but others were suggesting otherwise. There seems to be quite a bit of confusion about what is and is not permitted in a formal ZFC proof.

[Justin Thyme]

Dan Christensen wrote:
> On Friday, June 5, 2015 at 3:33:16 PM UTC-4, George Greene wrote:
>> On Tuesday, June 2, 2015 at 2:27:09 PM UTC-4, Dan Christensen
>> wrote:
>>> At one point, I have to assume X is an element of X for some set
>>> X. Would this be allowed in a formal proof using ZFC?
>>
>> ZFC has nothing to do with it. This is always allowed, period. You
>> can always assume anything you want.
>
> As I would have expected, but others were suggesting otherwise. There
> seems to be quite a bit of confusion about what is and is not
> permitted in a formal ZFC proof.

Cut and pasted from your post of a few minutes ago:
~Er:Ax:[x in r <=> x not in x]

Move the ~ passed the quantifiers:
Ar:Ex:~[x in r <=> x not in x]

Propositional calculus:
Ar:Ex:[x in r <=> x in x]

Read the above backwards for a proof.

[Martin Shobe]

On 6/6/2015 9:39 AM, Dan Christensen wrote:
> On Friday, June 5, 2015 at 3:33:16 PM UTC-4, George Greene wrote:
>> On Tuesday, June 2, 2015 at 2:27:09 PM UTC-4, Dan Christensen wrote:
>>> At one point, I have to assume X is an element of X for some set X.
>>> Would this be allowed in a formal proof using ZFC?
>>
>> ZFC has nothing to do with it.
>> This is always allowed, period. You can always assume anything you want.
>
> As I would have expected, but others were suggesting otherwise. There seems to be quite a bit of confusion about what is and is not permitted in a formal ZFC proof.

The confusion was over what you were asking, not what is allowed.

Martin Shobe

[Zuhair]

On Tuesday, June 2, 2015 at 9:38:35 PM UTC+3, Dan Christensen wrote:
> On Tuesday, June 2, 2015 at 2:35:26 PM UTC-4, Justin Thyme wrote:
>
> Interesting. Then, is it possible to prove in ZFC that a power set of any set S is never a subset of S?
>
>
> Dan
>

Yes of course. Z proves that for EVERY set S whatsoever the power set of S is *strictly* supernumerous to S. Now for a proof by contradiction assume that there exist a set S such that P(S) is a subset of S, then the identity function on P(S) would be an injective map from P(S) to S and thus P(S) would be subnumerous to S, thus P(S) is not strictly supernumerous to S. A contradiction! Thus no set S can have its power as a subset of it.

This proof has nothing to do with Regularity, it can be carried out in Z-Regularity. Actually any assumption like x in x or the alike violations of regularity are not needed for such a proof.

Zuhair

[Steffen Schuler]

Dan Christensen wrote:
> I have just written a formal proof in my own non-ZFC set theory
> (that the power set of S is never a subset of S). At one point, I
> have to assume X is an element of X for some set X. Would this be
> allowed in a formal proof using ZFC?

No, this would not be allowed in ZFC. With the axiom of regularity,
ZFC assumes just the opposite statement. It is also not necessary,
to suppose the assumption that X is an element of X or contrary
that the axiom of regularity holds. An informal proof in ZFC without
supposing either this assumption or the axiom of regularity that
can easily be formalized follows:

-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*

The author borrowed some notations from Metamath.

Let x e. y denote that x is an element of y.
Let x e/ y denote that x is not an element of y.
Let x (_ y denote that x is a subset of y.
Let x (/ y denote that x is not a subset of y.
Let P~(x) denote the powerset of x.

Theorem. For every set x, P~(x) (/ x.

Proof. Suppose that it is not the case that for every set x, P~(x)
(/ x. Then we can conclude that for some set b, P~(b) (_ b. By
the axiom schema of separation let c be some set such that

(1) for every set x, x e. c iff both x e. b and x e/ x.

Then c (_ b by the definition of subset, so c e. P~(b) by the
definition of powerset. Since P~(b) (_ b, this means that c e. b
by the definition of subset. Plugging in c for x into statement
(1), we can conclude that

c e. c iff c e. b and c e/ c.

Then since c e. b, we can infer the contradiction

c e. c iff c e/ c.

Therefore, for every set x, P~(x) (/ x.

QED

> [...]

[Jack Campin]

Steffen Schuler <schuler....@gmail.com> wrote:
> Dan Christensen wrote:
>> I have just written a formal proof in my own non-ZFC set theory
>> (that the power set of S is never a subset of S). At one point, I
>> have to assume X is an element of X for some set X. Would this be
>> allowed in a formal proof using ZFC?
> No, this would not be allowed in ZFC.

You can assume whatever the heck you like. ZFC isn't tied to any
specific proof methodology and a natural deduction system allowing
hypotheticals is fine. Presumably you want to derive a contradiction
from that assumption.

-----------------------------------------------------------------------------
e m a i l : j a c k @ c a m p i n . m e . u k
Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland
mobile 07800 739 557 <http://www.campin.me.uk> Twitter: JackCampin

[Dan Christensen]

On Friday, August 14, 2015 at 12:59:19 PM UTC-4, Jack Campin wrote:
> Steffen Schuler <schuler....@gmail.com> wrote:
> > Dan Christensen wrote:
> >> I have just written a formal proof in my own non-ZFC set theory
> >> (that the power set of S is never a subset of S). At one point, I
> >> have to assume X is an element of X for some set X. Would this be
> >> allowed in a formal proof using ZFC?
> > No, this would not be allowed in ZFC.
>
> You can assume whatever the heck you like. ZFC isn't tied to any
> specific proof methodology and a natural deduction system allowing
> hypotheticals is fine.

Makes sense to me.

> Presumably you want to derive a contradiction
> from that assumption.
>

Yes.

It is a bit disturbing to see such a lack of consensus on such a basic matter. Are formal proofs in ZFC not really that widely used in journals, etc.? In my day, you could easily get an undergraduate degree in mathematics without ever having studied ZFC theory. Is that still the case?

Dan

[George Greene]

> On Friday, August 14, 2015 at 12:59:19 PM UTC-4, Jack Campin wrote:
> > You can assume whatever the heck you like. ZFC isn't tied to any
> > specific proof methodology and a natural deduction system allowing
> > hypotheticals is fine.

On Friday, August 14, 2015 at 1:19:53 PM UTC-4, Dan Christensen wrote:
> It is a bit disturbing to see such a lack of consensus
> on such a basic matter. Are formal proofs in ZFC not really
> that widely used in journals, etc.?

You could read some journal articles! They are mostly over my head but I
would say that the style in which they present is sort of "meta" -- ZFC is
at an implementation-level of detail. They don't care about the specific
axiomatization unless that's what the article is in fact about.

I'm pretty sure nobody can tell you what axiom-system Wiles' proof (as
assisted by Taniyama/Ribet/whoever) of FLT was in. It Doesn't Matter!
Modular forms *are* what they are *ir*respective of any particular axiomatization!

[Rupert]

As you correctly point out, no proof in a journal article is ever anything remotely like a fully formal proof.

Wiles' proof in the form originally written can be formalised in ZFC+"there is a proper class of inaccessible cardinals", but it seems to be generally agreed that it is not too hard to bring it down into ZC. Whether or not FLT can be proved in PA is still open as far as I know.

[Steffen Schuler]

Jack Campin wrote:

> Steffen Schuler wrote:
>> Dan Christensen wrote:
>>> I have just written a formal proof in my own non-ZFC set theory
>>> (that the power set of S is never a subset of S). At one point, I
>>> have to assume X is an element of X for some set X. Would this be
>>> allowed in a formal proof using ZFC?
>> No, this would not be allowed in ZFC.
>
> You can assume whatever the heck you like. ZFC isn't tied to any
> specific proof methodology and a natural deduction system allowing
> hypotheticals is fine. Presumably you want to derive a contradiction
> from that assumption.

This is true. Mr. Campin, thank you for correcting my false claim.

> [...]

[Julio Di Egidio]

On Friday, August 14, 2015 at 5:50:12 AM UTC+1, Steffen Schuler wrote:
> Dan Christensen wrote:
> > I have just written a formal proof in my own non-ZFC set theory
> > (that the power set of S is never a subset of S). At one point, I
> > have to assume X is an element of X for some set X. Would this be
> > allowed in a formal proof using ZFC?
>
> No, this would not be allowed in ZFC. With the axiom of regularity,
> ZFC assumes just the opposite statement. It is also not necessary,
> to suppose the assumption that X is an element of X or contrary
> that the axiom of regularity holds. An informal proof in ZFC without
> supposing either this assumption or the axiom of regularity that
> can easily be formalized follows:
>
> -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
>
> The author borrowed some notations from Metamath.
>
> Let x e. y denote that x is an element of y.
> Let x e/ y denote that x is not an element of y.
> Let x (_ y denote that x is a subset of y.
> Let x (/ y denote that x is not a subset of y.
> Let P~(x) denote the powerset of x.
>
> Theorem. For every set x, P~(x) (/ x.
>
> Proof. Suppose that it is not the case that for every set x, P~(x)
> (/ x. Then we can conclude that for some set b, P~(b) (_ b. By
> the axiom schema of separation let c be some set such that
>
> (1) for every set x, x e. c iff both x e. b and x e/ x.

Are you using unrestricted comprehension?

> Then c (_ b by the definition of subset, so c e. P~(b) by the
> definition of powerset. Since P~(b) (_ b, this means that c e. b
> by the definition of subset. Plugging in c for x into statement
> (1), we can conclude that
>
> c e. c iff c e. b and c e/ c.
>
> Then since c e. b, we can infer the contradiction
>
> c e. c iff c e/ c.
>
> Therefore, for every set x, P~(x) (/ x.
>
> QED

Shouldn't you just conclude: not for every set x, P(x) (_ x?

Julio

[Julio Di Egidio]

On Saturday, August 15, 2015 at 9:56:50 AM UTC+1, Julio Di Egidio wrote:

> Shouldn't you just conclude: not for every set x, P(x) (_ x?

Oops, in your notation that was: not for every set x, P~(x) (_ x

Julio

[Steffen Schuler]

Julio Di Egidio wrote:
> Steffen Schuler wrote:
>> [...]

>> Then we can conclude that for some set b, P~(b) (_ b. By
>> the axiom schema of separation let c be some set such that
>>
>> (1) for every set x, x e. c iff both x e. b and x e/ x.
>
> Are you using unrestricted comprehension?

No, I'm not using unrestricted comprehension since we can infer
Russell's Paradox from the latter principle. Instead, I'm using
only the comprehension restricted by the set b. Hence, c = {x e.
b | x e/ x}. This restricted comprehension is allowed by the axiom
schema of separation which is contained in the axiom system of ZFC.

> [...]

[George Greene]

> On Friday, August 14, 2015 at 7:25:04 PM UTC+2, George Greene wrote:
> > I'm pretty sure nobody can tell you what axiom-system Wiles' proof (as
> > assisted by Taniyama/Ribet/whoever) of FLT was in.

Wow!
Assisted by a lot more than just them!
"How deep the rabbit-hole goes":
http://mathoverflow.net/questions/97820/a-recommended-roadmap-to-fermats-last-theorem