ポストの定理

提供: testwiki
ナビゲーションに移動 検索に移動

ポストの定理: Post's theorem)は、計算可能性理論における定理で、算術的階層チューリング次数の関係を表している。名称はエミール・ポストに因んでいる。

背景

ポストの定理は定義可能性と再帰理論に関連したいくつかの概念を必要とする。この節ではそれら概念の概要を解説する。

算術的階層は、ペアノ算術で定義可能な自然数の集合を階層的に分類するものである。ある論理式Σm0 に属するとは、それが冠頭標準形(全ての量化子が先頭にある)の存在量化式で、存在量化と全称量化m 回交互にあって、それらが量化されていない論理式に適用されている場合である。次のような形式のペアノ算術の言語で書かれた論理式 ϕ(s)Σm0 論理式である。

n1n2n3n4Qnmρ(n1,,nm,x1,,xk)

ここで ρ は量化子を含まない論理式で、Qm が偶数なら m が奇数なら である。次のように ρ限定量化子のみを含む論理式

(n11n21nj11)(n12nj22)(n13)(Q1n1m)ρ(n11,njmm,x1,,xk)

は、ペアノ算術の公理により、上記形式と等価である。そのため、Σm0 論理式をこの代替形式で定義することも珍しくない。

自然数の集合 AΣm0 であるとは、それを Σm0 論理式で定義できることを意味し、すなわち、Σm0 論理式 ϕ(s) を使って、自然数 n について ϕ(n) が成り立つときのみ、その自然数が A に含まれる。ある集合が Σm0 であるとき、n>m である任意の n についての Σn0 でもある。ただし、個々の m について Σm0 ではない Σm+10 集合が存在する。従って、量化子の交代回数は、集合の複雑さの尺度を定義するのに必要である。

ポストの定理では、上で定義したような絶対的な算術的階層だけでなく、相対化された算術的階層も使う。自然数の集合 AB に対して相対的に Σm0 であることを Σm0,B と表記する。これは、B のメンバーシップを表す述語を含めた拡張言語で記述された Σm0 論理式で A を定義可能であることを意味する。

算術的階層が自然数の集合の定義可能性の尺度となる一方、チューリング次数は自然数の集合の計算不可能性のレベルの尺度となる。集合 A が集合 Bチューリング還元可能であることを ATB と記述し、B についての神託を与える神託機械によって A特性関数を計算できることを意味する。集合 Aチューリングジャンプは、A に関連する停止性問題の形式である。集合 A のチューリングジャンプ A は、A についての神託機械を持ち 0 が入力されたときに停止するチューリング機械のインデックスの集合である。あらゆる集合 A はそのチューリングジャンプにチューリング還元可能であるが、ある集合のチューリングジャンプは決して元の集合にチューリング還元できない。

ポストの定理は有限回反復されたチューリングジャンプを使用する。任意の自然数の集合 A について、A(n) とは A のチューリングジャンプを n 回反復したものを表す。従って、A(0)A そのものであり、A(n+1)A(n) のチューリングジャンプである。

ポストの定理とその系

ポストの定理は、算術的階層と (n) の形式のチューリング次数、すなわち空集合の有限回反復したチューリングジャンプとの密接な関係を確立する(空集合を任意の計算可能な集合に置き換えても定理は成り立つ)。

ポストの定理は次の通りである。

  1. 集合 BΣn+10 であるのは、B(n) の神託機械を持つチューリング機械により帰納可枚挙な場合である。すなわち、BΣ10,(n) で表される場合である。
  2. 集合 (n) は、n>0 のあらゆる n について Σn0 完全である。すなわち、Σn0 のあらゆる集合は (n)多対一還元可能である。

ポストの定理には様々な系があり、算術的階層とチューリング次数の様々な関係を表している。例えば、以下のような系がある。

  1. ある集合 C があるとする。集合 BΣn+10,C であるのは、BΣ10,C(n) となることと等価である。これはポストの定理の前半部分を C の神託機械で相対化したものである。
  2. 集合 BΔn+1 であるのは、BT(n) と等価である。より一般化すると、BΔn+1C であるのは、BTC(n) と等価である。
  3. 集合が算術的に定義できるのは、ある n について Σn0 である場合である。ポストの定理によれば、集合が算術的といえるのは、その集合をある m について (m) にチューリング還元可能な場合のみである。

参考文献

  • Rogers, H. The Theory of Recursive Functions and Effective Computability, MIT Press. ISBN 0-262-68052-1; ISBN 0-07-053522-1
  • Soare, R. Recursively enumerable sets and degrees. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1987. ISBN 3-540-15299-7