形式的理論の次数との関係
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2018/06/27 23:30 UTC 版)
「低基底定理」の記事における「形式的理論の次数との関係」の解説
これらの諸定理は形式的理論の計算可能性と密接に関係している。任意の無矛盾理論 T {\displaystyle T} はヘンキン構成の類似によって無矛盾かつ完全な理論に拡大することができる。それにはまず閉論理式の全体を φ 0 , φ 1 , … {\displaystyle \varphi _{0},\varphi _{1},\ldots } と並べる。 T {\displaystyle T} にこれらの閉論理式の肯定形または否定形を付け加えることによって無矛盾完全なものに拡大する。有限な拡大の仕方は幾つもあるので、それらひとつひとつの拡大に対して 2 < ω {\displaystyle 2^{<\omega }} の元を対応させる。その対応は n {\displaystyle n} 番目の閉論理式の肯定形と否定形のどちらを付け加えたかによって n {\displaystyle n} 項目の値を 0 {\displaystyle 0} または 1 {\displaystyle 1} にすることで与えられる。このとき T {\displaystyle T} の無矛盾拡大に対応する 2 < ω {\displaystyle 2^{<\omega }} の元の全体は無限二分木を成す。もし無矛盾拡大の木が次数 a {\displaystyle a} の無限枝を持てば、それを用いて T {\displaystyle T} の無矛盾拡大で次数 a {\displaystyle a} のものが得られる。 T {\displaystyle T} が計算可能であったとしても、対応する無矛盾拡大の木が計算可能とは限らないので、基底定理を使用できない。そこで無矛盾拡大の木を次のような木に置き換える。 2 < ω {\displaystyle 2^{<\omega }} の元 σ {\displaystyle \sigma } は、 T {\displaystyle T} を σ {\displaystyle \sigma } で拡大した理論から複雑さ(例:証明図のゲーデル数) | σ | {\displaystyle |\sigma |} 未満で矛盾に至ることがないならば、その木に属すものとする。このように定義された木は計算可能であるから基底定理が使用できる。 低基底定理を上記の木に適用することで T {\displaystyle T} の無矛盾完全拡大で低次数を持つものが構成できる。
※この「形式的理論の次数との関係」の解説は、「低基底定理」の解説の一部です。
「形式的理論の次数との関係」を含む「低基底定理」の記事については、「低基底定理」の概要を参照ください。
- 形式的理論の次数との関係のページへのリンク