ユーザーブログ:AlweLogic/表現可能性と計算不能関数の値の独立性

\(\newcommand{\card}[1]{\mathrm{card}(#1)} \newcommand{\Pow}[1]{\mathcal{P}(#1)} \newcommand{\Powfin}[1]{\mathcal{P}_\mathrm{fin}(#1)} \newcommand{\inepsilon}{\,\epsilon\,} \newcommand{\notinepsilon}{\not\!\epsilon\,} \newcommand{\range}[1]{\mathrm{ran}(#1)} \newcommand{\field}[1]{\mathrm{field}(#1)} \newcommand{\Nat}{\mathbb{N}} \newcommand{\rnk}[1]{\mathrm{rnk}\mleft(#1\mright)} \newcommand{\numeral}[1]{\underline{#1}} \newcommand{\standardmodel}{\mathbb{N}} \newcommand{\otyp}[1]{\mathrm{otyp}(#1)} \newcommand{\conjunct}{\bigwedge} \newcommand{\disjunct}{\bigvee} \newcommand{\struc}[1]{\left\langle #1\right\rangle} \newcommand{\sequence}[1]{\left\langle #1\right\rangle} \newcommand{\autid}{\mathsf{Aut}(\mathsf{ID})_0} \newcommand{\Cl}[2]{\mathsf{Cl}_{#1}(#2)} \newcommand{\IT}[2]{\mathsf{IT}_{#1}(#2)} \newcommand{\ITs}{(\mathsf{ITA})} \newcommand{\SIGMA}{\mathbf{\Sigma}} \newcommand{\PI}{\mathbf{\Pi}} \newcommand{\DELTA}{\mathbf{\Delta}} \newcommand{\club}[1]{\mathrm{Club}_{#1}} \newcommand{\stat}[1]{\mathrm{Stat}_{#1}} \newcommand{\nonstat}[1]{\mathrm{NS}_{#1}} \newcommand{\Rat}{\mathbb{Q}} \newcommand{\Real}{\mathbb{R}} \newcommand{\cut}{(\mathsf{cut})} \newcommand{\RobR}{\mathsf{R}} \newcommand{\RobQ}{\mathsf{Q}} \newcommand{\PAmin}{\mathsf{PA}^{-}} \newcommand{\IOpen}{\mathsf{IOpen}} \newcommand{\IDeltazero}{\mathsf{I}\Delta_0} \newcommand{\PA}{\mathsf{PA}} \newcommand{\KP}{\mathsf{KP}} \newcommand{\KPomega}{\mathsf{KP}\omega} \newcommand{\ZFC}{\mathsf{ZFC}} \newcommand{\code}[1]{\left\ulcorner #1\right\urcorner}\) 表現可能性による計算可能関数の特徴付けとそれを用いて計算不能関数の値の独立性を示す。

定義1.1 (算術 \(\mathsf{R}\))

算術\(\mathsf{R}\)は以下の公理からなる。 \(m\neq n\)なるような自然数\(m,n\in\Nat\)に対して\(\numeral{m}\neq\numeral{n}\)は\(\RobR\)の公理である。 自然数\(m,n\in\Nat\)に対して\(\numeral{m}+\numeral{n}=\numeral{m+n}\)は\(\RobR\)の公理である。 自然数\(m,n\in\Nat\)に対して\(\numeral{m}\times\numeral{n}=\numeral{m\times n}\)は\(\RobR\)の公理である。 \((\forall x)[x\nless\numeral{0}]\)は\(\RobR\)の公理である。 自然数\(n\in\Nat\)に対して\((\forall x)\left[x<\numeral{n+1}\leftrightarrow \disjunct_{i<n+1}x=\numeral{i}\ right]\)は\(\RobR\)の公理である。 自然数\(n\in\Nat\)に対して\((\forall x)[x<\numeral{n}\lor x=\numeral{n}\lor \numeral{n}<x]\)は\(\RobR\)の公理である。

定義1.2 表現可能性、可証全域性

\(T\)を理論、\(R\)を\(\Nat\)上の有限項関係、\(f\)を\(\Nat\)上の有限変数関数とする。 \(R\)が\(T\)に於いて\define{表現可能}{representable}であるとは以下を満たす論理式\(\varphi(\vec{u})\)が存在することである。 任意の\(\vec{n}\in\Nat^\nu\)に対して\(\vec{n}\in R\)ならば\(T\vdash\varphi(\vec{\numeral{n}})\)である。 任意の\(\vec{n}\in\Nat^\nu\)に対して\(\vec{n}\notin R\)ならば\(T\vdash\lnot\varphi(\vec{\numeral{n}})\)である。 \(R\)が\(T\)に於いて\define{弱表現可能}{weakly representable}であるとは以下を満たす論理式\(\varphi(\vec{u})\)が存在することである。 任意の\(\vec{n}\in\Nat^\nu\)に対して\(\vec{n}\in R\)ならば\(T\vdash\varphi(\vec{\numeral{n}})\)である。 任意の\(\vec{n}\in\Nat^\nu\)に対して\(\vec{n}\notin R\)ならば\(T\nvdash\varphi(\vec{\numeral{n}})\)である。 \(f\)が\(T\)に於いて\define{関数的に表現可能}{functionally representable}であるとは以下を満たす論理式\(\varphi(\vec{u},v)\)が存在することである。 \(f\)のグラフ\(G_f\)は\(T\)にて\(\varphi(\vec{u},v)\)によって表現される。すなわち\(f(\vec{n})=m\)ならば\(T\vdash\varphi(\vec{n},m)\)であり、\(f(\vec{n})\neq m\)ならば\(T\vdash\lnot\varphi(\vec{n},m)\)である。 任意の\(\vec{n}\in\Nat^\nu\)に対して\(T\vdash(\forall x)(\forall y)[\varphi(\vec{n},x)\land\varphi(\vec{n},y)\to x=y]\)である。 \(f\)が\(T\)に於いて\define{可証全域関数}{provably total function}であるとは、\(f\)を\(T\)に於いて関数的に表現する論理式\(\varphi(\vec{u},v)\)が存在して \[T\vdash(\forall\vec{x})(\exists !y)\varphi(\vec{x},y)\] となることである。

事実1.2 表現可能性定理など
\(T\)を\(\mathsf{R}\)を含む無矛盾で\(\Sigma_1\)-定義可能な理論とし、\(f\)を\(\Nat\)上の有限変数関数とする。このとき以下は同値である。 \(f\)は計算可能である。 \(f\)のグラフは\(\Sigma_1\)-定義可能である。 \(f\)のグラフは\(\Delta_1\)-定義可能である。 \(f\)は\(T\)にて関数的に表現可能である。 \(f\)の\(T\)にてグラフは表現可能である。 \(f\)の\(T\)にてグラフは弱表現可能である。

定理1.3

\(T\)を\(\mathsf{R}\)を含む\(\Sigma_N\)-健全かつ\(\Sigma_1\)-定義可能な理論とし、\(f\)を\(T\)に於いて可証全域な\(\Sigma_N\)-定義可能計算不能関数とする。 このとき、ある自然数\(n,m\)に対して\(T\nvdash f(\numeral{n})=\numeral{m}\)かつ\(T\nvdash f(\numeral{n})\neq \numeral{m}\)となる。 証明　事実1.2より\(f\)のグラフは弱表現可能ではない。すなわち任意の論理式\(\varphi(x,y)\)に対して ある\(n,m\)が存在して\(f(n)=m\)かつ\(T\nvdash\varphi(\numeral{n},\numeral{m})\)である。 ある\(n,m\)が存在して\(f(n)\neq m\)かつ\(T\vdash\varphi(\numeral{n},\numeral{m})\)である。 のいずれかが成り立つ。ここで\(f\)は可証全域であるから\(f\)を定義する\(\Sigma_n\)-論理式を\(\psi(x,y)\)とするとき\(f(n)=m\Leftrightarrow\Nat\models \psi(\numeral{n},\numeral{m})\)となる。 よって任意の\(n,m\)に対して\(f(n)\neq m\)であるとき\(\Sigma_N\)-健全性から\(T\nvdash\varphi(\numeral{n},\numeral{m})\)となる。 すなわち\(\psi(x,y)\)に対して2.は成り立たない。よって1.が成り立つ。\(\square\)