Existential definitions in ZFC

Question

In formal set theory (ZFC to be specific) there are some types of definitions: predicate definitions, for instance $A \subset B$ is an abbreviation of $\forall x(x \in A \Rightarrow x \in B)$, comprehension definitions, for instance $A \cap B$ is an abreviation of $\{x \in A: x \in B\}$

The predicate definitions are abbreviations of formulas and comprehension definitions are abbreviations of sets (terms or objects in ZFC).

The problem is with existential uniqueness definitions where we put a name to an object which existential uniqueness is given by a theorem of existential uniqueness. Let be the theorem of existential uniqueness $\forall x \exists! y (\forall z (z \in y \Longleftrightarrow z \subset x))$. It is a direct consequence of the Power Set Axiom.

In this case given a set A, the Power Set Pow(A) is not an abbreviation, you can not substitute Pow(A) by $\forall x \exists! y (\forall z (z \in y \Longleftrightarrow z \subset x))$ because one is a Set (a term or object) and the other is a formula. How can this type of definitions be expressed in a formal way?

Even worse, in many books the Power Set Axiom $\forall x \exists y (\forall z (z \in y \Longleftrightarrow z \subset x))$ is used directly to name Pow(A) without mention that the uniqueness must be proved in order to be able to define Pow(A).

I used Pow(A) as an example but my question is about existential definitions (Is this the right name for this type of definitions?) in general for ZFC. Where a can I find a proper treatment of this topic?

Briefly "existential definitions" are essentially different to definitions such that:

$A \subset B \equiv_{def} \forall x(x \in A \Rightarrow x \in B)$

$A \cap B \equiv_{def} \{x \in A: x \in B\}$

How a existential definition can be written? It is unavoidable the use of metalanguage?

How to name an object that exists thanks to an existential uniqueness theorem?

Answer 1

Once you specify a condition, uniqueness follows by extensionality. And since that we can prove that, there is little point in using $\exists!y$ in the statement of the axiom, because $\exists!$ is not a standard quantifier, but rather a shorthand statement for a much more complicated formula.

Now, you want to talk about class-functions like $\mathcal P(\cdot)$ or constants like $\varnothing$ or $\omega$. And that is a valid concern, since the language of set theory only has the $\in$ symbol.

Enter the notion of a conservative extension. In logic, if you have a language $\cal L$ and a theory $T$, and you have a formula $\varphi(x)$ such that $T$ proves that $\varphi(x)$ defines a unique set, then we can extend the language to $\cal L^+$ by adding a constant symbol $c_\varphi$ and the axiom $\varphi(c_\varphi)$.

We can now prove that any model of $T$ can be interpreted naturally as a model for $T+\varphi(c_\varphi)$ as an interpretation for the language $\cal L^+$. Similarly we can do that with definable functions or relations. And moreover, every proof from $T+\varphi(c_\varphi)$ in $\cal L^+$ can be translated to a proof from $T$ in the language $\cal L$.

And that is what actually going on. In effect we extend the language of set theory to include many "convenient symbols", and we know that we can recursively translate all the statements and proofs from the extended language back to the original language of set theory with just $\in$.

Answer 2

There seems to be some uncertainty as to precisely what you're asking, but perhaps this is an answer to your question.

If you want to only use abbreviations of the sort used for $A\subset B$, the answer is that you don't try to translate terms in isolation; you try to translate formulas in which they occur. Since the well formed formulae of set theory are formed inductively from atomic formulae of the form $\alpha\in\beta$ and $\alpha=\beta$, that means if we want to "translate $\{x:\varphi\}$" you just have to figure out what "$\{x:\varphi\}\in\alpha$," "$\alpha\in\{x:\varphi\}$," and "$\alpha=\{x:\varphi\}$" should be abbreviations for. Here is a version that works adequately in ZF:

• For $\alpha\in\{x:\varphi\}$, we can just say it's a synonym for $\exists y(\alpha\in y\wedge\forall z(z\in y\leftrightarrow\phi))$.
• For $\{x:\varphi\}\in\alpha$, we say that this is just short for $\exists y(y\in\alpha\wedge y=\{x:\varphi\})$.
• and for $\alpha=\{x:\varphi\}$ we refer to the first bullet point and extensionality, translating it as $\forall y(y\in\alpha\leftrightarrow y\in\{x:\varphi\})$.

If we keep unpacking any formula containing set abstracts in this way, we'll eventually reduce them to formulas in which the only terms are variables and the atomic formula are those involving $\in$ and $=$. These formulae get really long and ugly, though; luckily, for reasons Asaf gives, we don't really have to be careful about this as long as our axioms guarantee the existence of a set of all the things satisfying the property $\varphi$--we can just treat them as atomic terms and carry on.

Answer 3

One approach that fx Bourbaki uses is introducing the Hilbert operator. By doing that you don't need more primitives as the quantifier(s) can be expressed in therms of the Hilbert operator.

The advantage of using this is that the language allows a construct to turn a predicate into an object (fulfilling the predicate if possible).

This is similar to the ad-hoc solution to simply allow definition of a symbol by a predicate that has unique validity.

Answer 4

Seeing your comments to Asaf's answer, I think another way to solve your issue would be with another viewpoint : think in terms of (classical) sequent calculus.

Assume you want to prove the theorem "For any set $A$, there exists $B$ such that there is an injection $A\to B$, and no surjection $A\to B$". The usual choice to prove this theorem is using $B=P(A)$. But how to write this formally ?

When you do your sequents calculus, at some point you arrive at $ZF\vdash \exists B, \phi_P(A,B)$ where $\phi_P(x,y)$ is an abbreviation for the formula "$y$ is the powerset of $x$".

At this point you think "Let $B$ be the powerset of $A$", and your natural deduction proof goes on with $ZF, \phi_P(A,B)\vdash ...$" where "..." is anything it must be.

When you arrive at "$ZF, \phi_P(A,B)\vdash$ there is an injection $A\to B$ and no surjection $A\to B$", you can use one of the inference rules of the sequent calculus :

From $\Gamma, \phi(t)\vdash \psi$ ($t$ not free in $\Gamma$) and $\Gamma \vdash \exists x, \phi(x)$, infer $\Gamma\vdash \psi$.

Apply this to $\phi(x) = \phi_P(A,x)$, and $\psi = \exists y, \Omega(y)$ where $\exists B, \Omega(B)$ is the formula we're trying to prove, you finally get $ZF\vdash \exists B, \Omega(B)$. Using generalization, $ZF\vdash \forall A, \exists B, blabla$.

So we've used the powerset of $A$ in a formal proof, but the thing is you can name it (store it in a sense) as a nonused variable, by putting its definition on the side of the hypotheses, and using the (now used) variable in the proof, using its definition at various points in the proof.

That's if you want to use the defined object to prove something else. If you want to prove some properties of the defined object, there are similar things you can do, for instance instead of proving $\forall A, |P(A)|>|A|$ you can prove $\forall A, \forall B, \phi_P(A,B)\implies |B|>|A|$ etc. Since there is only one $B$ such that $\phi_P(A,B)$, this last theorem is the same thing as what you're trying to prove.

I've done this in a purely syntactical fashion but of course to my mind it's important to keep in mind the semantic aspect of things, and in this regard, Asaf's answer mentioning conservative extensions is a very interesting one. Note that he also mentioned the syntactic aspect ("translating a proof in $\mathcal{L}^+$ into a proof in $\mathcal{L}$ recursively"), the only thing I did "more" is give hints as to how this translation can be achieved.

If anyone can make my answer better by correcting some mistakes I've probably made, such modifications are of course most welcome

Answer 5

In the language of ZFC there are no constants or functional symbols, so the only terms are variables. One way how to deal with defintions is to ignore the possibility to introduce new symbols and just imagine that every formula that uses definitions is an abbreviation of a formula in language of ZFC. Definitions can be regarded as an informal but precise way how to write shorter and more readable formulas in the place of very long ones. It should be clear how to translate a formula containing defined symbols into a formula in the pure ZFC language.

For example, $A\subset B$ can be translated into $(\forall x)(x\in A\Rightarrow x\in B)$, and a formula containing $\subset$ somewhere inside is translated by replacing appropriately each subformula of the form $A\subset B$. Similarly for any defined predicate symbol $P(x_1,\dots,x_n)$.

As regards defined function symbols, all we need is to know how to translate a formula of the form $y=F(x_1,\dots,x_n)$, this is replaced by the formula $\varphi(y,x_1,\dots,x_n)$ used as a definition of $F$. Then we also know how to translate $y\in F(x_1,\dots,x_n)$: we replace it by $(\exists z)(y\in z\wedge\varphi(z,x_1,\dots,x_n))$. Similarly we can translate $F(x_1,\dots,x_n)\in y$. The fact that for any $x_1,\dots,x_n$ there is exactly one $y$ satisfying $\varphi(y,x_1,\dots,x_n)$ can be regarded as a "background knowledge", there is no need to encode it directly into the translation.

By the way, $\{x\in A\!:x\in B\}$ is also an abbreviation which has to be translated into a pure ZFC language; formula $y=\{x\in A\!:x\in B\}$ is of course replaced by $(\forall x)(x\in y\Leftrightarrow(x\in A\wedge x\in B))$.