ここでは理論\(T\)の言語は定数記号\(c_k\)、関数記号\(f_k\)、述語記号\(R_k\)を有限個しか持たないものに制限する。
また、長さ\(n\)の記号列に現れる変数記号を\(x_k(0≤k<n)\)に制限する。長さ\(n\)の証明には変数記号がたかだか\(n\)個しか出現しないから、このように変数記号を制限しても証明能力も証明の長さも変わらない。
\(T\)の定数記号の数を\(\mathrm{consts}_T\)、関数記号の数を\(\mathrm{funcs}_T\)、述語記号の数を\(\mathrm{preds}_T\)とする。
\(\mathrm{syms}_T=8+\mathrm{consts}_T+\mathrm{funcs}_T+\mathrm{preds}_T\)とする。\(T\)の言語の記号に、以下のように自然数を割り当てる:
\(┌(┐=1,\) \(┌,┐=2,\) \(┌)┐=3,\) \(┌¬┐=4,\) \(┌∧┐=5,\) \(┌∃┐=6,\) \(┌=┐=7,\) \(┌c_k┐=8+k,\) \(┌f_k┐=8+\mathrm{consts_T}+k,\) \(┌R_k┐=8+\mathrm{consts_T}+\mathrm{funcs_T}+k,\) \(┌x_k┐=\mathrm{syms}_T+k.\)
理論\(T\)に対して、関数\(\mathrm{hl}_T\)を以下のように帰納的に定義する:
- \(n=0\)ならば、\(\mathrm{hl}_T(n)=1.\)
- \(n>0\)ならば、\(\mathrm{hl}_T(n)=\mathrm{hl}_T(n-1)+(\mathrm{syms}_T+n)^n.\)
長さ\(n\)の記号列\(φ\)の\(0≤k<n\)文字目の記号を\(φ_k\)で表す。\(φ\)に以下のように自然数を割り当て、\(┌φ┐\)で表す。
- \(n=0\)ならば、\(┌φ┐=0.\)
- \(n>0\)ならば、\(┌φ┐=\mathrm{hl}_T(n-1)+\sum_{k=0}^{n-1}(┌φ_k┐-1)(\mathrm{syms}_T+n)^k.\)
チューリング機械の符号化を1つ固定し、チューリング機械をその符号と同一視する。チューリング機械の状態は有限個で互いに区別が付けばいいので、自然数で表す。また停止状態は\(0\)に固定する。
\(\mathrm{state}(M,x)=y\) を、「チューリング機械\(M\)の\(x\)ステップ目の状態は\(y\)である」を意味する述語とする。
\(\mathrm{steps}(M)=x := \mathrm{state}(M,x)=0∧∀y<x.\mathrm{state}(M,y)≠0\) とする。これは「チューリング機械\(M\)の実行ステップ数は\(x\)である」を意味する述語である。
\(\mathrm{halt}(M) := ∃x.\mathrm{steps}(M)=x\) とする。これは「チューリング機械\(M\)は停止する」を意味する述語である。
\(\mathrm{proof}_T\)を理論\(T\)の証明述語とする。すなわち、\(\mathrm{proof}_T(x,y)\)は「\(y\)は\(x\)の\(T\)における証明である」を意味する述語である。
\(\mathrm{TR}(T,n)≤m := ∀y<\mathrm{hl}_T(n)∀M≤y.\mathrm{proof}_T(┌\mathrm{halt}(M)┐,y)→\mathrm{steps}(M)≤m\) とする。
\(\mathrm{TR}(T,n)=m := \mathrm{TR}(T,n)≤m∧∀k<m.¬\mathrm{TR}(T,n)≤k\) と定義する。