16
$\begingroup$

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)$.

$\endgroup$
6
  • 2
    $\begingroup$ In first order logic you never make definitions. And you can mechanically translate that away. On the other hand, you can always just add a constant symbol in your language, and postulate the definition as an axiom (once you proved its existence). This is what metamath does. $\endgroup$
    – Trebor
    Apr 30, 2022 at 4:06
  • 3
    $\begingroup$ Hilbert's epsilon implies the axiom of choice. You can weaken the precondition to "It exists unique ...", resulting in the inverted iota operator (or whatever name that is). $\endgroup$
    – Trebor
    Apr 30, 2022 at 4:17
  • $\begingroup$ @Trebor I would be interested in more details on the concrete approach MetaMath does. I guess you could index by axioms used but it does also seem to require theorems live in Set. $\endgroup$ Apr 30, 2022 at 16:41
  • $\begingroup$ Thoughts on adding a [choice-principle] tag? $\endgroup$
    – Couchy
    Apr 30, 2022 at 21:49
  • 1
    $\begingroup$ The formalisation of ZF set theory in Isabelle (Isabelle/ZF) uses definite descriptions in order to avoid assuming the axiom of choice. Details here: cl.cam.ac.uk/~lp15/papers/Formath/set-I.pdf $\endgroup$ May 6, 2022 at 13:50

3 Answers 3

18
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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...)

$\endgroup$
12
  • 2
    $\begingroup$ I thought I was rather explicit about the fact that mixing formulas inside terms goes beyond first-order logic, there's no point in beating around the bush on that matter. It doesn't matter whether that's a natural thing to do, for the point I was trying to make: many meta-theorems about FOL fly out of the window once it we extend it so that the stratification between terms and formulas is gone. $\endgroup$ May 1, 2022 at 15:18
  • 2
    $\begingroup$ By the way, how would you accommodate the subset notation $\{x \in A \mid \phi(x)\}$ using definitional extensions? That one has always bothered me. $\endgroup$ May 1, 2022 at 15:19
  • 2
    $\begingroup$ @AndrejBauer: My point was that logicians familiar with Fitch-style systems have always considered on-the-fly definitorial expansion for constant-symbols to be just one of the two main variants of ∃elim; they do not consider it a meta-level tool. This alone is sufficient evidence that formal FOL for these logicians is not as narrow as your post suggests. It is true that most modern logic texts describe definitorial expansion as meta-level facts, but it is also true that most of them also never give a practically usable deductive system for FOL, much less a Fitch-style system, so... $\endgroup$
    – user21820
    May 1, 2022 at 15:35
  • 1
    $\begingroup$ @AndrejBauer: Regarding set-builder notation, you are absolutely correct that set-builder notation used in ordinary mathematics is not an instance of definitorial expansion. This is also why, in the Fitch-style system I linked, I explicitly included the type-notation rule (which corresponds to the class-specification schema for ZFC). But in fact if we have definitorial expansion then we can actually do without set-builder notation without too much trouble, because we just need to apply definitorial expansion on the appropriate specification axiom (which is just ∃elim in my system). $\endgroup$
    – user21820
    May 1, 2022 at 15:40
  • 1
    $\begingroup$ We can even do without class-builder notation, by applying definitorial expansion for predicate-symbols, though if we do not use any extra syntactic sugar then it would mean that we would have to write things like "ORD(k)" instead of "k∈ORD". So in some sense definitorial expansion is all we need to work comfortably 'within' ZFC. And of course, definitorial expansion for function-symbols allows us to get Powerset and Pairing and Union as function-symbols, as well as other class-functions. $\endgroup$
    – user21820
    May 1, 2022 at 15:43
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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