2
$\begingroup$

In page 4 of Gödel's book The Consistency Of The Axiom Of Choice and Of The Generalized Continuum Hypothesis With The Axioms Of Set Theory, Gödel defined the $n$-tuple as

  1. $\langle x \rangle = x$;
  2. $\langle x_1, \ldots, x_n\rangle = \langle x_1, \langle x_2, \ldots, x_n \rangle\rangle$ for each $n \in \mathbb N$.

He defines $n$-tuples in a different order, while, customarily, we'd rather accept $\langle x_1, \ldots, x_{n}\rangle = \langle \langle x_1, \ldots, x_{n-1} \rangle, x_{n}\rangle$. But let's ignore this trivial difference.

I know this is a 1-based inductive definition. In my notes (invoking MK), I proved so called finite recursion theorem; it is a theorem without the limit case (the 3rd case) of transfinite recursion and the domain is restricted in $\mathbb N$, which states:

Let $\mathscr U$ denotes the universal class $\mathscr U = \{x: \exists X: x \in X\}$. Given a function $\phi: \mathscr U \to \mathscr U$, then there is a unique function $f: \mathbb N \to \mathscr U$ such that

  1. Base case: $f(0) = c$;
  2. Successor case: $f(n^+) = \phi(f(n))$ for each $n \in \mathbb N$.

This theorem can be easily proven (the proof is quite similar to that of the transfinite version), and gives the reason why some terms can be defined inductively. By this theorem, the ellipsis notation (arbitrarily finite case) can be well-defined.

I know MK and NBG are different system, but I'm sure that if (JUST if) inductive definitions must be supported by the definition of natural numbers, then so is Gödel's definition on $n$-tuples.

So, why can Gödel define such an inductive concept before the set theoretical definition of natural numbers is verified in the book? Or, does he used Peano's natural numbers as the foundation of his system implicitly?


This is a question I confused for a long time. So, in my notes, I avoid using ellipsis notation or natural index as possible as I can until the set theoretical $(\mathbb N, +, \times, \le)$ is introduced – even if I state that the Peano's axioms are invoked in the logic system, I have no idea when can I use them in set theory – though I know sometimes I can't.

$\endgroup$

1 Answer 1

5
$\begingroup$

It depends on whether you wish to define a finite ordered tuple, say, a $3$-tuple $w=(x,y,z)$ at the metalanguage level or at the object language level.

In the first case, saying $w=(x,y,z)$ is simply as a shorthand for a huge well-formed formula $\varphi(x,y,z,w)$ that says "$w$ is a non-empty set and its elements are either equal to the set that contains only $x$ or equal to the set with elements that contains $x$ and ...you are supposed to describe $(y,z)$ here..."

In the second case, saying $w=(x,y,z)$ means something else depending on your definition of a (formal) ordered pair as a set. For example,

  • If you define an $n$-tuple over a set $S$ as a function [$\ast$] from the von Neumann ordinal $n$ to the set $S$, $w=(x,y,z)$ means that "$w$ is a function whose domain is the set $\{0,1,2\}$ and it takes the values $x$, $y$ and $z$ at the points $0$, $1$ and $2$ respectively". Clearly I am not going to write down the very long formula that describes this situation, but we can do that if we are patient enough.
  • If you define finite ordered pairs by the recursion theorem, as you do in the question, then $w$ will be a specific element of the image of the function that you prove exists by the recursion theorem.

What is the difference between these two approaches? In the first case, the informal recursion takes place at a syntactic level as a part of your symbol manipulation apparatus. Therefore, not only do you not need to justify this recursion, you cannot justify it within your system by any theorem. Think of it as a recursive computer program, where the shorthand $w=(x,y,z)$ commands the symbol manipulator:

  1. Write the formula that says "$w$ has two elements, and the elements of $w$ are either $\{x\}$ or..."
  2. Now write the formula that says "...or they are... $\{x,(y,z)\}$"

but now the symbol manipulator needs to repeat the process because of $(y,z)$ until it terminates.

In the second case, you are defining an ordered tuple as a special type of objects in your language rather than a shorthand for a formula that holds between several objects. If you are doing this by a formal recursive definition, then you do need some variation of the recursion theorem to justify this definition, as you expected.


[$\ast$]: The most common set-theoretic definition of a function requires you to already have the notion of "ordered pair". Therefore, you may ask whether there is a circularity here. There is not. In order to define $n$-tuples at the object language level as functions, you need to already have ordered pairs at the syntactic level. After having this general definition of an $n$-tuple, you can also define a (formal) ordered pair, i.e. a $2$-tuple, which as you can see is a completely different object than the ordered pair at the syntactic level. Therefore, depending on what you mean, $(0,1)$ may be the set $\{\{0\},\{0,1\}\}$ but it may also be the set $\{(0,0),(1,1)\}=\{\{\{0\}\},\{\{1\}\}\}$.

$\endgroup$
4
  • $\begingroup$ To be fair, in both cases we define ordered pair as objects in our system. But I don't know how to articulate the difference that I took so long to explain... $\endgroup$
    – Burak
    Commented Feb 26 at 12:26
  • $\begingroup$ Thank you @Burak, I read carefully hours later! $\endgroup$ Commented Feb 27 at 5:43
  • $\begingroup$ Thank you @Burak, I have another question within the context of metalanguage: I was told that in logic functions are a primitive notion. But, as a tuple $\omega = (x,y)$ can be considered a short hand of a predicate $\varphi = (x,y,z)$, is it possible to define functions in this way? Say: A predicate $\varphi(x,y)$ is a function (with variable $x$ and dependent value $y$) if and only if for any $x$ there is at most one $y$ such that $\varphi(x,y)$ holds true? In this case, can "function" be defined in the term of "predicate"? $\endgroup$ Commented Feb 28 at 8:05
  • $\begingroup$ @WenchuanZhao: Yes. Indeed, such functions are frequently used, e.g. in the statement of the Replacement Axiom of ZFC. $\endgroup$
    – Burak
    Commented Feb 28 at 20:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .