Skip to main content
Mathematics LibreTexts

5.10: Definitions by Recursion are Representable

  • Page ID
    10070
  • \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)\(\newcommand{\AA}{\unicode[.8,0]{x212B}}\)

    If you look at the definition of a term (Definition 1.3.1), the definition of formula (Definition 1.3.3), the definition of \(u_t^x\) (Definition 1.8.1), and the definition of (Definition 1.8.2), you will notice that all of these definitions were definitions "by recursion". For example, in definition of a term, you see the phrase

    \(\ldots t\) is \(f t_1 t_2 \ldots t_n\), where \(f\) is an \(n\)-ary function symbol of \(\mathcal{L}\) and each of the \(t_i\) are terms of \(\mathcal{L}\)

    so a term can have constituent parts that are themselves terms. In the last two sections we have used the device of construction sequences to show that the sets \(TERM\), \(FORMULA\), \(TERMSUB\), and \(SUB\) are representable sets. In this section we outline a proof that all such sets of strings, defined "by recursion", give rise to sets of Gödel numbers that are representable. It will be clear from our exposition that a more general statement of our theorem could be proved, but what we present will be sufficient for our needs.

    Definition 5.10.1.

    A string of symbols \(s\) form a first-order language \(\mathcal{L}\) is called an expression if \(s\) is either a term of \(\mathcal{L}\) or a formula of \(\mathcal{L}\).

    theorem 5.10.2.

    Suppose that we have a set of \(\mathcal{L}_{NT}\)-expressions, which we will call \(\textit{Set}\), defined as follows: An expression \(s\) is an element of \(\textit{Set}\) if and only if:

    1. \(s\) is an element of \(\textit{BaseCaseSet}\), or
    2. There is an expression \(t\), a proper substring of \(s\), such that \(\left( t, s \right)\) is an element of \(\textit{ConstructionSet}\).

    If the sets of strings \(\textit{BaseCaseSet}\) and \(\text{ConstructionSet}\) give rise to sets of Gödel numbers \(BASECASESET\) and \(CONSTRUCTIONSET\) that are defined by \(\Delta\)-formulas, then the set

    \[SET = \{ \ulcorner s \urcorner | s \in \textit{Set} \}\]

    is representable, and has a \(\Delta\)-definition \(Set\).

    Chaff: Try to keep the various typefaces straight:

    • \(\textit{Set}\) is a bunch of \(\mathcal{L}_{NT}\)-expressions - strings of symbols from \(\mathcal{L}_{NT}\).
    • \(SET\) is a set of natural numbers - the Gödel numbers of the strings in \(\textit{Set}\).
    • \(Set\) is an \(\mathcal{L}_{NT}\)-formula such that \(\mathfrak{N} \models Set \left( \bar{a} \right)\) if and only if there is an \(s \in Set\) such that \(\ulcorner s \urcorner = a\).
    Proof

    We follow very closely the proof of the representability of the set \(TERM\), which is in Section 5.8. As you worked through Exercise 6 in Section 5.8, you saw that you could prove the analogs of Lemmas 5.8.4 through 5.8.6 for formulas, so you have established the following lemma:

    lemma 5.10.3.

    Suppose that \(s\) is an \(\mathcal{L}_{NT}\)-expression and \(u\) is a substring of \(s\) that is also an expression. Then

    1. If \(\ulcorner s \urcorner = a\), then the number of symbols in \(s\) is less than or equal to \(a\).
    2. The length of the shortest construction sequence of \(s\) is less then or equal to the number of symbols in \(s\).
    3. \(\ulcorner u \urcorner < \ulcorner s \urcorner\).
    proof

    Now we can write a \(\Delta\)-definition of \(SETCONSTRUCTIONSEQUENCE\) and then use this lemma to show \(SET\) is representable:

    \(SetConstructionSequence \left( c, a \right) =\)

    \[CodeNumber \left( c \right) \land \\ \left( \exists l < c \right) \left[ Length \left( c, l \right) \land IthElement \left( a, l, c \right) \land \\ \left( \forall i \leq l \right) \left( \forall e < c \right) \left( IthElement \left( e, i, c \right) \rightarrow \\ BaseCaseSet \left( e \right) \lor \\ \left( \exists j < i \right) \left( \exists e_j < c \right) \\ \left( IthElement \left( e_j, j, c \right) \land ConstructionSet \left( e_j, e \right) \right) \right) \right].\]

    We know, by assumption, that there are \(\Delta\)-formulas \(BaseCaseSet\) and \(ConstructionSet\) that define the representable sets \(BASECASESET\) and \(CONSTRUCTIONSET\). Thus, all of the quantifiers in the definition above are bounded, and \(SetConstructionSequence\) is a \(\Delta\)-formula.

    As before we can use Lemmas 5.8.5 and 5.8.7 to bound the size of the shortest construction sequence for \(a\): By the same argument as in Section 5.8, there is a construction sequence coded by a number \(c\) such that \(c < \left( 2^{a^a} \right)^{a^2 + a}\). So we define

    \(Set \left( a \right) =\)

    \[\left( \exists c < \left( \bar{2}^{a^a} \right)^{a^\bar{2} + a} \right) SetConstructionSequence \left( c, a \right)\]

    and we have a \(\Delta\)-definition of the set \(SET\), finishing our proof.

    This is a wonderful theorem, as it saves us lots of work. Merely by noting that their definitions fit the requirements of Theorem 5.10.2, the following sets all turn out to be representable and have \(\Delta\)-definitions:

    1. \(FREE\), where \(\left( x, f \right) \in FREE\) if and only if \(x\) is the Gödel number of a variable that is free in the formula with Gödel number \(f\).
    2. \(SUBSTITUTABLE\), where \(\left( t, x , f \right) \in SUBSTITUTABLE\) if and only if \(t\) is the Gödel number of a term that is substitutable for the variable with Gödel number \(x\) in the formula with Gödel number \(f\).

    Exercises

    1. Work through the details (including the needed modification of Theorem 5.10.2) and show that both \(FREE\) and \(SUBSTITUTABLE\) are representable.
    2. Suppose that the function \(f : \mathbb{N}^{k+1} \rightarrow \mathbb{N}\) is defined as follows:
      \[\begin{align} f \left( \underset{\sim}{a}, 0 \right) &= g \left( \underset{\sim}{a} \right) \\ f \left( \underset{\sim}{a}, b + 1 \right) &= h \left( \underset{\sim}{a}, b f \left( \underset{\sim}{a}, b \right) \right), \end{align}\]
      where \(g\) and \(h\) are representable functions represented by \(\Delta\)-formulas. Show that \(f\) is a representable function. [Suggestion: One approach is to define the formula \(f ConstructionSequence \left( c, \underset{\sim}{a}, l \right)\), with the idea that the sequence coded by \(c\) will be \(\left( f \left( 0 \right), f \left( 1 \right), \ldots, f \left( l \right) \right)\). Or, you might try to fit this situation into a theorem along the lines of Theorem 5.10.2.]
    3. Use Exercise 2 to show that the following functions are representable:
      (a) The factorial function \(n !\)
      (b) The Fibonacci function \(F\), where \(F \left( 1 \right) = F \left( 2 \right) = 1\), and for \(k \geq 3\), \(F \left( k \right) = F \left( k - 1 \right) + F \left( k - 2 \right)\)
      (c) The function \(a \uparrow i\), where \(a \uparrow 0 = 1\) and \(a \uparrow \left( j + 1 \right) = a^{a \uparrow j}\) (You should also compute a few values, along the lines of \(2 \uparrow 3\), \(2 \uparrow 4\), and \(2 \uparrow 5\).)

    This page titled 5.10: Definitions by Recursion are Representable is shared under a CC BY-NC-SA 4.0 license and was authored, remixed, and/or curated by Christopher Leary and Lars Kristiansen (OpenSUNY) via source content that was edited to the style and standards of the LibreTexts platform; a detailed edit history is available upon request.