Talk:Axiom of empty set

Does logic imply the existence of the empty set?

The last paragraph does not make sense. You don't need any fancy axiom (like infinity) to conclude that there exists at least object; it is a theorem of the first-order predicate logic, in which the theory is assumed to be formulated. Then existence of an empty set follows from separation. -- EJ 21:51, 17 August 2005 (UTC)

Some versions of First-order logic implicitly assume that something exists. However, I consider them to be wrong, a hang-over from the days when "For all" was assumed to imply "Some". What about a model whose universe is the empty set? It contains no elements. So your version of logic would disallow it. But I see no reason to exclude it. So that version of logic is erroneous. JRSpriggs 04:17, 16 September 2006 (UTC)

It's the other way around. The "axiom" of empty set is a hang-over from early 20th century, when the now familiar logic was not yet spelled out formally. Empty models are disallowed for good reasons, their presence instantly breaks too many things to be worth the trouble, such as modus ponens, the intuitive axiom $\forall x\,\varphi (x)\to \varphi (y)$, prenexing rules, and Bernays substitution.

Bear in mind that it does not matter what you find erroneous, but what is accepted as standard by the mathematical community. Every single book on set theory I am aware of declares the background logic to be the first-order classical logic with equality. I've never seen any reference formulating set theory in the free logic, as you would want it. -- EJ 16:12, 16 September 2006 (UTC)

$\forall y((\forall x\,\varphi (x))\to \varphi (y))$ is true in the empty model as are all universally quantified sentences. As for your other claims, "... breaks ... modus ponens, ... prenexing rules, and Bernays substitution.", I would like to see more explanation. JRSpriggs 02:57, 18 September 2006 (UTC)

Validity is affected by adding universal quantifiers in front, that's another (mis)feature of free logic. The schema $\forall y\,(\forall x\,\varphi (x)\to \varphi (y))$ is indeed valid, but the schema $\forall x\,\varphi (x)\to \varphi (y)$ generally is not. Take $\varphi (y)=\exists z\,(z=z)$ for instance. Now the other examples.

Modus ponens: let P be a unary predicate symbol (binary would do all the same, if you want to stick to the language of ZFC). Then $P(x)\lor \neg P(x)$ and $(P(x)\lor \neg P(x))\to \exists y\,(P(y)\lor \neg P(y))$ are valid in all models (empty or not; every formula with at least one free variable holds in the empty model). However, the formula $\exists y\,(P(y)\lor \neg P(y))$ does not hold in the empty model.

Prenexing: for example, the equivalence

$(Q\lor \exists x\,P(x))\equiv \exists x\,(Q\lor P(x))$

fails in the empty model. Most of the other prenexing rules fail as well, but I didn't bother to check them all.

Bernays substitution: if P is a unary predicate, then $\forall x\,P(x)\to P(y)$ is valid, whereas the schema $\forall x\,\varphi (x)\to \varphi (y)$ for arbitrary formulas $\varphi$ is not, as explained above. -- EJ 17:24, 18 September 2006 (UTC)

I rewrote the last paragraph of the article in a way which acknowledges the possibility that logic could force the existence of some set. But since some set theories may not have separation as an axiom schema, empty set may still be required. JRSpriggs 06:16, 19 September 2006 (UTC)

I regard formulas with free variables as either a short-hand for a sentence (probably with extra universal quantifiers) or as not well-formed. Since you are not saying what the free variable x means, then you have an ambiguity which can lead to logical fallacies.

$\forall x(P(x)\lor \neg P(x))$ and $\forall x((P(x)\lor \neg P(x))\to \exists y\,(P(y)\lor \neg P(y)))$ are indeed valid. However, from them you can only conclude $\forall x(\exists y\,(P(y)\lor \neg P(y)))$.

Well, you are correct about the prenexing. But is it so hard to just say $\exists w(\top )\to [(Q\lor \exists x\,P(x))\equiv \exists x\,(Q\lor P(x))]$ instead?

And since free variables are invalid, the Bernays substitution is not a problem. JRSpriggs 06:16, 19 September 2006 (UTC)

If you want logic to work the same way for relativized quantifiers (bounded quantifiers), e.g. $\forall x\in \{\}P(x)$, as for plain quantifiers, then you must include the empty model as a valid model. JRSpriggs 09:09, 20 September 2006 (UTC)

The logic of relativized and unrelativized quantifiers is different regardless of what I want, because ZFC proves the existence of a set in one way or another.

Prenexing: no, it is not so hard. But it is counterintuitive, and it is contrary to what a typical mathematician learns about the standard logic.

Treating formulas with free variables as not well-formed or incomplete makes sense. However, the point is that classical logic is described by simple and elegant calculi, such as this one:

$(\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))$

$\varphi \to (\psi \to \varphi )$

$(\neg \varphi \to \neg \psi )\to (\psi \to \varphi )$

$\forall x\,\varphi \to \varphi (t/x)$

$\varphi ,\varphi \to \psi \vdash \psi$

$\varphi \to \psi \vdash \varphi \to \forall x\,\psi ,$ x not free in $\varphi$

The completeness of this (and other) calculi heavily relies on using formulas which are not sentences (whether they are considered valid standalone propositions or not), in the same way as I used it in the modus ponens example above. I wonder whether you know a calculus for free logic approaching the simplicity of this one.

Let's look at the general picture. I am not saying that it is impossible to develop ZFC on top of free logic. However, it is nonstandard, and it is a gratuitous complication. It would make sense if used as a basis for a theory which genuinely needs empty models, but that is not the case of set theory. All the trouble necessary to modify the usual logic only serves to justify another complication, viz. addition of an axiom. More precisely, it is even worse: it's purpose is so that we can say "the axiom is redundant, but that's because of the axiom of infinity, not because of logic". I, for one, find such approach pointless, absurd, and confusing. But I am a logician, not a set theorist. -- EJ 18:23, 21 September 2006 (UTC)

I was not aware of any distinction between "free logic" and first order predicate logic until you mentioned it here. I was aware that some people used what I considered to be invalid and sloppy logic. But I had developed my own rigorous version which I use personally. However, it is a kind of natural deduction and it would be too much (and inappropriate) to describe it on this talk page. And putting it in an article would violate the policy on OR. JRSpriggs 09:12, 1 October 2006 (UTC)

The now very old discussion above is confused. First-order set theory is based on first-order logic which proves the existence of at least one thing. Proof. Let T be a validity. Then by existential generalization (derivable or taken as primitive), $\exists xT$ is a theorem. This does not imply the existence of a set/class unless it is assumed that only sets/classes exist. If this is not assumed, then one needs an additional axiom, e.g. stating that for any thing x, there is a set {x}, in order to get the existence of at least one set from only the resources of FOL. Since most presentations of set theory want to be free from urelements, it is easiest to take the existence of the empty set as axiom and to formulate Infinity in terms of the empty set. Devlin, Mendelson, Suppes, and others do this. Smullyan and Fitting (Set Theory and the Continuum Problem) are sloppy here, since their Theorem 1.1 and its proof depends on their being a class to begin with, which does not follow from anything they say previously (including what they say about "V"). Stoll (Set theory and Its Logic) is equally sloppy, taking "there is a set" as a "temporary axiom" but never replacing that axiom with anything else that allows one to remove the "temporary" qualification. I haven't looked at other literature, but it would be interesting to do so! Nortexoid (talk) 09:24, 25 October 2012 (UTC)

Re "This does not imply the existence of a set/class unless it is assumed that only sets/classes exist": This may be true in principle, but this assumption is built in the most common axiomatic set theories like ZFC. For example, ZFC is a theory in single-sorted first-order logic, and as such it has only one type of objects. These objects are informally called "sets" for clarity. The statement $\exists x\,x=x$, provable in logic, means "there exists a set" in ZFC, and it is impossible to speak about "things that are not sets" in ZFC. This may not be true for other set theories (e.g., in set theories with urelements where sets are only objects satisfying a special predicate), but that’s no reason to delete a piece of information applicable to mainstream set theory.—Emil J. 11:49, 25 October 2012 (UTC)

What does it mean to say that ZFC has only type of object? Do you mean that its intended interpretation includes only one type of object? True, but ZFC does not demand this. The point is this. None of the non-existential axioms of ZFC entail that there exists a set. Moreover, Infinity entails the existence of TWO sets (given Regularity) if it is formulated as $\exists X\exists Y(X\in Y\land \forall Z(Z\in Y\to Z\cup \{Z\}\in Y)$. If we formulate it as it is formulated in various wikipedia entries, then it already depends on the existence of the empty set, which itself cannot follow from Infinity in this case. So one still needs an axiom implying that there is a set, independent of Infinity, unless one takes the above formulation implying the existence of two sets, one of which need not be the empty set. But that is in any case equivalent to asserting the existence of a set A and then using that in the axiom of Infinity.

If in ZFC-minus-existential-axioms one could already prove the existence of a set from the bare resources of FOL alone, all these brilliant set theorists keen on theoretical economy would not go out of their way to redundantly postulate as axiom the existence of a set. Nortexoid (talk) 12:54, 25 October 2012 (UTC)

ZFC is a particular set of axioms in first-order logic. The language for these axioms has only one type of variable, and thus each interpretation (model) has only one type of object. The jargon for this is that ZFC is a "single sorted" theory. This is what is meant by saying there is only "one type of object" in ZFC.

The first-order logic that is usually studied (and which is usually used to formalize ZFC) includes $(\exists x)[x=x]$ as a logical axiom - this is provable in every first-order theory with equality, including the empty theory. The other option, "free logic", would not include that existence axiom as a logical principle. But free logic is not commonly used in the literature, because for example free logic does not validate typical deduction rules such as the rule:

$\psi \lor (\exists x)\phi (x)\vdash (\exists x)[\psi \lor \phi (x)]$ when x is not free in ψ

So even without the axiom of the empty set or the axiom of infinity, the background first-order logic used to formalize ZFC still proves $(\exists x)[x=x]$. Given any set, we can form the empty set using the axiom of separation. This is why the axiom of the empty set is often not included by authors, because it is provable from separation. Neither of the two most common references, Jech and Kunen, include the axiom of the empty set. It's mostly used, in my experience, in pedagogical contexts where not all of the axioms are assumed from the beginning, and in which the students are not familiar with formal logic. — Carl (CBM · talk) 13:34, 25 October 2012 (UTC)

It depends on how the theory is formulated, and what theory we are talking about. In some theories there are sets and classes and, while one can prove there is a class from FOL alone, one cannot use this to prove there is a set. (I believe Mendelson's version of NBG is like this.) As such one needs an axiom implying the existence of at least one set. In some theories there are urelements and most axioms are stated as (universally quantified) conditionals: if x and y are sets, there is a set whose members are precisely x and y, etc. (Suppes's version of ZFC is like this.) As such, ExT (e.g. T := x=x) does not imply the existence of a set, so one needs an axiom implying the existence of at least one set. Nortexoid (talk) 14:18, 25 October 2012 (UTC)

(e/c) I am not talking about any interpretations. The formulas of ZFC are constructed by means of Boolean connectives and quantifiers $\exists x$, $\forall x$ from atomic formulas $x\in y$, $x=y$, where $x,y$ are any two of a countable list of object variables. Nothing more. It is customary to call the objects for which these variables stand for “sets”, but it does not really matter, you can call them any other way you like (but if you do, and if you also want to call some things “sets” in ZFC, you first need to make sure that your “sets” are defined by a formula in the above language). Regardless of any interpretation, it is a purely syntactic fact that in first-order predicate calculus in this language, the sentence

$\exists x\,\forall y\,\neg (y\in x)$

is derivable from the sentence

$\forall x\,\exists y\,\forall z\,(z\in y\leftrightarrow z\in x\land \neg (z=z)).$

The first one is how this article defines the axiom of empty set, and the second one is an instance of the schema of separation.

I fail to see how what you wrote about the axiom of infinity has to do with anything. The article already explicitly states that the argument may or may not work depending on the exact formulation of the axiom, which is what you appear to be saying.—Emil J. 13:52, 25 October 2012 (UTC)

I agree, it depends on how the theory is formulated. This much should be made clear when it is said that ZFC implies the existence of at least one set from the resources of FOL alone. Nortexoid (talk) 14:34, 25 October 2012 (UTC)

But that claim is completely clear, because it is only talking about ZFC. — Carl (CBM · talk) 14:56, 25 October 2012 (UTC)

As already mentioned, there are versions of ZFC with urelements (Suppes), so it's not completely clear. Nortexoid (talk) 16:16, 25 October 2012 (UTC)

Uncontroversial?

"The axiom of empty set is generally considered uncontroversial, and it or an equivalent appears in just about any alternative axiomatisation of set theory."

That sentence should be stronger, or else removed entirely, because it seems to imply that there are some people who find the existence of an empty set controversial, and axiomatisations of set theory that don't include empty sets. Zemyla^t 19:34, 25 September 2017 (UTC)