自己検証理論

自己検証理論とは、ペアノ算術よりもはるかに弱い、一貫性のある一階算術体系であり、自身の一貫性を証明できるものである。ダン・ウィラードは、これらの体系の性質を最初に研究し、そのような体系のファミリーを記述した。ゲーデルの不完全性定理によれば、これらの体系はペアノ算術の理論も、その弱い断片であるロビンソン算術も含むことはできないが、強い定理を含むことはできる。

概略的に言うと、ウィラードの体系構築の鍵は、対角化を形式化できなくても、内部的に証明可能性について議論できる程度にゲーデルの仕組みを形式化することにある。対角化は、乗法が全関数であることを証明できることに依存している（そして、結果の初期バージョンでは、加算も）。加算と乗法はウィラードの言語の関数記号ではない。代わりに、減法と除法が関数記号であり、加算と乗法の述語はこれらを用いて定義されている。ここでは、$\displaystyle \Pi _{2}^{0}}$乗算の全体を表す 文：$${\displaystyle (\forall x,y)\ (\exists z)\ {\rm {multiply}}(x,y,z).}$$ どこ$\displaystyle {\rm {乗算}}}$は、${\displaystyle z/y=x.}$ このように演算を表現すると、与えられた文の証明可能性は、解析タブローの終了を記述する算術文として符号化できる。そして、一貫性の証明可能性を公理として単純に追加すればよい。結果として得られる体系は、通常の算術に対する相対的一貫性論証によって一貫性を証明できる。

さらに、真の$\displaystyle \Pi _{1}^{0}}$理論の整合性を維持しながら、理論に算術的な文を追加する。

• Solovay, Robert M. (1989年10月9日). 「PAモデルへの矛盾の注入」 . Annals of Pure and Applied Logic . 44 ( 1–2 ): 101–132 . doi : 10.1016/0168-0072(89)90048-1 .
• Willard, Dan E. (2001年6月). 「自己検証公理系、不完全性定理および関連する反射原理」 . The Journal of Symbolic Logic . 66 (2): 536–596 . doi : 10.2307/2695030 . JSTOR 2695030 . S2CID 2822314 .  
• Willard, Dan E. (2002年3月). 「意味タブローとカットフリー版の第2不完全性定理をロビンソンの算術Qにほぼ拡張する方法」 .記号論理学ジャーナル. 67 (1): 465–496 . doi : 10.2178/jsl/1190150055 . JSTOR 2695021 . S2CID 8311827 .  

• ダン・ウィラードのホームページ。 2018年8月18日にウェイバックマシンにアーカイブされました。