-5
$\begingroup$

I have written a formal proof of the theorem:

$$\forall U \exists r(\forall a(a\in r \leftrightarrow (a\in U \wedge a\notin a)) \wedge r\notin U \wedge r\notin r)$$

See: http://www.dcproof.com/SeparationAxiom.htm

(Somewhat non-standard notation: & = $\wedge$, | = $\vee$)

It seems you can select a subset much like the so-called Russell Set from any set $U$ without obtaining a contradiction. How can I be certain?

Edit: Apparently you can't be certain. See my own answer below.

  • 3
    A formal proof from what basis of axioms?2012-06-25
  • 1
    It's really unclear what you mean by "the Russell set." The $r$ that you are asserting here is just a subset of $U$, so it is not the "Russell set" that normally leads to any contradiction. Basically, you are saying, for any set $U$, you can find the subset $r$ of $U$ of elements which don't contain themselves. This doesn't mean the same $r$ satisfies this property for all $U$.2012-06-25
  • 0
    @JasonDeVito Like the notation, the axioms are somewhat non-standard. The axioms of logic used are based a form of natural deduction of the kind implicit in most undergraduate mathematics textbooks. The only axiom of set theory I use is a subset axiom like the Axiom of Separation in ZF.2012-06-25
  • 0
    It's clear that the theory consisting solely of separation is consistent. For example, $\{ \varnothing \}$ is a model of it.2012-06-25
  • 0
    @ThomasAndrews Yes, the $r$ would, of course, depend on $U$. I only meant to suggest similarities to the Russell Set.2012-06-25
  • 0
    @ChrisEagle Sorry, I didn't mean to suggest there aren't other set-theoretic axioms in this system. I meant that the only set-theoretic axiom *used in this proof* is a subset (or separation) axiom.2012-06-25
  • 0
    @Dan: Then what is your actual question? It's axiom systems that are or are not contradictory, not proofs.2012-06-25
  • 0
    @ChrisEagle I want to show that the existence of this subset $r\subset U$ does not lead to a contradiction in the same way that the existence of the Russell Set does.2012-06-25
  • 2
    @Dan: I have proved that your statement is not contradictory by exhibiting a structure in which it is true. If "does not lead to a contradiction" means something other than this, you'll have to tell us what that is.2012-06-25
  • 2
    @DanChristensen The only way to prove this is to prove the consistency of some set of axioms. In and of itself, there is no contradiction.2012-06-25
  • 3
    From the comments to my answer, you seem to think you have a particular contradiction you can show from this statement. If so, present that, and ask us what is wrong with the argument, don't ask us to show the consistency of your ill-defined axiomatic system.2012-06-25
  • 0
    @ThomasAndrews I was able to obtain $r\notin U$ and $r\notin r$. I was wondering if I could also get $r\in r$. If that is possible, it would mean big trouble for not only for the system I use here, but for ZF theory as well.2012-06-25
  • 0
    Of course there might be a contradiction in ZF. However what if *your* proof software is to blame?2012-06-26
  • 0
    @AsafKaragila The subset (separation) axiom in my system is meant to be identical to that in ZF. And the other axioms and rules used there are just those commonly used in mathematics textbooks. So, if an inconsistency did arise, it should be fairly simple to determine whether it was a result of a software problem, or whether it was a deeper problem that would also arise in a purely ZF implementation.2012-06-26
  • 0
    @Dan: Be forewarned, every software has bugs. Not every bug is easy to spot.2012-06-26
  • 0
    @AsafKaragila The specs for every axiom and rule are fairly simple. That is the beauty of any formal system. It should be easy to manually verify every line of a proof if some inconsistency is discovered.2012-06-26
  • 0
    And if the proof is $100,000$ steps long? What if there is a memory leak at the $60,000$-th step. Can you trace through that manually and see? If so, you are wasting your time with math software. I am sure every software developing organization would hire you for ridiculous amounts of money.2012-06-26
  • 0
    @AsafKaragila If you can write it, I can verify it. I ask only that you try to break it down into a series of smaller proofs of not more than about 1,000 lines each. (Anyway, there's that moderator again! Gotta go.)2012-06-26
  • 1
    Let me just finish this discussion with the remarked that if I could write a proof for the inconsistence of ZF, I would probably submit it as a dissertation and skip all those years of extensive study instead. Good for me, I cannot write such proof so I can spend a few more years as a student meddling with ZF.2012-06-26

3 Answers 3