Abstract:
در این مقاله قصد داریم تأثیر افزودن نقاط ثابت به منطق های توجیه را بررسی کنیم. به ویژه به مطالعه منطق مسور اثبات ها، که توسط فیتینگ معرفی شده است و گسترشی از منطق اثبات های آرتموف به یک منطق محمول ها می باشد، می پردازیم. ما گسترش های نقطه ثابتی از منطق مسور اثبات ها را ارایه می دهیم. این گسترش ها توسط افزودن عملگرهای نقطه ثابت (یا عملگرهای قطری)، که توسط اسمورینسکی معرفی شده است، به زبان منطق مسور اثبات ها به دست می آیند. سپس پارادوکس دانا و نسخه های خودارجاعی از پارادوکس امتحان غیرمنتظره را در این گسترش های نقطه ثابت صورت بندی می کنیم. با تفسیر یک جمله غافلگیرانه به عنوان گزاره ای که هیچ توجیهی برای آن وجود ندارد، ما در منطق مسور اثبات ها، راه حلی برای نسخه خود ارجاع پارادوکس امتحان غیرمنتظره ارایه می دهیم. ما در واقع نشان می دهیم که یکی از اصول منطق مسور اثبات ها (که فیتینگ آن را فرمول بارکان یکنواخت نامیده است) می تواند عامل ایجاد تناقض در این پارادوکس ها باشد، و بنابراین با رد این اصل می توانیم از استنتاج تناقض در پارادوکس های ذکر شده در مقاله جلوگیری کنیم. همچنین با معرفی مدل های مکرتیچف برای این گسترش های نقطه ثابتِ منطق مسور اثبات ها نشان می دهیم که این گسترش ها (بدون فرمول بارکان یکنواخت) سازگار هستند.
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.
Machine summary:
برای مثال قضیه ناتمامیت گودل (با ساخت جملـه ای کـه غیرقابل اثبات بودن خود را بیان مـی کنـد)، تعریـف ناپـذیری صـدق تارسـکی (بـا سـاخت جمله ای کـه بیـانگر کـاذب بـودن خـود اسـت ، پـارادوکس دروغگـو)، و پـارادوکس دانـا (یا پارادوکس داننده ) (the Knower Paradox) از کاپلان -مونتگیـو (بـا سـاخت جملـه ای کـه معرفت ناپذیری صدق خود را بیان می کند) همگی نتایجی از لم نقطه ثابت هستند.
ایـن جملـه در ܣܲ بـه صـورت زیر قابل بیان است : ഥሻܦሺݎ՞ ܶ ܦ که در آن ሻݔሺݎܶ یک محمول صدق (truth predicate) میباشد، یعنـی یـک محمـول بـا یک متغیر آزاد ݔ به گونه ای که برای هر جمله ܣ فرمول زیر اثبات پذیر باشد: ҧሻܣሺݎܶ ՞ ܣ ሻݔሺݎܶ به این صورت خوانده میشود: ݔ (عـدد گـودل فرمـولی اسـت کـه آن فرمـول ) صادق است .
محمول ሻݔሺܭ یک محمـول معرفـت (knowledge predicate) نامیـده مـیشـود، یعنـی یـک محمول با یک متغیر آزادݔ ،هر گاه برای هر جمله ܣ فرمول زیر اثبات پذیر باشد: ܣ ҧሻ՜ܣሺܭ ሻݔሺܭ به این صورت خوانده میشود: مـیدانـیم ݔ (عـدد گـودل فرمـولی اسـت کـه آن فرمول ) صادق است .
پالِ اگرِ در [٢٠] اثباتی از قضیه مونتگیو ارایـه کـرده اسـت کـه در آن از لـم نقطـه ثابـت برای ساختن جمله ای در ܣܲ استفاده شده است که نسـخه خـود ارجـاع زیـر از پـارادوکس امتحان غیرمنتظره را بیان میکند: "مگر اینکه شما بدانید این عبارت نادرست است ، شما فردا یک امتحان خواهیـد داشـت 1 اما شما نمی توانید از این عبارت بدانید که فردا یک امتحان خواهید داشت " نسخه بالا از پارادوکس اولین بار توسط کاپلان -مونتگیو در [٢١] ارایه شـد.