Skip to main content
Mathematics LibreTexts

5.12: Coding Deductions

  • Page ID
  • \( \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}}\)

    \( \newcommand{\vectorA}[1]{\vec{#1}}      % arrow\)

    \( \newcommand{\vectorAt}[1]{\vec{\text{#1}}}      % arrow\)

    \( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

    \( \newcommand{\vectorC}[1]{\textbf{#1}} \)

    \( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)

    \( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)

    \( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)

    \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

    \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)

    \(\newcommand{\avec}{\mathbf a}\) \(\newcommand{\bvec}{\mathbf b}\) \(\newcommand{\cvec}{\mathbf c}\) \(\newcommand{\dvec}{\mathbf d}\) \(\newcommand{\dtil}{\widetilde{\mathbf d}}\) \(\newcommand{\evec}{\mathbf e}\) \(\newcommand{\fvec}{\mathbf f}\) \(\newcommand{\nvec}{\mathbf n}\) \(\newcommand{\pvec}{\mathbf p}\) \(\newcommand{\qvec}{\mathbf q}\) \(\newcommand{\svec}{\mathbf s}\) \(\newcommand{\tvec}{\mathbf t}\) \(\newcommand{\uvec}{\mathbf u}\) \(\newcommand{\vvec}{\mathbf v}\) \(\newcommand{\wvec}{\mathbf w}\) \(\newcommand{\xvec}{\mathbf x}\) \(\newcommand{\yvec}{\mathbf y}\) \(\newcommand{\zvec}{\mathbf z}\) \(\newcommand{\rvec}{\mathbf r}\) \(\newcommand{\mvec}{\mathbf m}\) \(\newcommand{\zerovec}{\mathbf 0}\) \(\newcommand{\onevec}{\mathbf 1}\) \(\newcommand{\real}{\mathbb R}\) \(\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}\) \(\newcommand{\laspan}[1]{\text{Span}\{#1\}}\) \(\newcommand{\bcal}{\cal B}\) \(\newcommand{\ccal}{\cal C}\) \(\newcommand{\scal}{\cal S}\) \(\newcommand{\wcal}{\cal W}\) \(\newcommand{\ecal}{\cal E}\) \(\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}\) \(\newcommand{\gray}[1]{\color{gray}{#1}}\) \(\newcommand{\lgray}[1]{\color{lightgray}{#1}}\) \(\newcommand{\rank}{\operatorname{rank}}\) \(\newcommand{\row}{\text{Row}}\) \(\newcommand{\col}{\text{Col}}\) \(\renewcommand{\row}{\text{Row}}\) \(\newcommand{\nul}{\text{Nul}}\) \(\newcommand{\var}{\text{Var}}\) \(\newcommand{\corr}{\text{corr}}\) \(\newcommand{\len}[1]{\left|#1\right|}\) \(\newcommand{\bbar}{\overline{\bvec}}\) \(\newcommand{\bhat}{\widehat{\bvec}}\) \(\newcommand{\bperp}{\bvec^\perp}\) \(\newcommand{\xhat}{\widehat{\xvec}}\) \(\newcommand{\vhat}{\widehat{\vvec}}\) \(\newcommand{\uhat}{\widehat{\uvec}}\) \(\newcommand{\what}{\widehat{\wvec}}\) \(\newcommand{\Sighat}{\widehat{\Sigma}}\) \(\newcommand{\lt}{<}\) \(\newcommand{\gt}{>}\) \(\newcommand{\amp}{&}\) \(\definecolor{fillinmathshade}{gray}{0.9}\)

    It is probably difficult to remember at this point of our journey, but our goal is to prove the Incompleteness Theorem, and to do that we need to write down an \(\mathcal{L}_{NT}\)-sentence that is true in \(\mathfrak{N}\), the standard structure, but not provable from the axioms of \(N\). Our sentence, \(\theta\), will "say" that \(\theta\) is not provable from \(N\), and in order to "say" that, we will need a formula that will identify the (Gödel numbers of the) formulas that are provable from \(N\). To do that we will need to be able to code up deductions from \(N\), which makes it necessary to code up sequences of \(\mathcal{L}_{NT}\)-formulas.

    We have been pretty careful with our coding up to this point. If you check, every Gödel number that we have used has been even, with the exception of 3, which is the garbage case in Definition 5.7.1. We will now use numbers with smallest prime factor 5 to code sequences of formulas.

    Suppose that we have the sequence of formulas

    \[D = \left( \phi_1, \phi_2, \ldots, \phi_k \right).\]

    We will define the sequence code of \(D\) to be the number

    \[\ulcorner D \urcorner = 5^{\ulcorner \phi_1 \urcorner} 7^{\ulcorner \phi_2 \urcorner} \cdots p_{k+2}^{\ulcorner \phi_k \urcorner}.\]

    So, the exponent on the \(\left( i + 2 \right)^\text{nd}\) prime is the Gödel number of the \(i^\text{th}\) element of the sequence. You are asked in the Exercises to produce several useful \(\mathcal{L}_{NT}\)-formulas relating to sequence codes.

    We will be interested in using sequence codes to code up deductions from \(N\). If you look back at the definition of a deduction (Definition 2.2.1), you will see that to check if a sequence is a deduction, we need only check that each entry is either an axiom or follows from previous lines of the deduction via a rule of inference. So to say that \(c\) codes up a deduction from \(N\), we want to be able to say, for each entry \(e\) at position \(i\) of the deduction coded by \(c\),

    \[AxiomOfN \left( e \right) \lor LogicalAxiom \left( e \right) \lor RuleOfInference \left( c, e, i \right).\]

    The first two of these we have already developed. The last major goal of this section (and this chapter) is to flesh out the details of a \(\Delta\)-definition of a formula that recognizes when an entry in a deduction is justified by one of our rules of inference.

    As you recall from Section 2.4, there are two types of rules of inference: propositional consequence and quantifier rules. The latter of these is easiest to \(\Delta\)-define, so we deal with it first.

    The rule of inference (QR) is Definition 2.4.6, which says that if \(x\) is not free in \(\psi\), then the following are rules of inference:

    \[\left( \{ \psi \rightarrow \phi \}, \psi \rightarrow \left( \forall x \phi \right) \right) \\ \left( \{ \phi \rightarrow \psi \}, \left( \exists x \phi \right) \rightarrow \psi \right).\]

    If we look at the first of these, we see that if \(e\) is an entry in a code for a deduction, and \(e = \ulcorner \psi \rightarrow \left( \forall x \phi \right) \urcorner\), then \(e\) is justified as long as there is an earlier entry in the deduction that codes up the formula \(\psi \rightarrow \phi\), assuming that \(x\) is not free in \(\psi\). So all we have to do is figure our a way to say this.

    We will write the formula \(QRRule1 \left( c, e, i \right)\), where \(c\) is the code of the deduction, and \(e\) is the entry at position \(i\) that is being justified by the first quantifier rule. In the following, \(f\) is playing the role of \(\ulcorner \psi \urcorner\), while \(g\) is supposed to be \(\ulcorner \phi \urcorner\):

    \(QRRule1 \left( c, e, i \right) =\)

    \[SequenceCode \left( c \right) \land IthSequenceElement \left( e, i, c \right) \land \\ \left( \exists x, f, g < c \right) \left[ Formula \left( f \right) \land Formula \left( g \right) \land Variable \left( x \right) \land \\ \neg Free \left( x, f \right) \land \\ e = \bar{2}^\bar{4} \bar{3}^{\bar{2}^\bar{2} \bar{3}^{Sf} + 1} \bar{5}^{\bar{2}^\bar{6} \bar{3}^{Sx} \bar{5}^{Sy} + 1} \land \\ \left( \exists j < i \right) \left( \exists e_j < c \right) \left( IthSequenceElement \left( e_j, j, c \right) \land \\ e_j = \bar{2}^\bar{4} \bar{3}^{\bar{2}^\bar{2} \bar{3}^{Sf} + 1} \bar{5}^{Sg} \right) \right].\]

    After you write out \(QRRule2\) in the Exercises, it is obvious to define

    \(QRRule \left( c, e, i \right) =\)

    \[QRRule1 \left( c, e, i \right) \lor QRRule2 \left( c, e, i \right).\]

    Now we have to address propositional consequence. This will involve some rather tricky coding, so hold on tight as we review propositional logic.

    Assume that \(D\) is our deduction, and \(D\) is the sequence of formulas

    \[\left( \alpha_1, \alpha_2, \alpha_3, \ldots, \alpha_k \right).\]

    Notice that entry \(\alpha_i\) of a deduction is justified as a propositional consequence if and only if the formula

    \[\beta = \left( \alpha_1 \land \alpha_2 \land \cdots \land \alpha_{i-1} \right) \rightarrow \alpha_i\]

    is a tautology.

    Now, as we discussed in Section 2.4, in order to decide if a first-order formula \(\beta\) is a tautology, we must take \(\beta\) and find the propositional formula \(\beta_P\). Then if \(\beta_P\) is

    \[\left[ \left( \alpha_1 \right)_P \land \left( \alpha_2 \right)_P \land \cdots \land \left( \alpha_{i-i} \right)_P \right] \rightarrow \left( \alpha_i \right)_P,\]

    we must show any truth assignment that makes \(\left( \alpha_1 \right)_P\) through \(\left( \alpha_{i-1} \right)_P\) true must also make \(\left( \alpha_i \right)_P\) true.

    As outlined in Section 2.4, to create a propositional version of a formula, we first must find the prime components of that formula, where a prime component is a subformula that is either universal and not contained in any other universal subformula, or atomic and not contained in any universal formula. Rather than explicitly writing out a \(\Delta\)-formula that identifies the pairs \(\left( u, v \right)\) such that \(u\) is the Gödel number of a prime component of the formula with Gödel number \(v\), let us write down a recursive definition of this set of formulas, and we will leave it to the reader to find the minor modification of Theorem 5.10.2, which will guarantee that this set of Gödel numbers is representable.

    Definition 5.12.1.

    If \(\beta\) and \(\gamma\) are \(\mathcal{L}_{NT}\)-formulas, \(\gamma\) is said to be a prime component of \(\beta\) if:

    1. \(\beta\) is atomic and \(\gamma = \beta\), or
    2. \(\beta\) is universal and \(\gamma = \beta\), or
    3. \(\beta\) is \(\neg \alpha\) and \(\gamma\) is a prime component of \(\alpha\), or
    4. \(\beta\) is \(\alpha_1 \lor \alpha_2\) and \(\gamma\) is a prime component of either \(\alpha_1\) or \(\alpha_2\).
    proposition 5.12.2.

    The set


    \[\{ \left( u, f \right) | u = \ulcorner \gamma \urcorner \: \text{and} \: f = \ulcorner \beta \urcorner \: \text{and} \: \gamma \: \text{is a prime component of} \: \beta \: \text{for some} \: \mathcal{L}_{NT} \text{-formulas} \: \gamma \: \text{and} \: \beta \}\]

    is representable and has \(\Delta\)-definition \(PrimeComponent \left( u, f \right)\).


    Theorem 5.10.2.

    Now we will code up a canonical sequence of all of the prime components of \(\alpha_1\) through \(\alpha_i\). We will say \(r\) codes the PrimeList for the first \(i\) entries of the deduction coded by \(c\) if each element coded by \(r\) is a prime component of one of the first \(i\) entries of the deduction coded by \(c\), \(r\)'s elements are distinct, each prime component of each of the first \(i\) entries of the deduction coded by \(c\) is among the entries in \(r\), and if \(s\) is a smaller code number, \(s\) is missing one of these prime components:

    \(PrimeList \left( c, i, r \right) =\)

    \[SequenceCode \left( c \right) \land CodeNumber \left( r \right) \land \\ \left( \exists l < r \right) \left[ Length \left( r, l \right) \land \\ \left( \forall m, n \leq l \right) \left( \forall e_m, e_n < r \right) \\ \left( IthElement \left( e_m, m, r \right) \land IthElement \left( e_n, n, r \right) \right) \rightarrow \\ \left( \left( \exists k \leq i \right) \left( \exists f_k \leq c \right) IthSequenceElement \left( f_k, k, c \right) \land \\ PrimeComponent \left( e_m, f_k \right) \land \\ \left[ \left( m \neq n \right) \rightarrow \left( e_m \neq e_n \right) \right] \right) \land \\ \left[ \left( \forall k \leq i \right) \left( \forall f_k \leq c \right) \left( \forall u \leq f_k \right) \left( IthSequenceElement \left( f_k, k, c \right) \land \\ PrimeComponent \left( u, f_k \right) \rightarrow \\ \left( \exists m < l \right) IthElement \left( u, m, r \right) \right) \right] \right] \land \\ \left( \forall s < r \right) \left( CodeNumber \left( s \right) \rightarrow \\ \left( \exists k \leq i \right) \left( \exists f_k \leq c \right) \left( \exists u \leq f_k \right) \left[ IthSequenceElement \left( f_k, k, c \right) \land \\ PrimeComponent \left( u, f_k \right) \land \\ \left( \forall m < s \right) \left( \neg IthElement \left( u, m, s \right) \right) \right] \right)\]

    To decide if \(\beta\) is a tautology, we need to assign all possible truth values to all of the prime components in our list, and then evaluate the truth of each \(\alpha_i\) under a given truth assignment. So the next thing we need to do is find a way to code up an assignment of truth values to all of the prime components of all the \(\alpha_i\)'s. We will say that \(v\) codes up a truth assignment if \(v\) is the code number of a sequence of the right length and all of the elements coded by \(v\) are either 0 (for false) or 1 (for true).

    \(TruthAssignment \left( c, i, r, v \right) =\)

    \[PrimeList \left( c, i, r \right) \land CodeNumber \left( v \right) \land \\ \left( \exists l < r \right) \left( Length \left( r, l \right) \land Length \left( v, l \right) \land \\ \left( \forall i \leq l \right) \left( \forall e < v \right) \left( IthElement \left( e, i, v \right) \rightarrow \\ \left[ e = \bar{0} \lor e = \bar{1} \right] \right) \right).\]

    Now, given a truth assignment for the prime components of \(\alpha_1\) through \(\alpha_i\), coded up in \(v\), we need to be able to evaluate the truth of each formula \(\alpha_n\) under that assignment. To do this we will need to be able to evaluate the truth value of a single formula.

    Suppose that we first look at an example. Here is a formula construction sequence that ends with some formula \(\alpha\):

    \[\left( 0 < x, x< y, \left( 0 < x \lor x < y \right), \neg \left( 0 < x \right), \left( \forall x \right) \left( 0 < x \lor x < y \right), \left[ \left( \forall x \right) \left( 0 < x \lor x < y \right) \lor \left( \neg 0 < x \right) \right] \left( \alpha \right) \right).\]

    Let us assume that the PrimeList we are working with is

    \[\left( \left( \forall x \right) \left( 0 < x \lor x < y \right), 0 < x \right)\]

    and the chosen truth assignment for our PrimeList is

    \[\left( 0.1 \right).\]

    To assign the truth value to \(\alpha\), we follow along the construction sequence. When we see an entry that is in the PrimeList, we assign that entry the corresponding truth value from our truth assignment. If the entry in the construction sequence is not a prime component, one of three things might be true:

    1. The entry might be universal, in which case we assign it truth value 2 (for undefined).
    2. The entry might be an atomic formula that ends up inside the scope of a quantifier in \(\alpha\). Again, we use truth value 2.
    3. The entry might be the denial of or disjunction of earlier entries in the construction sequence. In this case we can figure out its truth value, always using 2 if any of the parts have truth value 2.

    So to continue our example from above, the sequence of truth values would be

    \[\left( 1, 2, 2, 0, 0, 0 \right).\]

    Exercise 7 asks you to write a \(\Delta\)-formula \(Evaluate \left( e, r, v, y \right)\), where you should assume that \(e\) is the Gödel number for a formula \(\alpha\), \(r\) is a code for a list including all of the prime components of \(\alpha\), \(v\) is a TruthAssignment for \(r\), and \(y\) is the truth value for \(\alpha\), given the truth assignment \(v\). Exercise 8 also concerns this formula.

    Now, knowing how to evaluate the truth of a single formula \(\alpha\), we will be able to decide if \(\alpha_i\), the \(i^\text{th}\) element of the alleged deduction that is coded by \(c\), can be justified by the propositional consequence rule. Recall that we need only check whether

    \[\left( \alpha_1 \land \alpha_2 \land \cdots \land \alpha_{i-1} \right) \rightarrow \alpha_i\]

    is a tautology. To do this, we need only see whether any truth assignment that makes \(\alpha_1\) through \(\alpha_{i-1}\) true also makes \(\alpha_i\) true. Here is the \(\Delta\)-formula that says this, where \(c\) codes the alleged deduction, and \(e\) is supposed to be the code for the \(i^\text{th}\) entry in the deduction, the entry that is to be justified by an appeal to the rule PC:

    \(PCRule \left( c, e, i \right) =\)

    \[IthSequenceElement \left( e, i, c \right) \land \\ \left( \exists r < \left[ \bar{2}^{\left( c^\bar{2} \right)^{\left( c^\bar{2} \right)}} \right]^{c^\bar{3}} \right) \\ \left( \forall v < \left( \left[ \bar{2}^{\left( c^\bar{2} \right)^{\left( c^\bar{2} \right)}} \right]^{\overline{\ulcorner \bar{1} \urcorner}} \right)^{c^\bar{2}} \right) \\ \left( \left[ PrimeList \left( c, i, r \right) \land TruthAssignment \left( c, i, r, v \right) \right] \rightarrow \\ \left[ \left( \left( \forall j < i \right) \left( \exists e_j < c \right) \\ \left( IthSequenceElement \left( e_j, j, c \right) \land Evaluate \left( e_j, r, v, \bar{1} \right) \right) \right) \\ Evaluate \left( e, r, v, \bar{1} \right) \right] \right).\]

    Now, to know that this works, we must justify the bounds that we have given for \(r\) and \(v\). The number \(r\) is supposed to code the list of prime components among the first \(i\) elements of the deduction \(c\). So \(r\) is of the form \(5^{\ulcorner \gamma_1 \urcorner} 7^{\ulcorner \gamma_2 \urcorner} \cdots p_{k+2}^{\ulcorner \gamma_k \urcorner}\), where the prime components are \(\gamma_1\) through \(\gamma_k\). First, we need to get a handle on the number of prime components there are. Since \(c\) is the code for the deduction, there are fewer than \(c\) formulas in the deduction, and each of those formulas has a Gödel number that is less than or equal to \(c\). So each formula in the deduction has fewer than \(c\) symbols in it, and thus fewer than \(c\) prime components. So we have no more than \(c\) formulas, each with no more than \(c\) prime components, so there are no more than \(c^2\) prime components total in the deduction coded by \(c\). If we look at the number \(r\), we see that

    \[\begin{align} r &= 5^{\ulcorner \gamma_1 \urcorner} 7^{\ulcorner \gamma_2 \urcorner} \cdots p_{k+2}^{\ulcorner \gamma_k \urcorner} \\ &\leq 5^c 7^c \cdots p_{k+2}^c \\ &\leq 5^c 7^c \cdots p_{c^2}^c \\ &\leq \left[ 2^{\left( c^2 \right)^{\left( c^2 \right)}} \right]^{c^3}, \end{align}\]

    where the last line depends on our usual bound for the size of the \(\left( c^2 \right)th prime.

    As for \(v\), \(v\) is a code number that gives us the truth values of the various prime components coded in \(r\). Thus \(v\) is of the form \(2^{i_1} 3^{i_2} \cdots p_k^{i_k}\), where there are \(k\) prime components, and each \(i_j\) is either \(\ulcorner \bar{0} \urcorner\) or \(\left( \ulcorner \bar{1} \urcorner \right)\). By the argument above, we know there are no more than \(c^2\) prime components, so

    \[\begin{align} v &= 2^{i_1} 3^{i_2} \cdots p_k^{i_k} \\ &\leq 2^{\ulcorner \bar{1} \urcorner} 3^{\ulcorner \bar{1} \urcorner} \cdots p_{c^2}^{\ulcorner \bar{1} \urcorner} \\ &\leq \left( \left[ 2^{\left( c^2 \right)^{\left( c^2 \right)}} \right]^{\ulcorner \bar{1} \urcorner} \right)^{c^2}. \end{align}\]

    Thus we have justified the bounds given for \(r\) and \(v\) in the definition of \(PCRule \left( c, e, i \right)\). Thus we have a \(Delta\)-definition, and the set \(PCRULE\) is representable.

    Now we have to remember where we were after we defined \(QRRule\). We are thinking of \(c\) as coding an alleged deduction from \(N\), and we need to check all of the entries of \(c\) to see if they are legal. We have already written \(\Delta\)-formulas \(LogicalAxiom\) and \(AxiomOfN\), and we are working on the rules of inference. The quantifier rules were relatively easy, so we then wrote a \(\Delta\)-formula \(PCRule \left( c, e, i \right)\) that is true if and only if \(e\) is the \(i^\text{th}\) entry of the deduction \(c\) and can be justified by the rule PC.

    At last, we are able to decide if \(c\) is the code for a deduction from \(N\) of a formula with Gödel number \(f\):

    \(Deduction \left( c, f \right) =\)

    \[SequenceCode \left( c \right) \land Formula \left( f \right) \land \\ \left( \exists l < c \right) \left( SequenceLength \left( c, l \right) \land IthSequenceElement \left( f, l, c \right) \land \\ \left( \forall i \leq l \right) \left( \forall e < c \right) \left[ IthSequenceElement \left( e, i, c \right) \rightarrow \\ \left( LogicalAxiom \left( e \right) \lor AxiomOfN \left( e \right) \lor \\ QRRule \left( c, e, i \right) \lor PCRule \left( c, e, i \right) \right) \right] \right).\]

    This formula represents the set \(DEDUCTIONS \subseteq \mathbb{N}^2\) and shows that \(DEDUCTION\) is a representable set. Given Church's Thesis, this makes formal the ideas of Chapter 2, where it was suggested that we ought to be able to program a computer to decide if an alleged deduction is, in fact, a deduction. We said earlier that if a computer could decide whether an alleged axiom was an axiom, in other words, if the collection of axioms was representable, and whether a use of a rule of inference was legitimate, then it could check whether an alleged deduction was ok. This brings us to a slightly sticky point.

    You will notice that we have carefully been using bounded quantification and that the formula \(Deduction \left( c, f \right)\) above is a \(\Delta\)-formula. But that depends on the fact that the collection of axioms \(N\) has a \(\Delta\)-definition, which is more restrictive than just saying that the collection of axioms is a representable set. So perhaps, if \(A\) is a representable set of axioms that does not have a \(\Delta\)-definition, we have a problem. Fortunately, this is not the case.

    Suppose that \(A\) is a representable set of axioms. We know, via Exercises 13 and 14 of Section 5.3, that \(A\) has a numeralwise determined definition \(AxiomOfA \left( e \right)\). Furthermore, if we define the formula \(Deduction_A\) as above, replacing \(AxiomOfN\) with \(AxiomOfA\), then \(Deduction_A\) is a numeralwise determined formula that defines the set \(DEDUCTION_A\), and so the collection of codes of deductions from our representable set of axioms \(A\) is itself representable and our computer can, in fact, check whether an alleged deduction from \(A\) is, in fact, a deduction from A.

    If you keep the equivalence between "computer-decidable" and representable in your head, we will say more about this in Chapters 6 and 7.


    1. Write a \(\Delta\)-formula \(SequenceCode \left( c \right)\) that is true in \(\mathfrak{N}\) if and only if \(c\) is the code of a sequence of \(\mathcal{L}_{NT}\)-formulas.
    2. Write a \(\Delta\)-formula \(SequenceLength \left( c, l \right)\) that is true in \(\mathfrak{N}\) if and only if \(c\) is a sequence code of a sequence of length \(l\).
    3. Write out a \(\Delta\)-formula \(IthSequenceElement \left( e, i, c \right)\) that is true in \(\mathfrak{N}\) if and only if \(c\) is a sequence code and the \(i^\text{th}\) element of the sequence coded by \(c\) has Gödel number \(e\).
    4. Write out a \(\Delta\)-formula \(QRRule2 \left( c, e, i \right)\) that will be true in \(\mathfrak{N}\) if \(e\) is the \(i^\text{th}\) entry in the sequence coded by \(c\) and is justified by the second quantifier rule.
    5. Here is your average, ordinary tautology:
      \[\phi \left( x, y \right) \: \text{is} \: \left[ \left[ \forall x P \left( x \right) \right] \rightarrow \left( Q \left( x, y \right) \rightarrow \left[ \forall x P \left( x \right) \right] \right) \right].\]
      Find a construction sequence for \(\phi\). Make a list of the prime components of \(\phi\). Pretending that your list of prime components is the prime list for \(\phi\), find all possible truth assignments for \(\phi\) and use the truth assignments to evaluate the truth of \(\phi\) under your assignments. If all goes well, every time you evaluate the truth of \(\phi\), you will get: True.
    6. Repeat Exercise 5 with the following formulas, which are not (necessarily) guaranteed to be tautologies:
      (a) \(\left( \forall x \right) \left( x < y \rightarrow x < y \right)\)
      (b) \(\left( \forall x \right) \left( x < y \right) \rightarrow \left( \forall x \right) \left( x < y \right)\)
      (c) \(\left( A \left( x \right) \lor B \left( y \right) \right) \lor \neg B \left( x \right)\)
      (d) \(\left( A \left( x \right) \lor B \left( y \right) \right) \rightarrow \left[ \left( \forall x \right) \left( \forall y \right) \left( A \left( x \right) \lor B \left( y \right) \right) \right]\)
      (e) \(\left[ \left( \forall x \right) \left( \forall y \right) \left( A \left( x \right) \lor B \left( y \right) \right) \right] \rightarrow \left( A \left( x \right) \lor B \left( y \right) \right)\)
    7. Write out the \(\Delta\)-formula \(Evaluate \left( e, r, v, y \right)\), as outlined in the text. You will need to think about formula construction sequences, as you did in Exercise 6 in Section 5.8.
    8. Show by induction on the longest of the two construction sequences that if \(d_1\) and \(d_2\) are codes for two construction sequences of \(\alpha\), and if \(Evaluate \left( d_1, r, v, y_1 \right)\) and \(Evaluate \left( d_2, r, v, y_2 \right)\) are both true, then \(y_1\) and \(y_2\) are equal. Thus, the truth assigned to \(\alpha\) does not depend upon the construction sequence chosen to evaluate the truth.

    This page titled 5.12: Coding Deductions 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.