در حوزه منطق، همراه مُدال (Modal Companion) یک منطق مُدال نرمال است که یک منطق سوپر-انتوئیژنیستی (یا منطق میانی) را با استفاده از یک ترجمه خاص، که در ادامه توضیح داده میشود، تفسیر میکند. همراهان مُدال، خواص گوناگونی از منطق میانی اصلی را به ارث میبرند. این ویژگی، مطالعه منطقهای میانی را با بهرهگیری از ابزارها و تکنیکهای توسعهیافته برای منطق مُدال، ممکن میسازد.
ترجمه گودل–مککینسکی–تارسکی (Gödel–McKinsey–Tarski translation)
فرض کنید A یک فرمول شهودی گزارهای باشد. یک فرمول مُدال T(A) با استفاده از استقرا بر پیچیدگی A به صورت زیر تعریف میشود:
- برای هر متغیر گزارهای p، داریم
T(p) = □p. T(A ∧ B) = T(A) ∧ T(B)T(A ∨ B) = T(A) ∨ T(B)T(A → B) = T(A) → T(B)T(A ⊥) = ⊥(جایی که ⊥ نمایانگر تناقض است)
از آنجایی که نقیض در منطق شهودی به صورت ¬A = A → ⊥ تعریف میشود، داریم:
T(¬A) = T(A → ⊥) = T(A) → T(⊥) = T(A) → ⊥ = □(T(A) → ⊥)
این ترجمه، T نامیده میشود و با نام ترجمه گودل یا ترجمه گودل–مککینسکی–تارسکی شناخته میشود. این ترجمه گاهی اوقات به شکلهای اندکی متفاوت ارائه میشود؛ برای مثال، ممکن است □ قبل از هر زیرفرمول درج شود. تمام این گونههای مختلف، در منطق S4 معادل اثباتپذیر هستند.
همراهان مُدال (Modal companions)
برای هر منطق مُدال نرمال M که S4 را بسط میدهد، جزء si-fragment آن، که با ρM نمایش داده میشود، به صورت زیر تعریف میگردد:
ρM = {A | T(A) ∈ M}
جزء si-fragment هر بسط نرمال S4، یک منطق سوپر-انتوئیژنیستی است. یک منطق مُدال M، همراه مُدال یک منطق سوپر-انتوئیژنیستی L است اگر ρM = L باشد.
هر منطق سوپر-انتوئیژنیستی، دارای همراهان مُدال است. کوچکترین همراه مُدال L برابر است با:
τL = NCl(T(L))
که در آن NCl نمایانگر بستار نرمال است. میتوان نشان داد که هر منطق سوپر-انتوئیژنیستی، بزرگترین همراه مُدال را نیز دارد که با σL نمایش داده میشود. یک منطق مُدال M همراه L است اگر و تنها اگر L ⊆ ρM.
به عنوان مثال، خود S4 کوچکترین همراه مُدال منطق شهودی (IPC) است. بزرگترین همراه مُدال IPC، منطق گرزِگورچیک (Grzegorczyk logic) Grz است که با محور زیر بر روی K محوربندی میشود:
□(□(p → □p) → p) → p
کوچکترین همراه مُدال منطق کلاسیک (CPC) S5 لوئیس است، در حالی که بزرگترین همراه مُدال آن منطق زیر است:
S5 □(p ↔ □p)
ایزومورفیسم بلوک–اساکیا (Blok–Esakia isomorphism)
مجموعه بسطهای یک منطق سوپر-انتوئیژنیستی L که با شمول مرتب شدهاند، یک شبکه کامل را تشکیل میدهند که با ExtL نمایش داده میشود. به طور مشابه، مجموعه بسطهای نرمال یک منطق مُدال M نیز یک شبکه کامل NExtM را تشکیل میدهد. عملگرهای همراه ρM، τL، و σL را میتوان به عنوان نگاشتهایی بین شبکههای ExtIPC و NExtS4 در نظر گرفت.
مشاهده میشود که هر سه این نگاشتها یکنواخت هستند و ρ تابع همانی بر روی ExtIPC است. L. Maksimova و V. Rybakov نشان دادهاند که ρ، τ، و σ در واقع همریختیهای کامل شبکه، کامل از بالا و کامل از پایین هستند. سنگ بنای نظریه همراهان مُدال، قضیه بلوک–اساکیا است که به طور مستقل توسط Wim Blok و Leo Esakia اثبات شد. این قضیه بیان میدارد:
نگاشتهایρوσایزومورفیسمهای وارون یکدیگر از شبکههایExtIPCوNExtGrzهستند.
بر این اساس، σ و محدودیت ρ به NExtGrz، ایزومورفیسم بلوک–اساکیا نامیده میشوند. یک نتیجه مهم قضیه بلوک–اساکیا، توصیف نحوی سادهای از بزرگترین همراهان مُدال است: برای هر منطق سوپر-انتوئیژنیستی L،
σL = {A | T(A) ∈ NCl(T(L))}
توصیف معنایی (Semantic description)
ترجمه گودل، counterpart قاب-نظری (frame-theoretic) دارد. فرض کنید F یک قاب مُدال عمومی، مُتعدی و بازتابی باشد. رابطه پیشین R، رابطه همارزی زیر را بر روی F القا میکند:
x ~ y اگر و تنها اگر R(x, y) و R(y, x)
که نقاط متعلق به یک خوشه را شناسایی میکند. فرض کنید ρF مجموعه ردههای همارزی F (یعنی ρF مجموعه ردههای همارزی F نسبت به ~ است) و
R' = {(C, D) | ∃x ∈ C, ∃y ∈ D, R(x, y)}
باشد. آنگاه (ρF, R') یک قاب شهودی عمومی است که اسکلت F نامیده میشود. نکته کلیدی ساختار اسکلت، حفظ اعتبار بر اساس ترجمه گودل است: برای هر فرمول شهودی A،
A در ρF معتبر است اگر و تنها اگر T(A) در F معتبر باشد.
بنابراین، جزء si-fragment یک منطق مُدال M را میتوان به صورت معنایی تعریف کرد: اگر M نسبت به کلاسی C از قابهای مُدال عمومی مُتعدی و بازتابی کامل باشد، آنگاه ρM نسبت به کلاس {ρF | F ∈ C} کامل است.
بزرگترین همراهان مُدال نیز توصیف معنایی دارند. برای هر قاب شهودی عمومی V، فرض کنید σV بستار V تحت عملیات بولی (تقاطع دوتایی و متمم) باشد. میتوان نشان داد که σV تحت □ بسته است، بنابراین (σV, R'') یک قاب مُدال عمومی است. اسکلت σF ایزومورف با F است. اگر L یک منطق سوپر-انتوئیژنیستی باشد که نسبت به کلاسی C از قابهای عمومی کامل است، آنگاه بزرگترین همراه مُدال آن σL نسبت به کلاس {σF | F ∈ C} کامل است.
اسکلت یک قاب کرایپکه، خود یک قاب کرایپکه است. از سوی دیگر، σF هرگز یک قاب کرایپکه نیست اگر F یک قاب کرایپکه با عمق بینهایت باشد.
قضایای حفظ (Preservation theorems)
ارزش همراهان مُدال و قضیه بلوک–اساکیا به عنوان ابزاری برای تحقیق در منطقهای میانی، از این واقعیت ناشی میشود که بسیاری از خواص جالب منطقها توسط برخی یا تمام نگاشتهای ρ، σ، و τ حفظ میشوند. برای مثال:
- تصمیمپذیری (decidability) توسط
ρ،τ، وσحفظ میشود. - خاصیت مدل متناهی (finite model property) توسط
ρ،τ، وσحفظ میشود. - جدولی بودن (tabularity) توسط
ρوσحفظ میشود. - کامل بودن کرایپکه (Kripke completeness) توسط
ρوτحفظ میشود. - تعریفپذیری مرتبه اول بر روی قابهای کرایپکه (first-order definability on Kripke frames) توسط
ρوτحفظ میشود.
سایر خواص
هر منطق میانی L دارای تعداد بینهایت همراه مُدال است و علاوه بر این، مجموعه {M ∈ NExtS4 | ρM ∈ ExtL} شامل یک زنجیره نزولی بینهایت است. به عنوان مثال، ExtIPC شامل S5، و منطقهای Grz_n برای هر عدد صحیح مثبت n است، جایی که Grz_n منطق بر روی n-عنصری است. مجموعه همراهان مُدال هر L یا شمارا است، یا دارای کاردینالیتی پیوسته است. Rybakov نشان داده است که شبکه ExtL را میتوان در NExtS5 جاسازی کرد؛ به طور خاص، منطقی دارای پیوستار همراهان مُدال است اگر دارای پیوستار بسط باشد (این امر، برای مثال، برای تمام منطقهای میانی زیر KC صادق است). نامشخص است که آیا عکس این قضیه نیز صادق است یا خیر.
ترجمه گودل را میتوان برای قواعد نیز به کار برد:
T(R) = (T(A_1), ..., T(A_n) / T(B))
یک قاعده R در منطق L پذیرفتنی (admissible) است اگر مجموعه قضایای L تحت R بسته باشد. مشاهده میشود که R در یک منطق سوپر-انتوئیژنیستی L پذیرفتنی است هرگاه T(R) در یک همراه مُدال L پذیرفتنی باشد. عکس این قضیه به طور کلی درست نیست، اما برای بزرگترین همراه مُدال L صادق است.
منابع
- Alexander Chagrov and Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997.
- Vladimir V. Rybakov, Admissibility of Logical Inference Rules, vol. 136 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1997.