طريقة الحلّ

بيّن الدرس عن دلالات منطق القضايا أن الصحة المنطقية وقابلية التحقق قابلتان للتقرير بجدول الصدق، بكلفة تتضاعف مع كل متغير، وأعلن عن طرق لا تقتضي المرور عليه كله. وردّ الدرس عن النتيجة الدلالية والتكافؤ الدلالي كل نتيجة دلالية إلى عدم قابلية للتحقق: $\Gamma \models \varphi$ إذا وفقط إذا كانت $\Gamma \cup \{\neg\varphi\}$ غير قابلة للتحقق. وأعطى الدرسان عن الأشكال الناظمية وعن خوارزميتها كلَّ صيغة شكلًا عطفيًا تُرى صحته المنطقية بنظرة واحدة، أما قابليته للتحقق فلا تُرى. وإذا كان الأمر كذلك، فإنه ينقصنا إجراء يحسم في عدم قابلية التحقق لعطف من العبارات بالعمل على العبارات نفسها. وهذا الإجراء هو الحلّ، الذي اقترحه جون آلان روبنسون سنة 1965 بناءً على أفكار مارتن ديفيس وهيلاري بوتنام (1960)؛ وهو نواة البرامج التي تحسم اليوم في قابلية التحقق لصيغ ذات ملايين من المتغيرات. وخلافًا لنظام وحدة الاستنتاج، الذي يدرس علاقاتِه بالدلالة الدرسان عن السلامة والتمام وعن مبرهنة التراص، فإن الحلّ لا يستنتج نتائج: بل يدحض مجموعات. ويبرهن هذا الدرس على أنه يفعل ذلك على نحو سليم وتامّ.

كما في الدروس السابقة، تسمّي $p$ و$q$ و$r$ و$s$ و$t$ المتغيرات من $v_1$ إلى $v_5$؛ ويدلّ الحرف $v$ بلا دليل سفلي، وكذلك $w$، على إسنادات؛ و$V(\varphi)$ مجموعة متغيرات $\varphi$.

العبارات ومجموعات العبارات

لنتذكر من الدرس عن الأشكال الناظمية أن الحرفية متغير أو نفي متغير، وأن الحرفية المقابلة لحرفية $\ell$، وتُكتب $\ell^{*}$، هي حرفية المتغير نفسه ذات الإشارة الأخرى؛ وتشكّل حرفيتان متقابلتان زوجًا متتامًّا. وبتوطئة نفي الحرفية، $v(\ell^{*}) = 1 - v(\ell)$ لكل إسناد $v$. وهناك كانت العبارة فصلًا لحرفيات؛ وهنا يحسن أن ننسى الترتيب والتكرار، اللذين لا يغيّران القيمة، وأن نحتفظ بالمجموعة.

العبارة مجموعة منتهية من الحرفيات. والعبارة التي لا حرفيات فيها تسمّى العبارة الفارغة وتُكتب $\Box$. ويقال إن الإسناد $v$ يحقق العبارة $C$، ويُكتب $v \models C$، إذا كانت قيمة حرفية ما من $C$ هي $1$ في $v$؛ وإلا فإن $v$ يدحضها. والعبارة ذات الحرفية الواحدة تسمّى أحادية. ومتغيرات العبارة تشكّل المجموعة $V(C)$؛ ومتغيرات مجموعة $S$ من العبارات تشكّل المجموعة $V(S)$، وهي اتحاد ما سبق. ويحقق الإسناد مجموعة $S$ من العبارات، $v \models S$، إذا حقق كل عبارة من عباراتها؛ وتكون $S$ قابلة للتحقق إذا حققها إسناد ما، وغير قابلة للتحقق في الحالة المعاكسة. وأخيرًا، إذا كانت $S$ مجموعة من العبارات و$C$ عبارة، فإن $S \models C$ تعني أن كل إسناد يحقق $S$ يحقق $C$.

تلزم عن التعريف حالتان طرفيتان يحسن تثبيتهما. فالعبارة الفارغة لا حرفيات فيها؛ لذلك لا تساوي أي حرفية منها $1$، ولا يحققها أي إسناد: $\Box$ غير قابلة للتحقق، وكذلك كل مجموعة تحتويها. أما المجموعة الفارغة من العبارات فليس فيها عبارات يجب تحقيقها، وكل إسناد يحققها. ولا ينبغي الخلط بينهما: $\{\Box\}$ غير قابلة للتحقق، و$\emptyset$ تحققها جميع الإسنادات.

العبارة التي تحتوي زوجًا متتامًّا تسمّى تحصيلية: لا تفرض أي شرط، ويمكن حذفها من أي مجموعة دون تغيير نماذجها. وليست كتابة العبارات مجموعاتٍ نزوةً في الترميز. فإذا أردنا أن نحصل من $(p \vee q)$ و$(p \vee \neg q)$ على $p$، أعطى الفصل $(p \vee p)$، التي تكافئ $p$ لكنها ليست الصيغة نفسها؛ أما بالمجموعات، فإن $\{p\} \cup \{p\} = \{p\}$، ويحدث دمج الحرفيات المكررة من تلقاء نفسه.