يادداشتي درباره نقاط ثابت در منطق مسور اثباتها و پارادوكس امتحان غيرمنتظره

A Note on Fixed Points in Quantified Logic of Proofs and the Surprise Test Paradox

در اين مقاله قصد داريم تأثير افزودن نقاط ثابت به منطق هاي توجيه را بررسي كنيم. به ويژه به مطالعه منطق مسور اثبات ها، كه توسط فيتينگ معرفي شده است و گسترشي از منطق اثبات هاي آرتموف به يك منطق محمول ها مي باشد، مي پردازيم. ما گسترش هاي نقطه ثابتي از منطق مسور اثبات ها را ارايه مي دهيم. اين گسترش ها توسط افزودن عملگرهاي نقطه ثابت (يا عملگرهاي قطري)، كه توسط اسمورينسكي معرفي شده است، به زبان منطق مسور اثبات ها به دست مي آيند. سپس پارادوكس دانا و نسخه هاي خودارجاعي از پارادوكس امتحان غيرمنتظره را در اين گسترش هاي نقطه ثابت صورت بندي مي كنيم. با تفسير يك جمله غافلگيرانه به عنوان گزاره اي كه هيچ توجيهي براي آن وجود ندارد، ما در منطق مسور اثبات ها، راه حلي براي نسخه خود ارجاع پارادوكس امتحان غيرمنتظره ارايه مي دهيم. ما در واقع نشان مي دهيم كه يكي از اصول منطق مسور اثبات ها (كه فيتينگ آن را فرمول باركان يكنواخت ناميده است) مي تواند عامل ايجاد تناقض در اين پارادوكس ها باشد، و بنابراين با رد اين اصل مي توانيم از استنتاج تناقض در پارادوكس هاي ذكر شده در مقاله جلوگيري كنيم. همچنين با معرفي مدل هاي مكرتيچف براي اين گسترش هاي نقطه ثابتِ منطق مسور اثبات ها نشان مي دهيم كه اين گسترش ها (بدون فرمول باركان يكنواخت) سازگار هستند.

In this note, we study the effect of adding fixed points to justification logics. By making use of the fixed point operators (or diagonal operators) introduced by Smorynski in his Diagonalization Operator Logic, we introduce fixed point extensions of Fitting's quantified logic of proofs QLP. We then formalize the Knower Paradox and various self-reference versions of the Surprise Test Paradox in these fixed point extensions of QLP. By interpreting a surprise statement as a statement for which there is no justification or evidence, we propose a solution to the self-reference version of the Surprise Test paradox. We show that one of the axioms of QLP (the Uniform Barcan Formula) could be the reason for producing contradiction in these paradoxes, and thus by rejecting this axiom we can avoid contradiction in the aforementioned paradoxes. By introducing Mkrtychev models for the fixed point extensions of QLP, we further show that these fixed point extensions (without the Uniform Barcan Formula) are consistent.