自己検証理論

自己検証理論 (Self-verifying theories) とは、無矛盾で、ペアノ算術よりはるかに弱く、自身の無矛盾性を証明できる算術の一階の体系である。ダン・ウィラードが初めてこの特性を調べ始め、そのような体系の一族を記述した。ゲーデルの不完全性定理によるとこれらの体系はペアノ算術の理論を含むことができないが、それにもかかわらず強い理論を含むことができる。たとえばペアノ算術の無矛盾性を証明できる自己検証体系が存在する。概略を示すと、ウィラードによる体系の構成の鍵は、ゲーデルの機構が体系内の証明可能性について議論できる程度の形式化を行うが、対角線論法を形式化できるようにしないことであった。対角線論法は乗法が (そして以前の版の成果では加法も) 全域関数であることを証明可能であることに依存している。加法と乗法はウィラードの言語においては関数記号ではない。代わりに、減法と除法が関数記号であり、これらから加法と乗法の述語を定義する。このとき、乗法の全域性を表現する以下の<math>\\Pi^0_2</math>文は証明できない::<math>(\\forall x,y)\\ (\\exists z)\\ (x,y,z).</math>ここで <math></math> は <math>z/y=x</math> を意味する三項述語である。演算がこの方法で表現されるとき、与えられた文の証明可能性は解析的タブロー を記述する算術の文としてコード化可能である。それから、無矛盾性の証明可能性は単に公理として追加可能である。結果として得られる体系は、通常の算術についての相対的無矛盾性の議論によって無矛盾性を証明できる。この理論にはいかなる真の<math>\\Pi^0_1</math>文を追加しても、なお無矛盾であるようにできる。