- Last updated
- Save as PDF
- Page ID
- 10067
\( \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}\)
We now change our focus from looking at functions and relations on the natural numbers, where it makes sense to talk about representable sets, to functions mapping strings of \(\mathcal{L}_{NT}\)-symbols to \(\mathbb{N}\). We will establish our coding system for formulas, associating to each \(\mathcal{L}_{NT}\) formula \(\phi\) its Gödel number, \(\ulcorner \phi \urcorner\). We will make great use of the coding function \(\langle \cdot \rangle\) that we defined in Definition 4.5.3.
Definition 5.7.1.
The function \(\ulcorner \cdot \urcorner\), with domain the collection of finite strings of \(\mathcal{L}_{NT}\)-symbols and codomain \(\mathbb{N}\), is defined as follows:
\[\ulcorner s \urcorner = \begin{cases} \begin{array}{ll} \langle 1, \ulcorner \alpha \urcorner \rangle & \text{if} \: s \: \text{is} \: \left( \neg \alpha \right), \: \text{where} \: \alpha \: \text{is an} \: \mathcal{L}_{NT} \text{-formula} \\ \langle 3, \ulcorner \alpha \urcorner, \ulcorner \beta \urcorner \rangle & \text{if} \: s \: \text{is} \: \left( \alpha \lor \beta \right), \: \text{where} \: \alpha \: \text{and} \: \beta \: \text{are} \: \mathcal{L}_{NT} \text{-formulas} \\ \langle 5, \ulcorner v_i \urcorner, \ulcorner \alpha \urcorner \rangle & \text{if} \: s \: \text{is} \: \left( \forall v_i \right) \left( \alpha \right), \: \text{where} \: \alpha \: \text{is an} \: \mathcal{L}_{NT} \text{-formula} \\ \langle 7, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: = t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 9 \rangle & \text{if} \: s \: \text{is} \: 0 \\ \langle 11, \ulcorner t \urcorner \rangle & \text{if} \: s \: \text{is} \: St, \: \text{with} \: t \: \text{a term} \\ \langle 13, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: + t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 15, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: \cdot t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 17, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: E t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 19, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: < t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 2i \rangle & \text{if} \: s \: \text{is the variable} \: v_i \\ 3 & \text{otherwise.} \end{array} \end{cases}\]
Notice that each symbol is associated with its symbol number, as set out in Table 5.1.
Example 5.7.2:
Just for practice, let's find \(\ulcorner 0 \urcorner\). Just from the chart above, \(\ulcorner 0 \urcorner = \langle 9 \rangle = 2^{10} = 1024\). To look at another example, look at \(\ulcorner 0 = 0 \urcorner\). Working recursively,
\[\begin{align} \ulcorner = 00 \urcorner &= \langle 7, \ulcorner 0 \urcorner, \ulcorner 0 \urcorner \rangle \\ &= \langle 7, 1024, 1024 \rangle \\ &= 2^8 3^{1025} 5^{1025} \end{align}\]
Exercise 3 asks you to investigate some of the subtleties of coding as it relates to this last example.
Example 5.7.3:
This is a neat function, but the numbers involved get really big, really fast. Suppose that we work out the Gödel number for the formula \(\phi\), where \(\phi\) is \(\left( \neg = 0S0 \right)\).
Since \(\phi\) is a denial, the definition tells us that
\[\ulcorner \phi \urcorner \: \text{is} \: \langle 1, \urcorner = 0S0 \urcorner \rangle = 2^2 3^{\ulcorner = 0S0 \urcorner + 1}.\]
So we need to find \(\ulcorner = 0S0 \urcorner\), and by the "equals" clause in the definition,
\[\ulcorner = 0S0 \urcorner \: \text{is} \: \langle 7, \ulcorner 0 \urcorner, \ulcorner S0 \urcorner \rangle = 2^8 3^{\ulcorner 0 \urcorner + 1} 5^{\ulcorner S0 \urcorner + 1}.\]
But \(\ulcorner 0 \urcorner = 2^{10} = 1024\), and \(\ulcorner S0 \urcorner = 2^{12} 3^{\ulcorner 0 \urcorner + 1} = 2^{12} 3^{1025}\). Now we're getting somewhere. Plugging things back in, we get
\[\ulcorner = 0S0 \urcorner \: \text{is} \: 2^8 3^{1025} 5^{\left[ 2^12 3^{1025} + 1 \right]}\]
so the Gödel number for \(\left( \neg = 0S0 \right)\) is
\[\ulcorner \phi \urcorner \: \text{is} \: 2^2 3^{\left( 2^8 3^{1025} 5^{\left[ 2^{12} 3^{1025} + 1 \right]} + 1 \right)}.\]
Chaff: To get an idea about how large this number is, consider the fact that the exponent on the 5 is \(\ulcorner S0 \urcorner = 2^{12} 3^{1025} + 1\), which is
4588239037329654294933009459423640636113835 33711852348723982661700090725110495540711416 24496800232720851201851240219667428400380468 28472630247645228844759293716788206726298594 57606066116964029586110650008838161967674248 714876110453564150536269711030213614452805279 213722748800276796114884183810302573694405480 301945785627339339194850085383681785222504546 327111992210992776215014423059901287305704225 3643605726211189929819826835540873386794064170 563975508362231081323849454313910276632860438529,
approximately \(10^{490}\).
Now, let us play a bit with the Gödel number of \(\phi\):
\[\begin{align} \ulcorner \phi \urcorner &= 2^2 3^{\left( 2^8 3^{1025} 5^{\left[ 2^{12} 3^{1025} + 1 \right]} + 1 \right)} \\ &> 3^{5^{\left[ 10^{490} \right]}}, \end{align}\]
so if we take common logarithms, we see that
\[\text{log} \left( \ulcorner \phi \urcorner \right) > 5^{\left[ 10^{490} \right]} \text{log} 3\]
and taking logarithms again,
\[\begin{align} \text{log} \left( \text{log} \left( \ulcorner \phi \urcorner \right) \right) &> 10^{490} \text{log} 5 + \text{log} \left( \text{log} 3 \right) \\ &> 10^{489}. \end{align}\]
Hmm... So this means that \(\text{log} \left( \ulcorner \phi \urcorner \right)\) is bigger than \(10^{\left[ 10^{489} \right]}\). But the common logarithm of a number is (approximately) the number of digits that it takes to express the number in base 10 notation, so we have shown that it takes more than \(10^{\left[ 10^{489} \right]}\) digits to write out the Gödel number of \(\phi\). If you remember that a googol is \(10^{100}\) and a googolplex is \(10^{10^{100}}\), \(\ulcorner \phi \urcorner\) is starting to look like a pretty big number, but it gets better!
To write out a string of \(10^{\left[10^{489} \right]}\) characters (assuming a million characters per mile, or about 16 characters per inch) would require far more than \(10^{\left[ 10^{488} \right]}\) miles, which is far more than \(10^{\left[ 10^{487} \right]}\) light years.
Or, to look at it another way, if we assume that we can put about 132 lines of type of an 8.5- by 11-inch piece of paper, and since a ream of paper (500 sheets) is about 2 inches thick, that gives a tack of paper more than \(10^{\left[ 10^{488} \right]}\) light years high. Since the age of the universe is currently estimated to be in the tens of billions of years (on the order of \(10^{10}\) years), if we assume that the universe is both Euclidean and spherical, the volume of the universe is less than \(10^{40}\) cubic light years, rather less than the \(10^{\left[ 10^{488} \right]}\) cubic light years we would need to store our stack of paper. In short, we don't win any prizes for being incredibly efficient with the coding that we have chosen. What we do win is ease of analysis. The fact that we have chosen to code using a representable function will make our proofs to come much easier to comprehend.
Exercises
- Evaluate the Gödel number for each of the following:
(a) \(\left( \forall v_3 \right) \left( v_3 + 0 = v_4 \right)\)
(b) \(SSSS0\) - Find the formula or term that is coded by each of the following:
(a) \(2^8 3^{\left( 2^{14} 3^{\left( 2^{18} 3^9 5^{1025} + 1 \right)} 5^{\left( 2^{18} 3^{33} 5^{1025} +1 \right)} + 1 \right]} 5^{\left[ 2^{18} 3^{129} 5^{1025} + 1 \right]}\)
(b) \(2^2 3^{\left( 2^{20} 3^{1025} 5^{\left( 2^{12} 3^{1025} + 1 \right)} + 1 \right)}\)
(c) \(2^6 3^9 5^{\left( 2^8 3^9 5^9 + 1 \right)}\) - Look at the number \(c = 2^8 3^{1025} 5^{1025} = \langle 7, \ulcorner 0 \urcorner, \ulcorner 0 \urcorner \rangle\). Find the number \(e\) such that \(IthElement \left( e, 2, c \right)\) is true. Suppose that \(d = \langle 3, 1, 4, 5 \rangle = 2^4 3^2 5^5 7^6\). Why is \(IthElement \left( 4, 1, d \right)\) false?
