Register to reply 
Empty set axiom (proofs in ZF) 
Share this thread: 
#1
May910, 03:40 PM

P: 127

In ZF (or at least the formulation I'm studying), the empty set axiom [tex](\exists \phi)(\forall z)(\neg (z\in \phi)) [/tex] is a consequence of the other axioms, namely the axiom of infinity (and separation, though googling says that's not necessary) which is [tex](\exists x) (p)[/tex] where p is some formula to guarantee the infinite set is what we want. Let's assume the axiom of separation (subset making) too.
Here are my questions: When they say that the Empty Set Axiom is a theorem in ZF, does that mean we can prove it using first order logical axioms and deductions (axioms like p=> (q=>p))? Does anyone know of such a proof, if so? The empty set is included in the 'p' of the Axiom of Infinity  though I'm guessing the Axiom of Infinity doesn't actually require it (immediately) to be empty. Assuming the Axiom of Separation, [tex](\forall x)(\exists y) (\forall z)(z\in y <=> z\in x \wedge q(z))[/tex] can we just pick q(z)="z not in x" and let x be the set discussed in the Axiom of infinity? If so, how do we formalize this? Thanks. And sorry if it's in the wrong forum. 


#2
May910, 05:53 PM

Sci Advisor
HW Helper
P: 3,682

Here's a proof from the axiom of separation (and a fragment of predicate calculus: predicate calculus, the rule of generalization, the axiom of specialization, and the axiom of quantified implication).
http://us.metamath.org/mpegif/axnul.html 


#3
May910, 06:29 PM

P: 312

I think because the above proof ultimately rests on the definition (shown as exdf)
[itex]\exists x\phi=_{df}\neg\forall x\neg\phi[/itex] it assumes that the axioms apply to a nonempty domain. That is the existence of some set is implicitly assumed. With that implicit assumption the axiom of infinity (which asserts the existence of a specific set) is not needed to prove the existence of the empty set. 


#4
May1010, 02:11 PM

P: 127

Empty set axiom (proofs in ZF)
Thanks, CRG.
Two thumbs fresh. In Propositional Logic, you can just about survive writing things out in full and doing every step. I notice that in Predicate Logic, we have to apply a number of 'shortcuts', all proveable but best left proven on the back of an envelope, before the proof looks reasonable. 


#5
May1010, 10:31 PM

Sci Advisor
HW Helper
P: 3,682




#6
May1210, 09:03 AM

P: 312

EDIT: *** Excised suggested alternative that was no better than the original. As you say exdef itself doesn't have much relevance. *** The point I wanted to make is that if we don't make the assumption in the predicate calculus that the domain of sets is nonempty, the proof doesn't actually prove something that we can interpret as existence for the empty set. In informal proofs based (loosely) on ZFC, it's usually thought necessary to use an axiom of ZFC stating the existence of some set, e.g. the axiom of infinity, so that we can use the restricted axiom of comprehension to prove the existence of the empty set (as OP was suggesting). Here that is an artifact of the predicate calculus in use. What the proof can can be interpreted as proving is that if any sets exist then the empty set exists, rather than that the empty set exists. 


#7
May1210, 09:53 PM

P: 402

http://plato.stanford.edu/entries/logicfree/ The fact that the domain is nonempty does not imply set existence: any formal interpretation pressuposes an amount of Set Theory, but they are at a level (called the metalanguage) above the theory (in this case ZFC) that we are discussing. Set existence must be proven within the theory, as a consequence from the axioms, not from the properties that we assume that the metalanguage has. You may see it like this: suppose we didn't know anything about set theory, and an alien gives us ZFC's axioms, without any interpretation. We don't have a clue about the objects that the axioms are intended to refer, but we may cook up some weird interpretation where they are all true, but doesn't mention sets at all. 


#8
May1310, 04:08 PM

Emeritus
Sci Advisor
PF Gold
P: 16,091




#9
May1310, 05:40 PM

P: 402

But it's not clear, in your reply, what part of my statement you consider false; when I say that free logics are mainly studied by philosophers (or anyone who studies philosophical logic), I didn't intend to diminish it, but it's definitely not a part of the mainstream of logic and the question if it's a fruitful line of reasearch is yet to be determined (and the same can be said of the categorial / algebraic approach; no offense intended). 


#10
May1310, 05:51 PM

Emeritus
Sci Advisor
PF Gold
P: 16,091




#11
May1310, 06:14 PM

P: 402




#12
May1310, 09:41 PM

Emeritus
Sci Advisor
PF Gold
P: 16,091

(I hope Jerbearrrrrr doesn't mind our continued discussion)
The point of view of your parenthetical seems... odd to me, although I can't quite articulate it. I think it's as if you are letting technicalities dictate your philosophical opinion, rather than adopting a neutral foundation, then laying your philosophical opinion on top of it. (also, I don't see why you consider convention and restriction exclusive  I would have called "restricting to nonempty domains" a convention) 


#13
May1410, 12:21 PM

P: 312

The discussion has obviously moved on since the post I'm replying to, so this is probably not so relevant, but I'll post it anyway.
In the given system it is immediate to prove [itex]\exists x(x=x)[/itex] (without using the ZFC group of axioms). Here [itex]x[/itex] is referred to as a set variable. If you interpret the system so that the set variables to refer to sets (as you presumably would for present purposes) would you not understand that formula to imply the existence of a set? If not, would you interpret the result proved, [itex]\exists x\forall y\neg y\in x[/itex], to imply the existence of an empty set with the same interpretation? My mathematical studies seem to have been continually interrupted by Kings of France rearing their bald heads, starting with a long discussion at school concerning the continuity of the real square root function at the argument 0 according to the [itex]\epsilon,\delta[/itex] definition. Maybe this will help. 


#14
May1510, 09:46 PM

P: 402

(Apologies to Jerbearrrrrr, the OP, for a discussion that may not interest him, and to Hurkyl and Martin Rattigan for the late response: the last two days were impossible)
I can give you a more explicit example of this distinction: one of the more studied subsystems of classical logic is the intuitionistic fragment, which rejects some classical equivalences and rules of inference. Nevertheless, it's a complete systems relative to Kripke models, but the more common completness proofs are formulated in classical logic, using arguments that are not intuitionistically valid. This is not a contradiction, because the proofs are carried in the (classical) metalanguage and their correctness is relative to it. When I wrote that a nonempty domain doesn't imply set existence, it was regarding the metalanguage/object language distinction above. 


Register to reply 
Related Discussions  
Feynman's empty space isn't really empty space  High Energy, Nuclear, Particle Physics  12  
Axiom of Empty Set superfluous in ZF?  Set Theory, Logic, Probability, Statistics  8  
Proofs...advice/places to find more practice proofs  Introductory Physics Homework  2 