自己検証理論のソースを表示

'''自己検証理論''' ({{lang-en|'''Self-verifying theories'''}}) は、無矛盾で、[[ペアノ算術]]よりはるかに弱く、自身の[[無矛盾性]]を証明できる[[算術]]の[[一階述語論理|一階]]の体系である。[[ダン・ウィラード]]が初めてこの特性を調べ始め、そのような体系の一族を記述した。[[ゲーデルの不完全性定理]]によるとこれらの体系はペアノ算術の理論を含むことができないが、それにもかかわらず強い理論を含むことができる。たとえばペアノ算術の無矛盾性を証明できる自己検証体系が存在する。

概略を示すと、ウィラードによる体系の構成の鍵は、[[クルト・ゲーデル|ゲーデル]]の機構が体系内の[[証明可能性]]について議論できる程度の形式化を行うが、[[対角線論法]]を形式化できるようにしないことであった。対角線論法は乗法が (そして以前の版の成果では加法も) 全域関数であることを証明可能であることに依存している。加法と乗法はウィラードの言語においては関数記号ではない。代わりに、減法と除法が関数記号であり、これらから加法と乗法の述語を定義する。このとき、乗法の全域性を表現する以下の[[算術的階層|<math>\Pi^0_2</math>文]]は証明できない:

:<math>(\forall x,y)\ (\exists z)\ {\rm multiply}(x,y,z).</math>

ここで <math>{\rm multiply}</math> は <math>z/y=x</math> を意味する三項述語である。
演算がこの方法で表現されるとき、与えられた文の証明可能性は[[解析的タブロー]] ([[:en:analytic tableaux|en]]) を記述する算術の文としてコード化可能である。それから、無矛盾性の証明可能性は単に公理として追加可能である。結果として得られる体系は、通常の算術についての[[相対的無矛盾性]]の議論によって無矛盾性を証明できる。

この理論にはいかなる真の[[算術的階層|<math>\Pi^0_1</math>文]]を追加しても、なお無矛盾であるようにできる。

== 出典 ==
* Solovay, R., 1989.  "Injecting Inconsistencies into Models of PA".   Annals of Pure and Applied Logic 44(1-2): 101&mdash;132.
* Willard, D., 2001.  "Self Verifying Axiom Systems, the Incompleteness Theorem and the Tangibility Reflection Principle".  Journal of Symbolic Logic 66:536&mdash;596.
* Willard, D., 2002.  "How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem to Robinson's Arithmetic Q" .  Journal of Symbolic Logic 67:465&mdash;496.

== 外部リンク ==
* [http://www.cs.albany.edu/FacultyStaff/profiles/willard.htm ダン・ウィラードのホームページ] {{en_icon}}

{{DEFAULTSORT:しこけんしようりろん}}
[[Category:数理論理学]]
[[Category:演繹理論]]
[[Category:数学に関する記事]]