بازی‌های منطقی

بازی‌های منطقی حالت خاصی از بازی‌ها هستند که با توجه به ساختار مشخصشان در علم منطق ریاضی و نظریه محاسبات کاربرد دارند. در این بازی‌ها وجود راهبرد پیروزی بررسی و معانی مختلفی به آن منسوب می‌شود. تفاوت‌های اصلی این بازی‌ها با نسخهٔ عام‌تر بازی که در نظریه بازی‌ها بررسی می‌شود، وجود تنها ۲ بازیکن، تعداد مراحل نامحدود، سنجیدن نتیجه به شکل برد یا باخت و عدم وجود استراتژی‌های ترکیبی می‌باشد.

امروزه این نوع بازی‌ها علاوه بر کاربردهای نظری، در علومی مانند نظریه استدلال و مناظره نیز کاربرد دارند.

بازی‌های منطقی

یک بازی منطقی به شکل یک دنبالهٔ نامتناهی از تصمیم‌های دو بازیکن اجرا می‌شود. در هر مرحله دقیقاً یک بازیکن حق انتخاب دارد و تصمیمات دو بازیکن از دامنهٔ $\Omega$ اتخاذ می‌شوند. بعد از تعدادی متناهی یا نامتناهی مرحله یک بازیکن می‌تواند به پیروزی برسد و دیگری شکست بخورد، بعد از این اتفاق ادامهٔ بازی نتیجهٔ حاصل را تغییر نمی‌دهد. به دلیل استدلالی که جلوتر مطرح می‌شود، دو بازیکن را $\forall$ و $\exists$ می‌نامیم. همچنین هر دنبالهٔ متناهی از تصمیمات را یک وضعیت بازی و هر دنبالهٔ نامتناهی از تصمیمات را یک واقعیت بازی می‌نامیم. پس به عنوان تعریف دقیق، یک بازی منطقی ۴ تایی $(\Omega ,\tau ,W_{\forall },W_{\exists })$ است به طوری $\Omega$ مجموعه‌ای از انتخاب‌ها، $\Omega ^{*}$ مجموعهٔ وضعیت‌های بازی و $\Omega ^{\omega }$ مجموعهٔ واقعیت‌های بازی باشند. $\tau$ در نفش تابع نوبت، هر عضو از $\Omega ^{\omega }$ را به $\exists$ یا $\forall$ متناظر می‌کند. در نهایت $W_{\exists }$ و $W_{\forall }$ زیرمجموعه‌هایی از اجتماع وضعیت‌ها و واقعیت‌های بازی هستند که با توجه به ثبات پیروزی، شرایط ذیل را ارضا می‌کنند:

$\forall \alpha \in (W_{\forall }\cap \Omega ^{*}):\forall \beta \in (\Omega ^{*}\cup \Omega ^{\omega }):(\alpha .\beta \in W_{\forall })$

$\forall \alpha \in (W_{\exists }\cap \Omega ^{*}):\forall \beta \in (\Omega ^{*}\cup \Omega ^{\omega }):(\alpha .\beta \in W_{\exists })$

$W_{\forall }\cap W_{\exists }=\emptyset$

بازی‌های منطقی با نام Gale-Stewart نیز شناخته می‌شوند.

تاریخچه

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

کاربردها

هر جا که بازی و منطق در هم تنیده شده‌اند و استدلال تعاملی مطرح است، می‌توان کاربردی برای بازی‌های منطقی یافت. تفاوت اصلی کاربردهای این شاخه با نظریهٔ بازی‌های تکراری، تمرکز روی برد و باخت و ساختار نتیجه‌گیری به جای محاسبهٔ سود و انگیزه‌های بازیکنان است.

استدلال تحلیلی

نوعی از یک بازی منطقی است که در آزمون‌های پذیرش مدارس حقوق رواج دارد. این بازی که به چهار دستهٔ خطی ساده، خطی پیچیده، گروهی و گروهی با ترکیبیات خطی تقسیم می‌شود، می‌تواند برای افزایش پیچیدگی شامل مفاهیم تناظر، ترتیب و جایگشت شود. فرضیات بازی مجموعه‌ای از شواهد و قوانین می‌باشد و بازیکنان باید تا مشخص شدن اطلاعات مخفی، نتیجه‌گیری‌های مد نظر را پیش ببرند.

مناظره

از دیرباز اعتبار صحت تعامل دو یا چند فرد به شکل محاوره‌ای در راستای اثبات یک یا چند گزاره مورد بحث بوده‌است. ارائهٔ مدل منطقی بر پایهٔ بازی می‌تواند به تحلیل و بررسی یک مناظره بپردازد و حتی راهکارهایی برای پیش‌برد آن ارائه دهد. این شاخه در تحلیل مناظرات سیاسی، قراردادهای مالی و پرونده‌های حقوقی کاربرد دارد.

سرگرمی‌های منطقی

بازی‌های سرگرم‌کننده‌ای که استدلال و نتیجه‌گیری منطقی را از بازیکن طلب می‌کنند در این دسته قرار می‌گیرند. معمای منطقی لوئیس کارول، که با کتاب‌های آلیس در سرزمین عجایب و آلیس آنسوی آینه در راستای ملموس کردن مفاهیم منطقی برای مخاطب عام شهره است، در کنار نمودار کرول به این دسته تعلق دارند. بازی‌هایی مثل سودوکو یا پیچ‌راهه‌های منطقی علی‌رغم اینکه ساختار کلامی ندارند می‌توانند در این دسته طبقه‌بندی شوند.

اثبات‌های تعاملی

بعضی از ابزارهای خودکار و نیمه‌خودکار اثبات ویژگی روی زبان‌های برنامه‌نویسی و ساختارهای رفتاری متفاوت، توانایی مدل‌سازی و استدلال روی ساختارهای تعاملی را نیز دارند. این ویژگی در پروژه‌های مرتبط به روش‌های صوری و درستی‌یابی صوری مفید واقع می‌شود و امکان تحلیل منطقی مفهوم هماهنگی در مهندسی نرم‌افزار بر پایه پیکرپار را فراهم می‌سازد.

ویژگی‌ها

تمامیت

یک بازی منطقی را تمام می‌نامیم اگر مجموعه‌های $W_{\forall }$ و $W_{\exists }$ خاصیت زیر را داشته باشند:

$\forall \alpha \in \Omega ^{\omega }:(\alpha \in W_{\forall }\lor \alpha \in W_{\exists })$

که شهودا به این معناست که برندهٔ هر بازی در زمان نامتناهی مشخص می‌شود و هر واقعیت بازی یک برنده دارد.

خوش‌تعریفی

اگر در یک بازی منطقی به ازای هر واقعیت، یکی از بازیکنان در تعداد متناهی مرحله به پیروزی برسد، آن بازی را خوش تعریف می‌نامیم:

$\forall \alpha \in \Omega ^{\omega }:\exists \beta \in \Omega ^{*}:(prefix(\beta ,\alpha )\land \beta \in (W_{\forall }\cup W_{\exists }))$

رابطهٔ $prefix\in (\Omega ^{*}\times \Omega ^{\omega })$ این‌گونه تعریف می‌شود: $prefix(\beta ,\alpha )\Leftrightarrow (\exists \gamma \in \Omega ^{\omega }:\beta .\gamma =\alpha )$

تناهی

اگر عدد طبیعی $k$ وجود داشته باشد به طوری که مستقل از روند بازی، در کمتر از $k$ مرحله برنده مشخص شود، بازی را متناهی می‌نامیم:

$\exists k\in \mathbb {N} :\forall \alpha \in \Omega ^{\omega }:\exists \beta \in \Omega ^{*}:(prefix(\beta ,\alpha )\land \beta \in (W_{\forall }\cup W_{\exists })\land |\beta |<k)$

مشخّص است که ویژگی تناهی، خوش‌تعریفی را نتیجه می‌دهد.

تعاریف متنوع

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

پیشبینی‌پذیری

استراتژی

در یک بازی منطقی، یه تابعی که به ازای هر وضعیت بازی تصمیم بازیکن را مشخّص می‌کند، استراتژی آن بازیکن می‌گوییم؛ بنابراین برای بازیکن $\forall$ تابع $s_{\forall }$ و برای بازیکن $\exists$ تابع $s_{\exists }$، به ازای هر ورودی از مجموعهٔ $\Omega ^{*}$ یک خروجی از مجموعهٔ $\Omega$ را مشخص می‌کنند. واضح است که برای دانستن روند بازی کافیست استراتژی‌های دو بازیکن را داشته باشیم. بدین ترتیب تابع $result$ را تعریف کنیم که یک بازی منطقی و دو استراتژی را به عنوان ورودی دریافت کرده و نتیجه را برمی‌گرداند:

$result:G,s_{\forall },s_{\exists },\to \{\forall ,\exists ,draw\}$

استراتژی برد

یک تابع تصمیم‌گیری را استراتژی برد می‌نامیم، اگر به ازای هر تصمیم‌گیری ممکن از سوی حریف، بازیکن را به پیروزی برساند. تابع $s_{\forall }$ در بازی $G$ استراتژی برد است اگر:

$\forall s_{\exists }:result(s_{\forall },s_{\exists },G)=\forall$

و مشابها برای $s_{\exists }$ تعریف می‌شود. یک بازی حداکثر برای یک بازیکن استراتژی برد دارد، چون اگر هر دو استراتژی برد داشته باشند می‌توان این دو استراتژی را مقابل یک‌دیگر اجرا کرد و نتیجه پیروزی هر دو بازیکن خواهد بود که تناقض است.

بازی‌های مصمم

یک بازی منطقی مصمم یا پیشبینی‌پذیر است اگر برای یکی از بازیکنان استراتژی برد داشته باشد. می‌توان نشان داد که هر بازی خوش‌تعریف، مصمم نیز هست.

ارتباط با منطق

در منطق مرتبهٔ اول از علائم $\forall$ و $\exists$ به معنای صور عمومی و صور وجودی استفاده می‌شود. هم‌نامی این دو صور با بازیکنان بازی‌های منطقی به این معناست که هر صور را می‌توان به شکل یک مرحله تصمیم‌گیری یکی از بازیکنان دید، بعضاً با توجه به حروف اول نام صورها، بازیکنان Abelard و Eloise نیز نامیده می‌شوند. بازیکن $\exists$ قصد دارد تا نمونه‌ای پیدا کند که عبارت را صحیح و بازیکن $\forall$ به دنبال نمونه‌ای است که عبارت را ناصحیح کند. می‌دانیم که به ازای هر عبارت در منطق مرتبه اول، یک عبارت در فرم نرمال وجود دارد که تمام صورهای آن در ابتدای فرمول قرار دارند. همچنین اختصاص دادن مقادیر به متغیرهای صورها مقدار عبارت داخلی را مشخص می‌کند. بدین ترتیب یک فرمول را می‌توان به شکل یک بازی منطقی دید که ابتدا بازیکنان برای متغیرها مقدار انتخاب می‌کنند و سپس صحیح یا ناصحیح بودن عبارت برندهٔ بازی را مشخص می‌کند. واضح است که این بازی متناهی و نتیجتاً خوش‌تعریف می‌باشد پس برای یک بازیکن استراتژی برد داریم. این استدلال مشابه قضیهٔ تمامیت معنایی منطق مرتبهٔ اول است.

بازی‌های پس و پیش

بازی‌های پس و پیش برای اثبات هم‌ارزی دو ساختار در منطق مرتبهٔ اول معرفی شدند. در این بازی‌ها تصمیمات هر بازیکن دامنهٔ ساختار متناظر است. هدف بازیکن همانندساز اثبات هم‌ارزی این دو ساختار است و بازیکن خراب‌کار در صورت ناتوانی حریف خود پیروز می‌شود. بازی به این شکل پیش می‌رود که در هر مرحله، بازیکن خراب‌کار یک عضو را انتخاب کرده و بازیکن همانندساز عضوی را انتخاب می‌کند که در کنار اعضای پیشین رفتاری مشابه اعضای انتخاب شده توسط خراب‌کار داشته باشد. در هر مرحله اگر تفاوتی در رفتار دیده شد بازیکن خراب‌کار پیروز می‌شود و اگر هیچ‌وقت بازیکن خراب‌کار پیروز نشد، بازیکن همانندساز را پیروز می‌دانیم. پس تعریف می‌کنیم روی ساختار $S$ با مجموعه توابع $F$ و مجموعه روابط $R$، هر وضعیت بازی به شکل دنبالهٔ انتخاب شده توسط دو بازیکن است:

$(a_{1},a_{2},...,a_{n}),(b_{1},b_{2},...,b_{n})\in S^{*}$

بازیکن خراب‌کار در این مرحله بازی را برده‌است اگر یکی از این سه شرط ارضا شود:

$\exists p:\exists f\in F:(f(a_{p_{1}},a_{p_{2}},...,a_{p_{k-1}})=a_{p_{k}})\neq (f(b_{p_{1}},b_{p_{2}},...,b_{p_{k-1}})=b_{p_{k}})$

$\exists p:\exists r\in R:r(a_{p_{1}},a_{p_{2}},...,a_{p_{k}})\neq r(b_{p_{1}},b_{p_{2}},...,b_{p_{k}})$

$\exists i,j:(a_{i}=a_{j})\neq (b_{i}=b_{j})$

که $p$ یک جایگشت جزئی از اعداد کمتر از $n$ است.

و بازیکن همانندساز برنده است اگر بازیکن خراب‌کار در هیچ مرحله‌ای پیروز نشود.

واضح است که اگر دو ساختار مذکور معادل باشند بازیکن همانندساز استراتژی برد دارد. همچنین اگر همانندساز استراتژی برد داشته باشد دو ساختار را هم‌ارز پس و پیش، و اگر همانندساز یک استراتژی داشته باشد که تا مرحلهٔ $k$ شکست نخورد دو ساختار را هم‌ارز پس و پیش مرتبهٔ $k$ می‌نامیم.

اثبات تعاملی

در نظریهٔ پیچیدگی محاسبات، سیستم‌های اثبات تعاملی محاسبه را به شکل دنباله‌ای از پیام‌ها میان اثبات‌کننده و مصحح می‌بینند. اثبات‌کننده ماشینی با توانایی نامحدود است که می‌تواند دروغ یا راست بگوید و مصحح ماشینی با توانایی محدود است که باید صحت پیام‌های اثبات‌کننده را ارزیابی کند. از ساده‌ترین کلاس‌های پیچیدگی اثبات‌های تعاملی می‌توان کلاس $NP$ را نام برد که با تبادل یک پیام به پایان می‌رسد. اگر ورودی به زبان تعلق نداشته باشد هیچ اثبات‌کنندهٔ بدخواهی نمی‌تواند مصحح را به دروغ متقاعد کند و اگر ورودی به زبان تعلق داشته باشد اثبات‌کننده‌ای وجود دارد که می‌تواند با ارائهٔ اثبات صحیح، مصحح را متقاعد کند. کلاس پیچیدگی $Arthur-Merlin$ یا به اختصار $AM$ مشابه با $NP$ است با این تفاوت که مصحح ممکن است با احتمال حداکثر $1/3$ اثبات درست را نپذیرد یا اثبات غلط را بپذیرد.