Is the Empty Set Axiom a Theorem in ZF?

[Jerbearrrrrr]

In ZF (or at least the formulation I'm studying), the empty set axiom (\exists \phi)(\forall z)(\neg (z\in \phi)) is a consequence of the other axioms, namely the axiom of infinity (and separation, though googling says that's not necessary) which is (\exists x) (p) 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, (\forall x)(\exists y) (\forall z)(z\in y <=> z\in x \wedge q(z)) 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.

 

[CRGreathouse]

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

 

[Martin Rattigan]

I think because the above proof ultimately rests on the definition (shown as ex-df)

\exists x\phi=_{df}\neg\forall x\neg\phi

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.

 

[Jerbearrrrrr]

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.

 

[CRGreathouse]

I think because the above proof ultimately rests on the definition (shown as ex-df)

\exists x\phi=_{df}\neg\forall x\neg\phi

it assumes that the axioms apply to a nonempty domain.

Not so much. Yes, if you can show that some set exists, then you can show that the null set exists -- but ex-def doesn't show that. The axiom of specialization is where the actual existence comes in here, via 19.20i and 19.22i.

 

[Martin Rattigan]

Not so much. Yes, if you can show that some set exists, then you can show that the null set exists -- but ex-def doesn't show that.

I should have worded my post more carefully.

EDIT: *** Excised suggested alternative that was no better than the original. As you say ex-def 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.

The axiom of specialization is where the actual existence comes in here, via 19.20i and 19.22i.

An interesting point. Statements 1 to 7 all contain free variables and so would be true for an empty domain with the usual interpretation of such statements as the universal closure. Only the last statement would be false, so it would seem the "actual existence" in this proof comes from using MP on an implication with a free variable in the antecedent but not in the consequent.

 

[JSuarez]

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 the classical predicate calculus, either pure or with non-logic axioms (such as the ones in ZFC) it is allways assumed that the domain of interpretation is nonempty. If we drop this assumption we get something called "free logic", that has significant differences from the classical calculus; it's studied mainly by philosophers, but you may see a good review here:

http://plato.stanford.edu/entries/logic-free/"

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.

An interesting point. Statements 1 to 7 all contain free variables and so would be true for an empty domain with the usual interpretation of such statements as the universal closure. Only the last statement would be false, so it would seem the "actual existence" in this proof comes from using MP on an implication with a free variable in the antecedent but not in the consequent.

The author himself states, in the second paragraph, that the proof doesn't obtain in free logics, because of ax-4 and what this one says is one of the things that fail in these logics; see the link above.

 

[Hurkyl]

If we drop this assumption we get something called "free logic", that has significant differences from the classical calculus; it's studied mainly by philosophers, but you may see a good review here:

That's not true -- e.g. if you care anything about the category viewpoint on things, free logic is much preferred. e.g. excluding the empty model spoils the otherwise excellent algebraic properties of any variety of universal algebras without constant symbols.

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.

This depends on whether you read the word "set" as referring to some a priori intuitive notion, or referring to the type of the variables in the formal theory.

 

[JSuarez]

That's not true

Well, it's certainly not false: free logics are defined as the ones where the ground terms and quantified variables may not denote anything, or denote outside the universe of discourse and a particular case is where the domain is empty.
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).

This depends on whether you read the word "set" as referring to some a priori intuitive notion, or referring to the type of the variables in the formal theory.

This depends of you take "set", "class", "number" or whatever to belong to the metalanguage or the object language, as I said in the paragraph immediately before the one you quote.

 

[Hurkyl]

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).

This was the part I was responding to. I will assert that, if nothing else, the convention of excluding empty models is sufficiently unimportant that authors don't find it worth mentioning when they adopt the opposite convention.

 

[JSuarez]

I will assert that, if nothing else, the convention of excluding empty models is sufficiently unimportant that authors don't find it worth mentioning when they adopt the opposite convention.

I disagree: the restriction to nonempty domains (restriction, not convention, because it has significant implications regarding the philosophical question of the ontological commitments of logic) it's stated explicitly in most introdutory textbooks; in more advanced contexts, it's not explicitly mentioned because it's assumed that the intended readers are aware of it.

 

[Hurkyl]

(I hope Jerbearrrrrr doesn't mind our continued discussion)

(restriction, not convention, because it has significant implications regarding the philosophical question of the ontological commitments of logic)

I wasn't so bold as to consider matters of great philosophical import; I was merely concerned with my mathematical applications: my groups can act on empty sets; my sheaves are sometimes supported on proper subsets; when I count linearly ordered sets, I get a nicer formula if there is one ordering on zero elements; in my varieties of universal algebras, there is a free algebra on zero elements, and the intersection of two sub-algebras is again a sub-algebra.

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)

 

[Martin Rattigan]

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 classical predicate calculus, either pure or with non-logic axioms (such as the ones in ZFC) it is allways assumed that the domain of interpretation is nonempty.

Agreed. Also with the metamath scheme. Taking the domain of interpretation as sets comes rather close to assuming what is to be proved in this case. At any rate the use of the ZFC axioms in the proof is minimal. (As they're stated that's unavoidable.)

The author himself states, in the second paragraph, that the proof doesn't obtain in free logics, because of ax-4 and what this one says is one of the things that fail in these logics;

I failed to read that before posting, but I assume the author included it to make essentially the same point.

The fact that the domain is nonempty does not imply set existence: any formal interpretation pressuposes an amount of Set Theory, ...

I don't understand this. I wasn't considering a formal interpretation of the language, certainly not to take a set used for such as a confirmation of the existence of one of the sets handled by the theory.

In the given system it is immediate to prove \exists x(x=x) (without using the ZFC group of axioms). Here x 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, \exists x\forall y\neg y\in x, to imply the existence of an empty set with the same interpretation?

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.

If you're looking for a proof of set existence, in this case empty set existence, from the ZF axioms, it is obvious that you need to construct a proof from the axioms. Whether that is sufficient to convince you of the existence of the empty set would depend on whether you believe the axioms with your interpretation of the terms. If you were sceptical of the existence of any set, you would probably be disinclined to accept the metamath predicate calculus with the interpretation of the set variables (strictly the variables referred to by the set variables) as sets, because of the axiom of existence. On the other hand you could take the view that should any set exist, the axioms and proof are convincing with the aforesaid interpretation. You could take this as a "proof", in the normal English sense, that if any set exists the empty set exists, but obviously this would not be a formal proof or result.

If we drop this assumption we get something called "free logic", that has significant differences from the classical calculus; it's studied mainly by philosophers, but you may see a good review here:

http://plato.stanford.edu/entries/logic-free/"

Thanks for the reference. It looks very interesting.

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 \epsilon,\delta definition.

Maybe this will help.

 

[JSuarez]

(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 wasn't so bold as to consider matters of great philosophical import; I was merely concerned with my mathematical applications: my groups can act on empty sets; my sheaves are sometimes supported on proper subsets; when I count linearly ordered sets, I get a nicer formula if there is one ordering on zero elements; in my varieties of universal algebras, there is a free algebra on zero elements, and the intersection of two sub-algebras is again a sub-algebra.

I don't disagree with you in these examples, and can even throw a couple more: the natural numbers are much more naturally (bad choice of words) defined in terms of sets if we start from 0; many combinatorial counting problems admit more simple solutions if we also start from zero. But classical first-order logic doesn't work on empty domains.

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.

My point of view is roughly this: I don't believe that there are neutral foundations; every choice we make is a philosophical one. Now, we can choose to leave our philosophical assumptions unexamined, or accept the ones who resist better to criticism; I try to follow the latter. Regarding logic, my position is a naturalistic one: I follow Quine in accepting that classical first-order logic is the most effective and correct system of logic that we have today (I go a little further by also accepting a few fragments of second-order and modal logic); given this, the restriction to nonempty domains is more than a technicality: it's a commitment demanded by logic.

also, I don't see why you consider convention and restriction exclusive -- I would have called "restricting to nonempty domains" a convention

A restriction is a choice imposed by external conditions; in this case, it's the position that there is a preferred and correct logic. A convention is a choice between alternatives that are somewhat neutral: you can't argue forcefully that one should be preferred to another and choose the more, well, convenient (again, bad choice of words). Given what I stated above, I don't consider that restriction a convention.

Taking the domain of interpretation as sets comes rather close to assuming what is to be proved in this case.

No, it's not. The "sets" in the interpretation are in the metalanguage and the ones in ZFC in the object language; these are distinct languages on distinct levels. The metalanguage is "above" the object one and provides a semantics for it, but we cannot identify the two.
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.

Originally Posted by JSuarez
The fact that the domain is nonempty does not imply set existence: any formal interpretation pressuposes an amount of Set Theory, ...
I don't understand this. I wasn't considering a formal interpretation of the language, certainly not to take a set used for such as a confirmation of the existence of one of the sets handled by the theory.

I don't understand this. I wasn't considering a formal interpretation of the language, certainly not to take a set used for such as a confirmation of the existence of one of the sets handled by the theory.

As above.

In the given system it is immediate to prove \exists x(x=x)

This is, in fact, a logically valid sentence (in classical logic, not in free logics): you don't need ZFC to prove it.

would you not understand that formula to imply the existence of a set?

Sorry, I wasn't clear; when you say "set variable" you are already assuming an interpretation and, given that this is a logically valid sentence and the objects of your domain are sets, then yes.
When I wrote that a nonempty domain doesn't imply set existence, it was regarding the metalanguage/object language distinction above.

\exists x\forall y\neg y\in x

This sentence, taken as an axiom, posits the existence of an empty set. You may ask why this is necessary is the other sentence above already implies the "existence" of a set; the reason is that we may not want to interpret ZFC, that is, we take as a formal system with no semantics (ZFC here is the union of the "proper" ZFC axioms, plus all logically valid sentences).

My mathematical studies seem to have been continually interrupted by Kings of France rearing their bald heads...

Where is Russell when we need him?