search

metamath / set.mm

Metamath source file for logic and set theory
Other
254 stars 88 forks source link

Prove irreflexivity of set membership in iset.mm #647

Closed jkingdon closed 5 years ago

jkingdon commented 5 years ago

In set.mm we have elirrv which is proved from ax-reg. The question is whether we can prove it in iset.mm from ax-setind. If so, this unlocks a number of theorems (some listed at #629 which takes irreflexivity of set membership as a given).

Most literature I know on this subject is for classical logic (and does not proceed from set induction but from one of the classically equivalent formulations of the axiom of foundation). Presumably there is an intuitionistic proof published somewhere but I'm not even sure where I'd look for it. Or I can just see whether @digama0 immediately sees it off the top of his head :wink: .

Proving irreflexivity, given a well-founded relation, but without assuming the axiom of set induction, is presumably similar but separate: see #646

digama0 commented 5 years ago

Indeed, the proof follows from df-fr, or its proper class analogue ax-setind.

Suppose R Fr A, and B R B where B e. A. Let S = ( A \ { B } ). Suppose everything R-less than x is in S, and suppose x = B; then since B R B we have B e. S which is a contradiction. Thus x =/= B and hence x e. S. Therefore S is inductive, so A C_ S, but this is a contradiction since B e. A and B e/ S.

The exact same proof works in the proper class setting; we just take S = ( _V \ { B } ) and everything else is the same.

digama0 commented 5 years ago

This proof also generalizes to show that there are no finite epsilon loops either (I think set.mm does the two and three cases), where you take S to be everything except the members of the loop.

jkingdon commented 5 years ago

elirr (irreflexivity) is merged into iset.mm and en2lop (lack of 2-cycle loops) is at #650 so I'm closing this.

The well-founded stuff remains at #646 .

jkingdon commented 4 years ago

en2lop (lack of 2-cycle loops) is at #650

In case anyone is still browsing old issues, this is a typo and en2lp is intended - http://us.metamath.org/ileuni/en2lp.html