# 自己検証理論

$(\forall x,y)\ (\exists z)\ {\rm multiply}(x,y,z).$

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

この理論にはいかなる真の$\Pi^0_1$を追加しても、なお無矛盾であるようにできる。

## 出典

• Solovay, R., 1989. "Injecting Inconsistencies into Models of PA". Annals of Pure and Applied Logic 44(1-2): 101—132.
• Willard, D., 2001. "Self Verifying Axiom Systems, the Incompleteness Theorem and the Tangibility Reflection Principle". Journal of Symbolic Logic 66:536—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—496.