5
$\begingroup$

Let's take some theorem of ZFC, e.g.: $$(1)\: \exists x \forall y ( y \notin x) $$ We can then choose a constant, denote it by '$\varnothing$' to get the following: $$(2)\:\forall x (x\notin \varnothing) $$ My question is: what's the precise proof of (2) given (1)? Also, let the axioms of FOL be the ones from Geoffrey Hunter's Metalogic (axiom schemata QS1-7), plus the axioms of ZFC (though I think they're irrelevant). The only allowed rule of inference is modus ponens.

P.S. I know that the question is ridiculous, and obviously the "jump" between (1) and (2) makes sense. The only thing that bugs me is that I can't justify this "jump" formally :)

Improve this question
$\endgroup$
  • $\begingroup$ I think you have to prove there's only $1$ empty set and then it should be obvious. $\endgroup$ – user2345215 Mar 9 '14 at 17:43
  • $\begingroup$ How are you going to go about proving it formally considering that $\sf ZFC$ has no constants in its language? In view of this, one would consider $(2)$ just a way of rewritting $(1)$. $\endgroup$ – Git Gud Mar 9 '14 at 17:43
  • $\begingroup$ Though they're intuitively interpreted to mean the same, they are not the same wffs. $\endgroup$ – user132181 Mar 9 '14 at 17:44
  • $\begingroup$ You can't have FOL with just Modus Ponens--you have to have at least one inference rule related to quantifiers as well. Whichever one you select, it should be sufficiently powerful to prove existential generalization. $\endgroup$ – Addem Mar 9 '14 at 17:45
  • 1
    $\begingroup$ A constant such as $\varnothing$ introduced in this way is called a Skolem constant, and the process of removing existential quantifiers by this method is called Skolemization. In a more typical case, the constant is instead a function; for example we can transform $\forall x. \exists y. \phi(x,y)$ by introducing a "Skolem function" $\psi(x)$ which has the property $\forall x.\phi(x,\psi(x))$. In general if there are $n$ instances of $\forall$ before the $\exists$, the Skolem function will have $n$ arguments. Your example has $n=0$. $\endgroup$ – MJD Mar 10 '14 at 13:55
7
$\begingroup$

It is a standard theorem about FOL that given a theory which entails a wff $\exists_1x\varphi(x)$, then we can conservatively add a new constant $c$ to the language of the theory, together with the new axiom $\varphi(c)$. This is conservative in this sense that we will still be able to prove nothing in the language of the original theory which we couldn't prove before (even when we use the new constant to instantiate old universal axioms -- see Henning Makholm's important comment below). So there is a good sense in which the new constant just sprinkles onto the original theory some "syntactic sugar" (some nice notation that enables the medicine to go down more easily, by helping us to put things more snappily or more memorably) without at all changing the basic power of the theory.

That is all that is going on in the present case. Adding notation for the empty set is typically just adding syntactic sugar, which we are allowed to do because, once we know there is a set with no members, it is immediate that this is unique, so we have $\exists_1x\forall y(y \notin x)$, and we can apply that mentioned standard theorem.

Improve this answer
$\endgroup$
  • $\begingroup$ Where can I find the proof of the metatheorem mentioned in the first paragraph? $\endgroup$ – user132181 Mar 9 '14 at 18:22
  • 2
    $\begingroup$ Too much syntactic sugar can cause semantic diabetes. :-) $\endgroup$ – Asaf Karagila♦ Mar 9 '14 at 18:22
  • 1
    $\begingroup$ Mendelson §2.9; Enderton §2.7 -- though they give a more general result (think of a constant as a zero-place function to apply the general result to this case). $\endgroup$ – Peter Smith Mar 9 '14 at 18:25
  • 3
    $\begingroup$ It bears notice that in the form quoted here, the metatheorem actually holds with merely $\exists$ in the premise rather than $\exists_1$ -- that is, we still get a conservative extension. The problem with that case is in the extended theory we still have to make do with the same axioms we had before, apart from the new one defining the notations -- we do not get any instances of, say, Axiom of Separation where the formula we separate over contains the symbol $\varnothing$. ...(cont.d) $\endgroup$ – hmakholm left over Monica Mar 9 '14 at 21:11
  • 3
    $\begingroup$ (cont.d) ... On the other hand, if we can prove $\exists_1$ we get the additional meta-result that every formula in the extended language which contains $\varnothing$ is provably equivalent to one in the original language -- which means we're free to use $\varnothing$ with abandon when we use the axiom schemata, because we can just pretend we "really" used the equivalent $\varnothing$-free formula of the pure language of set theory. $\endgroup$ – hmakholm left over Monica Mar 9 '14 at 21:13
1
$\begingroup$

See the following post.

Form George Tourlakis, Lectures in Logic and Set Theory. Volume 2 : Set Theory, page 122 :

"Let us recall the basics of introducing new function symbols [in first-order logic]. Suppose that we have the following:

$\vdash_T (\exists y) A(y, x)$ --- [call it : "existence condition"]

and

$\vdash_T A(y, x) \land A(z, x) \rightarrow y = z$ --- [call it : "uniqueness condition"]

then we may introduce a new function symbol, say $f_A$, into the language of $T$ by the axiom

$f_ A(x) = y \leftrightarrow A(y, x)$".

Now, in $\mathsf {ZFC}$ we have the Null Set axiom :

$\exists y \lnot \exists x (x \in y)$

i.e.

$\exists y \forall x (x \notin y)$.

Since it is provable from this axiom and the Extensionality axiom that there is a unique such set, we may use the "technique" described above to introduce the notation '$\emptyset$’ to denote it.

In conclusion, it is not enough to prove "the existence" condition; you need also "the uniqueness" condition.

Improve this answer
$\endgroup$
0
$\begingroup$

Let's add my rather informal view:

I think the definitions are considered only some kind of meta thing and not actually part of the language.

So you have to choose a way to give a meaning to definitions.

I can think of 2 kinds of definitions:

  • A property. Let's say $x$ is not empty means $\exists y(y\in x)$
  • An object. You want to denote the $\varnothing$ the $x$ such that $x$ is not empty.

Now let's try to resolve the following formula $$\forall x(x\text{ is not empty}\Longrightarrow x\ne\varnothing)$$

It's quite clear how to resolve a property, it's equivalent to $$\forall x(\exists y(y\in x)\Longrightarrow x\ne\varnothing)$$ but what about $\varnothing$? One way to look at it is to say the formula holds for all $x$ ($z$ in this case) from the definition of $\varnothing$ $$\forall z(\exists y(y\in z)\Longrightarrow\forall x(\exists y(y\in x)\Longrightarrow x\ne z))$$ For this to be actually useful, you need to known such $z$ exists and that it's unique. Both are quaranteed if $\varnothing$ is well defined.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.