منطق وجهی نرمال دوموضعی

در این مقاله، ابتدا معناشناسی کریپکی برای منطق وجهی نرمال با یک عملگر دو موضعی را تعریف کرده و سیستمی به نام k^2 را که نسبت به این معناشناسی درست و تمام است را معرفی خواهیم کرد. سپس دو نوع ترجمه ارائه خواهیم کرد و با استفاده از این ترجمه‌ها نشان خواهیم داد که منطق وجهی نرمال دو موضعی (k^2) و منطق وجهی نرمال استاندارد (k) بسیار به هم مرتبط هستند. یک ترجمه را تعبیر-پایدار می‌نامیم، در صورتی که اثبات‌پذیری در هر دو جهت حفظ شود. طبق این تعریف، ثابت خواهیم کرد که هر دو ترجمه‌ی معرفی شده، تعبیر-پایدار از k به k^2 و بالعکس هستند. یک توسیع از منطق k، یک مجموعه از فرمول‌ها است که شامل k است و تحت قواعد آن و جانشینی یکنواخت بسته است. توسیعی از منطق k^2 را نیز به همین صورت تعریف خواهیم کرد. در نهایت ثابت خواهیم کرد که یک تناظر یک-به-یک بین توسیع‌هایی از منطق k و منطق k^2 وجود دارد.

binary normal modal logic

in this article, first we define a kripke semantics for normal modal logic with a binary operator and we introduce a system k^2 which is sound and complete for this semantics. then, we will introduce two translations and show that binary normal modal logic k^2, and unary normal modal logic k, i.e. modal logic with one binary operator, are very closely related by these two translations. we call a translation a faithful interpretation if provability is preserved in both directions. so, with this terminology we will show that these two translations are faithful interpretation of k into k^2 and vice versa. a logic extending k will be a set of formulas containing k closed under its rules and uniform substitution. a logic extending k^2 is similarly defined. finally, we will prove that the classes of logics extending k and k^2 are closely related as well and there is a 1-1-correspondence between the logics extending k and extending k^2.