自己検証理論

自己検証理論

自己検証理論（Self-verifying theories）は、一階の算術体系の一つであり、特にその無矛盾性を証明する能力を持っています。この理論は、ペアノ算術のように強力ではないものの、非常に興味深い特徴を有しており、数理論理の研究において重要な位置を占めています。

この理論の研究は、ダン・ウィラードによって進められました。ウィラードは、自己検証理論の特性や、これに関連する体系の種類を詳しく探求し、その構造を明らかにしました。特に、ウィラードの体系ではゲーデルの不完全性定理が重要な役割を果たしています。

理論の特性

ゲーデルの不完全性定理によれば、ある算術体系が自らの無矛盾性を証明できないため、自己検証理論はペアノ算術を含まないものの、相対的により強い理論を含む可能性を秘めています。たとえば、ペアノ算術の無矛盾性を証明できる体系を作成することが可能です。

ウィラードによって構成されたこの理論の核心は、体系の内部において証明可能性について語ることができる程度の形式化を行う一方で、対角線論法を正確に表現しないことにあります。対角線論法は、乗法が全域関数であることや、以前の版本では加法も同様であることを証明するために依存しています。しかし、ウィラードの体系においては、加法と乗法は関数記号として扱われず、代わりに減法と除法が関数記号として使用されます。

この構造の利点は、証明可能性を解析的タブローの言語で記述することができる点です。この方法で表現されると、与えられた文の証明可能性は、算術の文としてコード化されます。また、無矛盾性の証明可能性は単純に公理として追加できるため、得られる体系は無矛盾性の証明が可能になります。

自己検証理論における無矛盾性は、その内部の構造によって影響を受けず、さらなる真のΠ₁⁰文を追加しても、なお無矛盾性が保たれる特性を持っています。この特徴は、ウィラードの理論が、算術的な性質と形式的な論理の関係を巧みに活用していることを示しています。

参考文献

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

外部リンク

• - ダン・ウィラードのホームページ

もう一度検索