Kripke’s Worlds: An Introduction to Modal Logics via Tableaux

مدل های جهان های ممکن توسط سائول کریپکه در اوایل دهه 1960 معرفی شدند. اساساً، مدل جهان ممکن چیزی نیست جز یک نمودار با گره‌های برچسب‌دار و لبه‌های برچسب‌دار. چنین نمودارهایی معناشناسی را برای منطق‌های مدال مختلف (اخلاق، زمانی، معرفتی و دوکساستیک، پویا، دئونتتیک، منطق توصیف) ارائه می‌کنند و همچنین برای سایر منطق‌های غیرکلاسیک (شهودی، شرطی، چندین منطق ناسازگار و مرتبط) مفید هستند. همه این منطق ها به طور فشرده در منطق فلسفی و ریاضی و در علوم کامپیوتر مورد مطالعه قرار گرفته اند و به طور فزاینده ای در حوزه هایی مانند معناشناسی برنامه ها، هوش مصنوعی و اخیراً در وب معنایی به کار گرفته شده اند. علاوه بر این، تمام این منطق ها نیز به صورت نظری اثبات مورد مطالعه قرار گرفتند. سیستم‌های اثبات منطق‌های مودال به سبک‌های مختلفی می‌آیند: سبک هیلبرت، استنتاج طبیعی، توالی‌ها و وضوح. با این حال، منصفانه است که بگوییم یکنواخت ترین و موفق ترین سیستم ها، سیستم های تابلوفرش هستند. با توجه به منطق و فرمول، آنها به فرد اجازه می دهند بررسی کند که آیا مدلی در آن منطق وجود دارد یا خیر. این اساساً به معنای تلاش برای ساختن مدلی برای فرمول با ساختن یک درخت است.

این کتاب با تلاش برای ساختن یک نمودار، رویکردی کلی‌تر را دنبال می‌کند، مزیت آن این است که یک نمودار به مدل کریپکی نزدیک‌تر است تا یک درخت. این یک مقدمه گام به گام با معناشناسی جهان های ممکن (و در نتیجه منطق های معین و سایر منطق های غیر کلاسیک) را از طریق روش تابلو ارائه می دهد. همراه با نرم افزاری به نام LoTREC (www.irit.fr/Lotrec) است. LoTREC اجازه می دهد تا بررسی کنید که آیا یک فرمول داده شده در یک دنیای معین از یک مدل معین درست است یا خیر و بررسی کنید که آیا یک فرمول داده شده در یک منطق معین قابل رضایت است یا خیر. اگر سیستم تابلوی آن منطق قبلاً در LoTREC پیاده‌سازی شده باشد، می‌توان آن را بلافاصله انجام داد. اگر هنوز اینطور نیست، LoTREC امکان پیاده‌سازی یک سیستم تابلو را به روشی نسبتاً آسان از طریق یک زبان تعاملی ساده، مبتنی بر نمودار ارائه می‌دهد.

Possible worlds models were introduced by Saul Kripke in the early 1960s. Basically, a possible world's model is nothing but a graph with labelled nodes and labelled edges. Such graphs provide semantics for various modal logics (alethic, temporal, epistemic and doxastic, dynamic, deontic, description logics) and also turned out useful for other nonclassical logics (intuitionistic, conditional, several paraconsistent and relevant logics). All these logics have been studied intensively in philosophical and mathematical logic and in computer science, and have been applied increasingly in domains such as program semantics, artificial intelligence, and more recently in the semantic web. Additionally, all these logics were also studied proof theoretically. The proof systems for modal logics come in various styles: Hilbert style, natural deduction, sequents, and resolution. However, it is fair to say that the most uniform and most successful such systems are tableaux systems. Given logic and a formula, they allow one to check whether there is a model in that logic. This basically amounts to trying to build a model for the formula by building a tree.

This book follows a more general approach by trying to build a graph, the advantage being that a graph is closer to a Kripke model than a tree. It provides a step-by-step introduction to possible worlds semantics (and by that to modal and other nonclassical logics) via the tableaux method. It is accompanied by a piece of software called LoTREC (www.irit.fr/Lotrec). LoTREC allows to check whether a given formula is true at a given world of a given model and to check whether a given formula is satisfiable in a given logic. The latter can be done immediately if the tableau system for that logic has already been implemented in LoTREC. If this is not yet the case LoTREC offers the possibility to implement a tableau system in a relatively easy way via a simple, graph-based, interactive language.