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

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