النظريات ذاتية التحقق

النظريات ذاتية التحقق هي أنظمة حسابية متسقة من الدرجة الأولى ، أضعف بكثير من حساب بيانو ، قادرة على إثبات اتساقها الذاتي . كان دان ويلارد أول من درس خصائصها، وقد وصف مجموعة من هذه الأنظمة. وفقًا لنظرية عدم الاكتمال لغودل ، لا يمكن لهذه الأنظمة أن تحتوي على نظرية حساب بيانو ولا على جزءها الضعيف، حساب روبنسون ؛ ومع ذلك، يمكنها أن تحتوي على نظريات قوية.

باختصار، يكمن جوهر بناء ويلارد لنظامه في صياغة جزء كافٍ من آلية غودل للتحدث عن إمكانية الإثبات داخليًا دون القدرة على صياغة عملية التقطير . يعتمد التقطير على القدرة على إثبات أن الضرب دالة كلية (وفي الإصدارات السابقة من النتيجة، الجمع أيضًا). الجمع والضرب ليسا رمزين داليين في لغة ويلارد؛ بل الطرح والقسمة هما كذلك، حيث تُعرَّف محمولات الجمع والضرب بدلالة هذين الرمزين. هنا، لا يمكن إثبات${\displaystyle \Pi _{2}^{0}}$جملة تعبر عن مجموع الضرب: $${\displaystyle (\forall x,y)\ (\exists z)\ {\rm {multiply}}(x,y,z).}$$ أين${\displaystyle {\rm {multiply}}}$هو المسند الثلاثي الذي يرمز إلى${\displaystyle z/y=x.}$ عند التعبير عن العمليات بهذه الطريقة، يمكن ترميز إمكانية إثبات جملة معينة كجملة حسابية تصف نهاية جدول تحليلي . ويمكن بعد ذلك إضافة إمكانية إثبات الاتساق ببساطة كمسلمة. ويمكن إثبات اتساق النظام الناتج باستخدام حجة الاتساق النسبي بالنسبة للحساب العادي.

ويمكن للمرء أن يضيف أي شيء صحيح${\displaystyle \Pi _{1}^{0}}$ربط جملة حسابية بالنظرية مع الحفاظ على اتساق النظرية.

• سولوفاي، روبرت م. (9 أكتوبر 1989). "إدخال التناقضات في نماذج المنطق البحت" . حوليات المنطق البحت والتطبيقي . 44 ( 1-2 ): 101-132 . doi : 10.1016/0168-0072(89)90048-1 .
• ويلارد، دان إي. (يونيو 2001). "أنظمة البديهيات ذاتية التحقق، ونظرية عدم الاكتمال، ومبادئ الانعكاس ذات الصلة" . مجلة المنطق الرمزي . 66 (2): 536-596 . doi : 10.2307/2695030 . JSTOR 2695030. S2CID 2822314 .  
• Willard, Dan E. (Mar 2002). "How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem almost to Robinson's Arithmetic Q". The Journal of Symbolic Logic. 67 (1): 465–496. doi:10.2178/jsl/1190150055. JSTOR 2695021. S2CID 8311827.

• Dan Willard's home page. Archived 2018-08-18 at the Wayback Machine