低基底定理

${\displaystyle \mathbb {P} }$ を計算可能な無限二分木の全体を包含関係で並べたものとする。これをショカシュとソーアの強制概念（JS forcing notion）という。いま ${\displaystyle T}$ を再帰的な無限二分木とする。${\displaystyle \mathbb {P} }$ の減少列 ${\displaystyle T_{e}}$ を次のように再帰的に定義する：

• ${\displaystyle T_{0}=T}$、
• ${\displaystyle T_{e+1}=T_{e}}$（${\displaystyle T_{e}\cap U_{e}}$ が有限なとき）、${\displaystyle T_{e+1}=T_{e}\cap U_{e}}$（${\displaystyle T_{e}\cap U_{e}}$ が無限なとき）、ただし ${\displaystyle U_{e}=\{\sigma \mid \{e\}_{|\sigma |}^{\sigma }(e)\uparrow \}}$ である。

この列は ${\displaystyle 0'}$-計算可能である。弱ケーニヒの補題より ${\displaystyle [T_{e}]}$（${\displaystyle T_{e}}$ の無限枝の全体）は空でない。${\displaystyle [T_{e}]}$ はカントール空間 ${\displaystyle 2^{\omega }}$ の閉集合であり、${\displaystyle 2^{\omega }}$ はコンパクトだから、${\displaystyle \bigcap _{e\in \mathbb {N} }[T_{e}]}$ は空でない。${\displaystyle \bigcap _{e\in \mathbb {N} }[T_{e}]}$ の任意の元は ${\displaystyle T}$ の無限枝であって低次数を持つ。

これらの諸定理は形式的理論の計算可能性と密接に関係している。任意の無矛盾理論 ${\displaystyle T}$ はヘンキン構成の類似によって無矛盾かつ完全な理論に拡大することができる。それにはまず閉論理式の全体を ${\displaystyle \varphi _{0},\varphi _{1},\ldots }$ と並べる。${\displaystyle T}$ にこれらの閉論理式の肯定形または否定形を付け加えることによって無矛盾完全なものに拡大する。有限な拡大の仕方は幾つもあるので、それらひとつひとつの拡大に対して ${\displaystyle 2^{<\omega }}$ の元を対応させる。その対応は ${\displaystyle n}$番目の閉論理式の肯定形と否定形のどちらを付け加えたかによって ${\displaystyle n}$ 項目の値を ${\displaystyle 0}$ または ${\displaystyle 1}$ にすることで与えられる。このとき ${\displaystyle T}$ の無矛盾拡大に対応する ${\displaystyle 2^{<\omega }}$ の元の全体は無限二分木を成す。もし無矛盾拡大の木が次数 ${\displaystyle a}$ の無限枝を持てば、それを用いて ${\displaystyle T}$ の無矛盾拡大で次数 ${\displaystyle a}$ のものが得られる。

${\displaystyle T}$ が計算可能であったとしても、対応する無矛盾拡大の木が計算可能とは限らないので、基底定理を使用できない。そこで無矛盾拡大の木を次のような木に置き換える。${\displaystyle 2^{<\omega }}$ の元 ${\displaystyle \sigma }$ は、${\displaystyle T}$ を ${\displaystyle \sigma }$ で拡大した理論から複雑さ（例：証明図のゲーデル数） ${\displaystyle |\sigma |}$ 未満で矛盾に至ることがないならば、その木に属すものとする。このように定義された木は計算可能であるから基底定理が使用できる。

低基底定理を上記の木に適用することで ${\displaystyle T}$ の無矛盾完全拡大で低次数を持つものが構成できる。

• Cenzer, Douglas (1999). “${\displaystyle \Pi _{1}^{0}}$ classes in computability theory”. In Griffor, Edward R.. Handbook of computability theory. Stud. Logic Found. Math.. 140. North-Holland. pp. 37–85. ISBN 0-444-89882-4. MR 1720779. Zbl 0939.03047  Theorem 3.6, p. 54.
• Cooper, S. Barry (2004). Computability Theory. Chapman and Hall/CRC. ISBN 1-58488-237-9 .
• Jockusch, Carl G., Jr.; Soare, Robert I. (1972). “Π(0, 1) Classes and Degrees of Theories”. Transactions of the American Mathematical Society 173: 33–56. doi:10.1090/s0002-9947-1972-0316227-0. ISSN 0002-9947. JSTOR 1996261. Zbl 0262.02041.  The original publication, including additional clarifying prose.
• Nies, André (2009). Computability and randomness. Oxford Logic Guides. 51. Oxford: Oxford University Press. ISBN 978-0-19-923076-1. Zbl 1169.03034  Theorem 1.8.37.
• Soare, Robert I. (1987). Recursively enumerable sets and degrees. A study of computable functions and computably generated sets. Perspectives in Mathematical Logic. Berlin: Springer-Verlag. ISBN 3-540-15299-7. Zbl 0667.03030 
• Diamondstone, David E.; Dzhafarov, Damir D.; Soare, Robert I. (2010). “${\displaystyle \Pi _{1}^{0}}$ Classes, Peano Arithmetic, Randomness, and Computable Domination”. Notre Dame Journal of Formal Logic 51 (1): 127-159. 

この項目は、数理論理学に関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています。

• 表示
• 編集