Talk:Axiom of empty set

From Wikipedia, the free encyclopedia

[edit] 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)