Do you need a Hilbert style Epsilon operator for definitions in set theory?

Question

I've started to play with mechanizing some set theory stuff. I'm not sure if I want a constructive flavor or not yet.

Anyhow you can do stuff like axiomize the empty set

$$ \top \vdash \exists P. \forall x. x \notin P$$

But you seem to need something like Hilbert's epsilon for making definitions.

$$ \emptyset = \varepsilon P. \forall x, x \notin P $$

Then you prove that the empty set really is empty $\top \vdash \forall x, x \notin \emptyset $ by applying the empty axiom and substitute existential quantification with epsilon.

I'm not sure how constructive this is and this complicates implementation concerns like capture avoiding substitution. Also to be honest I'm not really familiar with using epsilon style quantifiers.

It might help a little to add let binders but that isn't really the same issue. I don't really want to prove $\top \vdash \textbf{let} \, \emptyset = \varepsilon P. \forall x, x \notin P \, \textbf{in} \, \forall x, x \notin \emptyset $

I'm not sure why but you don't really seem to run into the same sort of problem with type theory.

It's kind of weird because you can hand-wave the issue with axiomatic set theory by saying that whenever we mention the empty set in a theorem $\top \vdash P$ we really mean $\top \vdash \exists \emptyset, (\forall x, x \notin \emptyset) \wedge P(\emptyset)$.

Answer 1

The type theories implemented in proof assistants have definitions which allow introduction of new symbols.

Traditional first-order logic avoids definitions by using instead a meta-theorem stating that, whenever $\forall x_1, \ldots, x_n \,.\, \exists! y \,.\, \phi(x_1, \ldots, x_n, y)$ is proved, and $\phi$ has only the indicated free variables, we can conservatively extend the theory with a new $n$-ary function symbol $f$ and the axiom $\forall x_1, \ldots, x_n \,.\, \phi(x_1, \ldots, x_n, f(x_1, \ldots, x_n))$. An example: in set theory we have $\exists! y \,.\, \forall z \,.\, z \not\in y$, therefore we may introduce a constant $\emptyset$ such that $\forall z \,.\, z \not\in \emptyset$.

This meta-theorem of first-order logic suffices for meta-theoretic studies in textbooks, but is not a workable solution if one is going to implement first-order logic. (If you try, you will just invent a little meta-language on top of first-order logic and then use that language instead, so what purpose did first-order logic serve?)

We can do without the meta-theorem by introducing Russell's description operator $\iota x{:}A \,.\, \phi(x)$, read as "the unique $x : A$ such that $\phi(x)$",

$$ \frac{\vdash \exists! x \in A \,.\, \phi(x)}{\vdash (\iota x{:}A \,.\, \phi(x)) : A} \qquad \frac{\vdash \exists! x \in A \,.\, \phi(x)}{\vdash \phi(\iota x{:}A \,.\, \phi(x))} $$

The $\iota$ operator is less commital than Hilbert's $\epsilon x{:}A . \phi(x)$, read as "any $x : A$ such that $\phi(x)$" because the latter implies the axiom of choice and excluded middle.

If you add meta-level definitions of symbols, then $\iota$ just might be workable. (Without $\iota$ and using only symbol definitions in ZFC you cannot define any interesting term constructors because ZFC only has one relational symbol $\in$.) Notice that $\iota$ and $\epsilon$ modify first-order logic in a fundamental way by allowing formulas inside terms.

Answer 2

If you're mainly interested in set theories based on FOL, then you don't need to know concrete details of what existing systems do, but rather you only need to know and understand the precise mechanism of definitorial expansion, which is a totally generic conservative extension of an FOL theory. For a system to be user-friendly, you would need such a mechanism to be on-the-fly, and indeed this is easy to do in any Fitch-style system such as this one. You might notice that the rules under "Definitorial Expansion" in that post cover the cases for predicate/function-symbols but not for constant-symbols. This is because the ∃elim rule already covers the latter! This is not entirely a coincidence; there are two main traditions for Fitch-style systems. One features this kind of ∃elim rule, whereas the other instead has something like ( ∃x∈S ( Q(x) ) ; ∀x∈S ( Q(x) ⇒ A ) ⊢ A ). These two traditions are briefly discussed in this paper (which calls them EI and ∃E respectively).

Given this, I disagree with the other answer that implicitly suggests that this kind of mechanism goes beyond FOL, since it is the natural and obvious thing to do in the same manner as for the ∃elim rule, when it comes to a Fitch-style system. Yes, having definitorial expansion of course comes at the cost of making the system slightly more complicated than the base system, but notice that whenever any logician says they are using ZFC they in fact mean that they are using ZFC plus on-the-fly definitorial expansion (or something essentially equivalent). Nobody uses plain ZFC, nor do they consider what they are using as 'beyond' FOL. In fact, many set theorists think of ZFC classes as "just formulae over ZFC with one free variable", and use them in exactly the same manner as is supported by on-the-fly definitorial expansion. (One can reify these by moving to MK set theory, but that is no longer ZFC, and set theorists who work in MK set theory also use definitorial expansion over MK...)

Answer 3

As Andrej mentioned you can define a little meta-language which compiles to first order logic.

I've been experimenting with this approach and it's simpler and better than you might expect but just not really suited to a set theory style.

You can define a little term language like

$$ e \mathrel{::=} x \mid \emptyset \mid \{ e_1 , e_2 \} \mid \bigcup e \mid \mathop{\mathcal{P}} e $$

And define an inductive predicate on variables

$$ \begin{align*} x \mathrel{\textbf{is}} y \iff & x = y \\ x \mathrel{\textbf{is}} \emptyset \iff &\forall y, y \notin x \\ x \mathrel{\textbf{is}} \{ e , e' \} \iff & \forall y, y \in x \leftrightarrow (y \mathrel{\textbf{is}} e \vee y \mathrel{\textbf{is}} e') \end{align*}$$

And so on. Basically you write a compiler.

Then you inductively prove a meta theorem that all terms are unique and exist.

$$ \vdash \exists! x. x \mathrel{\textbf{is}} e $$

However, after you gain enough power there's not really any benefit over a meta definition of terms directly as the subset of predicates that uniquely define sets.

$$ \{ P \mid [\top \vdash \exists! x. P] \} $$

Once you allow some form of definite description you lose the ability to compute decidable equality or normal forms. So you lose much of the benefit of having some sort of term language and might as well work directly with predicates equipped with proofs they uniquely define sets.

If you wanted to keep decidable equality and normal forms you would basically end up compiling some form of type theory to set theory and most versions of set theory really aren't very well suited to this.

So it's possible to define meta-languages of terms which compile to predicates and these types of DSLs could be very useful. However, any DSL which gives you the full power of set theory (some form of iota) won't be very useful over working with predicates directly.

Also you have all the usual problems of DSLs and compilers. I like parametric higher order abstract syntax for rapid prototyping of much of what I do but I can imagine it would be an extreme headache plumbing through environments explicitly with de Bruijn levels. Metatheoretically proving stuff about your DSL also seems pretty painful.