ما وراء النظرية: الخلاصة والتحديات

ملخص

يختم هذا الدرس الوحدة المخصّصة لما وراء النظرية، ويختم معها محتوى الدورة. فهو يعيد بناء السلسلة الاستنتاجية التي تمتدّ من الصحة المنطقية للمسلّمات إلى سلامة النظام؛ ومن توطئتي النفي المشترك إلى توطئة كالمار وإلى التمام للمقدمات المنتهية؛ ومن توطئة الشاهدين إلى مبرهنة التراص، وبواسطتها إلى التمام القوي؛ ومن الشكل العباري إلى سلامة طريقة الحلّ وتمام الدحض فيها، مبيّنًا في كل حلقة ما تستعمله من نتائج وفي أي درس يُبرهن عليها. ويبيّن كيف تلتقي في تطابق $\vdash$ و $\models$ الأجزاء الثلاثة السابقة من الدورة، أي اللغة والاستنتاج والدلالة، وما يسهم به كلٌّ منها في هذا التطابق؛ ويميّز ما برهنت عليه الدورة مما سلّمت به ومما تتركه مفتوحًا. ويعيد في تقييم الخروج المهارات التي قاسها تقييم الدخول، ويُختم بستة تحدّيات، أصعب من مسائل الدروس، تتطلّب الجمع بين أدوات عدة منها.

أهداف التعلم

إعادة بناء الترتيب المنطقي لنتائج الوحدة، مع تعيين النتائج السابقة التي تستند إليها كل نتيجة والدرس الذي يُبرهن عليها فيه، وتسويغ ترتيب التراص والتمام القوي.
شرح كيف تلتقي اللغة والاستنتاج والدلالة في تطابق $\vdash$ و $\models$ ، وأي نتيجة من كل وحدة من وحدات الدورة لا غنى عنها لهذا التطابق.
التمييز بين ما برهنت عليه الدورة وما سلّمت به (مخططات المسلّمات، والقواعد الأولية، والاستقراء) وما تتركه مفتوحًا (كلفة الحسم في قابلية التحقق، والمنطق ذو المكمّمات).
حلّ مسائل تجمع بين العلامات وتوطئة كالمار والتعويض المنتظم والتراص والحلّ، باستعمال الجانب السهل من التطابق في كل حالة.

ما حقّقته الوحدة

وضعت الوحدة نصب عينيها مقارنة العلاقتين اللتين بنتهما الوحدات السابقة على اللغة نفسها، أي قابلية الاستنتاج $\Gamma \vdash \varphi$ والنتيجة الدلالية $\Gamma \models \varphi$ ، والبرهان على أنهما تتطابقان. وقد تحقق هذا المقصد دون تحفّظات في الصياغات: فالعلاقتان علاقة واحدة لكل مجموعة من المقدمات، منتهية كانت أو غير منتهية، والحلّ يقدّم طريقًا ثالثًا، سليمًا وتامًّا بالقدر نفسه، للحسم في النتيجة. أما التحفّظات فهي في الطرائق، وقد صُرّح بكلٍّ منها في موضعه: فالتمام في الدرس الأول بنائي لكنه غير عملي، لأنه ينتج استنتاجات طويلة بطول الجدول؛ والتراص يضمن وجود إسناد، لكنه لا يعلّم كيف يُعثر عليه؛ والحلّ يحسم، لكن كلفته في أسوأ الحالات مسألة مفتوحة. ومع هذه التحفّظات، يمكن أن يُقرأ الطريق المقطوع سلسلةً استنتاجية واحدة من أربعة مقاطع.

السلامة

بدأ الدرس الخاص بـالسلامة والتمام بتثبيت المصطلحات: يكون النظام سليمًا إذا كان $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ ، وتامًّا إذا صحّ العكس، وذلك في ثلاث درجات (الضعيف، وللمجموعات المنتهية، والقوي). وفكّك حجة دائرية تزعم الحصول على التمام «من السلامة» بالانتقال من $\nvdash \chi$ إلى $\not\models \chi$ ، وهو انتقال يمثّل عكس النقيض للتمام الضعيف، وبيّن أن الخاصيتين مستقلتان. ثم برهن على أن كل حالة خاصة من A1 وA2 وA3 صحيحة منطقيًا، بافتراض إسناد يدحضها والوصول، عبر السطر الكاذب للاستلزام، إلى قيم مستحيلة؛ وبرهن، بالاستقراء القوي على عدد الأسطر، على السلامة، بحالة للمسلّمات وأخرى للمقدمات، وقاعدة الوضع الدلالية، ولقاعدة إبدال النفي المزدوج، التكافؤ $\theta \eqsem \neg\neg\theta$ مع مبرهنة الإبدال الدلالي. والخاصية التي تنتقل من سطر إلى سطر ليست الصحة المنطقية، بل التحقق بإسناد ثابت يحقق المقدمات، ولذلك تصحّ السلامة مع المقدمات، ولو كانت غير منتهية. ولزم عنها اتساق كل مجموعة قابلة للتحقق، ولا سيما اتساق النظام، والطريقة التي لم تكن لدى وحدة الاستنتاج: النموذج المضاد يبرهن على أن استنتاجًا ما غير موجود.

كالمار والتمام المنتهي

وبرهن الدرس نفسه على العكس في خطوتين. الأولى توطئة كالمار: إذا كانت متغيرات $\varphi$ من بين $u_{1}, \ldots, u_{n}$ ، فإن $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ لكل إسناد $v$ ، حيث $\psi^{v}$ هي $\psi$ إذا كان $v(\psi) = 1$ و $\neg\psi$ فيما عدا ذلك؛ فالنظام يستنتج من كل سطر ما يقوله السطر عن الصيغة. وليس لاستقرائها على التعقيد إلا حالة مركبة واحدة، هي $(\alpha \downarrow \beta)$ ، لأن النفي المشترك هو الرابط الأولي الوحيد، وفيها ثلاث حالات فرعية تتطلب توطئتين من النظام، الثانية منهما بصورتين: $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ ، المستنتجة بإدخال العطف والنفي المزدوج وتطبيقين لقاعدة إبدال النفي المزدوج، و $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ و $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ ، المستنتجتان بإدخال الفصل. والخطوة الثانية تحذف المقدمات: إذا كانت $\varphi$ تحصيل حاصل، فإنها تُستنتج من مقدمات كل سطر من الأسطر الـ $2^{n}$ ، والبرهان بالحالات يحذف حرفية المتغير الأخير، ثم حرفية ما قبله، حتى الوصول إلى $\vdash \varphi$ ، أي التمام الضعيف. وبمبرهنة الاستنتاج الدلالية وبعكس المبرهنة التركيبية، امتدّ التمام إلى المجموعات المنتهية من المقدمات؛ ومن ثم، في حالة المقدمات المنتهية، يتطابق الاستنتاج والنتيجة، ويتطابق التكافؤ الاستنتاجي مع الدلالي، وتكون قابلية الاستنتاج قابلة للتقرير، لأن الجدول يجيب عنها.

التراص والتمام القوي

تناول الدرس الخاص بـمبرهنة التراص الحالة غير المنتهية، التي لا تبلغها توطئة كالمار، لأن المقدمات غير المنتهية لا تُفرَّغ في استلزام. وبرهن، دون ذكر أي استنتاج، على أن مجموعة ما قابلة للتحقق إذا وفقط إذا كانت كل مجموعة من مجموعاتها الجزئية المنتهية قابلة للتحقق. وتكون متتالية من القيم لـ $v_{1}, \ldots, v_{n}$ جيدة إذا كانت كل مجموعة جزئية منتهية من المجموعة تتحقق بإسناد ما يمدّدها؛ وتضمن توطئة الشاهدين أن المتتالية الجيدة تُمدَّد إلى متتالية جيدة، لأنه لو لم يكن أيٌّ من التمديدين جيدًا، لناقض اتحادُ الشاهدين المنتهيين كونَ المتتالية جيدة؛ والإسناد الناتج عن تفضيل $1$ دائمًا حين يكون ذلك ممكنًا يحقق كل صيغة، بتوطئة التطابق، لأن في كل صيغة عددًا منتهيًا من المتغيرات. ولا يحتاج البناء إلى مسلّمة الاختيار، لأن المتغيرات مرقّمة ولكل خطوة قاعدة. ومن التراص لزمت صوره المتكافئة، صورة عدم قابلية التحقق وصورة النتيجة؛ ومن الأخيرة، ومن التمام للمقدمات المنتهية ومن الرتابة، التمام القوي؛ ومنه ومن السلامة، التطابق الكامل: $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ لكل $\Gamma$ ، وتكون المجموعة متسقة إذا وفقط إذا كانت قابلة للتحقق. ونبّه الدرس إلى أن هذا الترتيب ليس مسألة تفضيل: فالحصول على التراص من تمام قوي لم يُحصَّل بعد يكون دائريًا. واختُتم بتلوين البيانات القابلة للعدّ، الذي يترجم مسألة غير منتهية إلى مجموعة من الصيغ أجزاؤها المنتهية قابلة للتحقق، وبحدود ما تستطيع مجموعة من الصيغ أن تعبّر عنه.

الحلّ

استبدل الدرس الخاص بـطريقة الحلّ بمجموعات الصيغ مجموعاتٍ من العبارات، كلٌّ منها مجموعة منتهية من الحرفيات، مع تمثيلين: الشكل العباري، الذي له النماذج نفسها، والشكل التعريفي، الذي يُدخل متغيرًا جديدًا لكل كتابة جزئية مركبة، ولا يحفظ إلا قابلية التحقق، وينمو كما تنمو الصيغة، لا كقوة للعدد اثنين. وتعمل على العبارات قاعدة واحدة: من $C$ و $D$ ، مع $\ell \in C$ و $\ell^{*} \in D$ ، يُستدلّ على $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ ، والدحض اشتقاق يصل إلى $\Box$ . وبُرهن على السلامة كما بُرهن على سلامة النظام، بالاستقراء على الاشتقاق، وبكون المحلِّلة نتيجة لمقدمتيها؛ وعلى تمام الدحض بالاستقراء على عدد المتغيرات، بحذف متغير يحفظ قابلية التحقق ويبني برهانه نموذجًا؛ وفي المجموعات غير المنتهية، بالتراص مرة أخرى. ونتج عن ذلك أن $\Gamma \models \varphi$ إذا وفقط إذا كان لشكل عباري لـ $\Gamma \cup \{\neg\varphi\}$ دحض، وأن الإشباع، وهو منتهٍ لأنه مع $n$ من المتغيرات لا يوجد أكثر من $4^{n}$ عبارة، يحسم في قابلية التحقق دون جداول. وعرض الدرس مسألة قابلية التحقق، التي لا يعرف أحد كلفتها في أسوأ الحالات، وحالتين تُحسمان بسرعة: عبارات هورن والعبارات ذات الحرفيتين.

يجمع الرسم التالي المقاطع الأربعة في سلسلة واحدة. كل عقدة في العمود نتيجة، مرقّمة بحسب الترتيب المنطقي، وموصولة بقوس بالحلقات السابقة التي يستعملها برهانها؛ وحولها تطفو الدعامات، أي المبادئ والأدوات التي ترجع إليها السلسلة مرة بعد مرة، وكلٌّ منها موصولة بخط متصل بالحلقات التي تستند إليها وبخط منقّط بالحلقة التي تُثبَت فيها، إلا ما جاء منها من الوحدات السابقة، فيُرسم أطواقًا. وعند النقر على دعامة تُبرَز كل الحلقات التي تستعملها، وتحيل كل حلقة إلى الدرس الذي يُبرهن عليها فيه. ويُلاحظ أن السلامة والتراص، اللذين ثبتا أحدهما في المقطع الأول والآخر في الثالث، يعودان إلى الظهور في المقاطع التالية، وأن أكثر الدعامات ورودًا في الوحدة هي الإسنادات والتطابق، ويليها الاستقراء بصوره الثلاث: على أسطر الاستنتاج، وعلى تعقيد الصيغة، وعلى عدد متغيرات مجموعة من العبارات.

دعامات السلسلة

Aالاستقراء والتراجع. الاستقراء القوي على الأعداد الطبيعية، والاستقراء على تعقيد الصيغ، وحالته المركبة الوحيدة $(\alpha \downarrow \beta)$ ، والتعريف بالتراجع. بُرهن عليها في الوحدة الأولى. يُقبل دون برهان في هذه الوحدة.
Bنظام الدورة. A1 وA2 وA3، وقاعدة الوضع، وقاعدة إبدال النفي المزدوج؛ والانعكاسية، والرتابة، وقاعدة الوضع بين الاستنتاجات، والطابع المنتهي، و $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ . ثُبّتت في الوحدة الثانية. يُقبل دون برهان في هذه الوحدة.
Cالتقنيات المشتقة. النفي المزدوج، من الدرس الخاص بالتقنيات الأربع؛ وإدخال العطف وإدخال الفصل والبرهان بالحالات (إذا كان $\Gamma \cup \{\psi\} \vdash \chi$ و $\Gamma \cup \{\neg\psi\} \vdash \chi$ ، فإن $\Gamma \vdash \chi$ )، من الدرس الخاص بتقنيات المنطق الكلاسيكي. بُرهن عليها في الوحدة الثانية. يُقبل دون برهان في هذه الوحدة.
Dالإسنادات والتطابق. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ؛ إذا تطابق إسنادان على $V(\varphi)$ ، أعطيا $\varphi$ القيمة نفسها؛ وتُحسم الصحة المنطقية بـ $2^{n}$ من الأسطر. بُرهن عليها في الوحدة الثالثة. يُقبل دون برهان في هذه الوحدة.
Eالنتيجة الدلالية. السطر الكاذب للاستلزام، والرتابة، و $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ ، و $\Gamma \models \varphi$ إذا وفقط إذا كانت $\Gamma \cup \{\neg\varphi\}$ غير قابلة للتحقق، ومبرهنة الإبدال الدلالي. بُرهن عليها في الوحدة الثالثة. يُقبل دون برهان في هذه الوحدة.
Fالأشكال العطفية. توطئة القيمة؛ كل صيغة تكافئ شكلًا ناظميًا عطفيًا قد يحتاج إلى $2^{n}$ من العبارات؛ والفصل بين حرفيات صحيح منطقيًا إذا وفقط إذا احتوى زوجًا متتامًّا. بُرهن عليها في الوحدة الثالثة. يُقبل دون برهان في هذه الوحدة.
Gالسلامة. إذا كان $\Gamma \vdash \varphi$ ، فإن $\Gamma \models \varphi$ ، لكل مجموعة $\Gamma$ ؛ والنموذج المضاد يبرهن على أن استنتاجًا ما غير موجود. تثبت في: 2. السلامة.
Hالتراص. تكون مجموعة من الصيغ قابلة للتحقق إذا وفقط إذا كانت كل مجموعة جزئية منتهية منها قابلة للتحقق؛ ومن ثم فإن ما ليس قابلًا للتحقق يكون كذلك في جزء منتهٍ منه. تثبت في: 11. مبرهنة التراص.

المقطع 1 السلامة
- التحقق من أن كل حالة خاصة من المخططات صحيحة منطقيًا دون بناء جدولها.
- البرهان على السلامة بالاستقراء القوي على عدد الأسطر، مع حالة قاعدة إبدال النفي المزدوج.
- البرهان بنموذج مضاد على أن صيغة ما لا تُستنتج، واستخلاص الاتساق من السلامة.
1. الصحة المنطقية للمسلّمات. كل حالة خاصة من A1 وA2 وA3 صحيحة منطقيًا: فالإسناد الذي يدحضها يقتضي، عبر السطر الكاذب للاستلزام، قيمًا مستحيلة.
  تستند إلى: E (النتيجة الدلالية). يُبرهن في: السلامة والتمام.
2. السلامة. إذا كان $\Gamma \vdash \varphi$ ، فإن $\Gamma \models \varphi$ ، لكل $\Gamma$ : بالاستقراء القوي على عدد الأسطر، بحالة للمسلّمات وأخرى للمقدمات، وقاعدة الوضع الدلالية، ولقاعدة إبدال النفي المزدوج، $\theta \eqsem \neg\neg\theta$ مع الإبدال الدلالي.
  تستعمل: 1. الصحة المنطقية للمسلّمات. تستند إلى: A (الاستقراء والتراجع), B (نظام الدورة), E (النتيجة الدلالية). يُبرهن في: السلامة والتمام.
3. الاتساق والنماذج المضادة. كل مجموعة قابلة للتحقق متسقة؛ والنظام متسق و $\nvdash v_{1}$ ؛ وإذا حقق إسناد ما $\Gamma$ ودحض $\varphi$ ، فإن $\Gamma \nvdash \varphi$ ، والجدول يشهد بأن ما ليس صحيحًا منطقيًا ليس مبرهنة.
  تستند إلى: G (السلامة), D (الإسنادات والتطابق). يُبرهن في: السلامة والتمام.
المقطع 2 كالمار والتمام المنتهي
- استنتاج توطئتي النفي المشترك في النظام، مع قاعدة إبدال النفي المزدوج حيث تلزم.
- البرهان على توطئة كالمار بالاستقراء على التعقيد، مع حالة مركبة واحدة.
- حذف مقدمات الأسطر بالبرهان بالحالات، وتفريغ المقدمات المنتهية بمبرهنتي الاستنتاج.
- الحسم بالجدول في قابلية الاستنتاج والتكافؤ الاستنتاجي والاتساق انطلاقًا من مقدمات منتهية.
1. إدخال النفي المشترك. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ و $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ : عطف النفيين هو $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ؛ والنفي المزدوج يزيل النفي الخارجي، وقاعدة إبدال النفي المزدوج تزيل النفيين الداخليين.
  تستند إلى: B (نظام الدورة), C (التقنيات المشتقة). يُبرهن في: السلامة والتمام.
2. نفي النفي المشترك. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ و $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ ، لأن $\neg(\alpha \downarrow \beta)$ هي $(\alpha \vee \beta)$ ويكفي إدخال الفصل.
  تستند إلى: B (نظام الدورة), C (التقنيات المشتقة). يُبرهن في: السلامة والتمام.
3. توطئة كالمار. إذا كان $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ ، فإن $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ لكل إسناد $v$ ؛ وليس لخطوة الاستقراء إلا حالة واحدة، هي $(\alpha \downarrow \beta)$ ، مع ثلاث حالات فرعية بحسب قيم $\alpha$ و $\beta$ .
  تستعمل: 4. إدخال النفي المشترك, 5. نفي النفي المشترك. تستند إلى: A (الاستقراء والتراجع), D (الإسنادات والتطابق), B (نظام الدورة). يُبرهن في: السلامة والتمام.
4. التمام الضعيف. إذا كان $\models \varphi$ ، فإن $\vdash \varphi$ : توطئة كالمار تستنتج $\varphi$ من كل سطر، والبرهان بالحالات يحذف الحرفيات من المتغير الأخير إلى الأول، مع $2^{n}$ من استعمالات التوطئة و $2^{n} - 1$ من استعمالات البرهان بالحالات.
  تستعمل: 6. توطئة كالمار. تستند إلى: C (التقنيات المشتقة). يُبرهن في: السلامة والتمام.
5. التمام للمقدمات المنتهية. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ : مبرهنة الاستنتاج الدلالية تقود إلى تحصيل حاصل، والتمام الضعيف يستنتجه، وعكس مبرهنة الاستنتاج يعيد المقدمات.
  تستعمل: 7. التمام الضعيف. تستند إلى: E (النتيجة الدلالية), B (نظام الدورة). يُبرهن في: السلامة والتمام.
6. التطابق المنتهي والحسم. لـ $\Gamma$ منتهية، $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ ، و $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ؛ ومن ثم فإن قابلية الاستنتاج من مقدمات منتهية قابلة للتقرير، بواسطة الجدول.
  تستعمل: 8. التمام للمقدمات المنتهية. تستند إلى: G (السلامة), D (الإسنادات والتطابق). يُبرهن في: السلامة والتمام.
المقطع 3 التراص والتمام القوي
- البرهان على التراص بتثبيت قيم المتغيرات واحدةً بعد أخرى، مع لامتغيّر المتتاليات الجيدة وحجة الشاهدين.
- الانتقال بين صورة قابلية التحقق وصورة عدم قابلية التحقق وصورة النتيجة.
- الحصول على التمام القوي من التراص، دون دائرية، ومنه على تطابق الاتساق مع قابلية التحقق.
- ترميز مسائل عن موضوعات غير منتهية في مجموعات من الصيغ وحلّها بالتراص.
1. توطئة الشاهدين. إذا كانت المتتالية $s$ من القيم المثبّتة جيدة (كل مجموعة جزئية منتهية من المجموعة تتحقق بإسناد يمدّدها)، فإن $(s, 1)$ أو $(s, 0)$ جيدة: لو لم تكن أيٌّ منهما جيدة، لناقض اتحادُ الشاهدين المنتهيين كونَ $s$ جيدة.
  تستند إلى: D (الإسنادات والتطابق). يُبرهن في: مبرهنة التراص.
2. مبرهنة التراص. تكون $\Gamma$ قابلة للتحقق إذا وفقط إذا كانت كل مجموعة جزئية منتهية قابلة للتحقق: تُثبَّت $v_{n + 1}$ على $1$ إذا كانت $(s_{n}, 1)$ جيدة، وعلى $0$ فيما عدا ذلك، والإسناد الناتج يحقق كل صيغة بتوطئة التطابق. ولا حاجة إلى مسلّمة الاختيار، لأن المتغيرات مرقّمة.
  تستعمل: 10. توطئة الشاهدين. تستند إلى: A (الاستقراء والتراجع), D (الإسنادات والتطابق). يُبرهن في: مبرهنة التراص.
3. الصور المتكافئة. تكون $\Gamma$ غير قابلة للتحقق إذا وفقط إذا كان جزء منتهٍ ما منها كذلك؛ و $\Gamma \models \varphi$ إذا وفقط إذا كان $\Gamma_{0} \models \varphi$ لمجموعة ما $\Gamma_{0} \subseteq \Gamma$ منتهية؛ وهذه الصورة الأخيرة تستلزم بدورها المبرهنة.
  تستعمل: 11. مبرهنة التراص. تستند إلى: E (النتيجة الدلالية). يُبرهن في: مبرهنة التراص.
4. التمام القوي. إذا كان $\Gamma \models \varphi$ ، فإن $\Gamma \vdash \varphi$ ، لكل $\Gamma$ : صورة النتيجة تعطي $\Gamma_{0}$ منتهية، والتمام للمقدمات المنتهية يعطي $\Gamma_{0} \vdash \varphi$ ، والرتابة تعطي $\Gamma \vdash \varphi$ .
  تستعمل: 8. التمام للمقدمات المنتهية, 12. الصور المتكافئة. تستند إلى: B (نظام الدورة). يُبرهن في: مبرهنة التراص.
5. الاستنتاج هو النتيجة. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ لكل $\Gamma$ ؛ والمبرهنات هي تحصيلات الحاصل بالضبط، وتكون المجموعة متسقة إذا وفقط إذا كانت قابلة للتحقق.
  تستعمل: 13. التمام القوي. تستند إلى: G (السلامة). يُبرهن في: مبرهنة التراص.
6. تلوين البيانات القابلة للعدّ. بمتغير $x_{i,c}$ لكل رأس ولون، وبصيغ تقول إن لكل رأس لونًا واحدًا لا غير وإن المتجاورين مختلفان، يقبل البيان القابل للعدّ تلوينًا بـ $k$ من الألوان إذا قبله كل بيان جزئي منتهٍ منه.
  تستند إلى: H (التراص), F (الأشكال العطفية). يُبرهن في: مبرهنة التراص.
المقطع 4 الحلّ
- تمثيل مجموعة من الصيغ بمجموعة من العبارات، بالشكل العطفي أو بالشكل التعريفي.
- بناء الدحوض دون حذف زوجين متتامّين في خطوة واحدة.
- البرهان على سلامة الحلّ وتمام الدحض فيه، للمجموعات المنتهية، وبالتراص لأي مجموعات.
- الحسم في النتائج بالإشباع، وتمييز الحالات التي تُحسم بسرعة.
1. الشكل العباري. العبارة مجموعة منتهية من الحرفيات، تتحقق إذا كانت قيمة إحداها $1$ ، و $\Box$ غير قابلة للتحقق؛ والشكل العباري لـ $\Gamma$ له النماذج نفسها، و $\Gamma \models \varphi$ إذا وفقط إذا كان شكل عباري لـ $\Gamma \cup \{\neg\varphi\}$ غير قابل للتحقق.
  تستند إلى: F (الأشكال العطفية), E (النتيجة الدلالية). يُبرهن في: طريقة الحلّ.
2. الشكل العباري التعريفي. بمتغير جديد لكل كتابة جزئية وعبارات تعريفه، تكون $T(\varphi)$ متساوية في قابلية التحقق مع $\varphi$ ، وفيها على الأكثر $4k + 1$ عبارة، في كل منها ثلاث حرفيات على الأكثر؛ والأشكال التعريفية تحسم في النتيجة من مقدمات منتهية.
  تستعمل: 16. الشكل العباري. تستند إلى: A (الاستقراء والتراجع), D (الإسنادات والتطابق). يُبرهن في: طريقة الحلّ.
3. سلامة الحلّ. $\{C, D\} \models R_{\ell}(C, D)$ ، بالحالات بحسب قيمة $\ell$ ؛ وبالاستقراء القوي على الاشتقاق، $S \models C$ لكل عبارة $C$ مشتقة من $S$ ، وإذا كان لـ $S$ دحض، فهي غير قابلة للتحقق.
  تستعمل: 16. الشكل العباري. تستند إلى: A (الاستقراء والتراجع). يُبرهن في: طريقة الحلّ.
4. حذف متغير. $E_{p}(S)$ ، التي تحفظ العبارات الخالية من $p$ ومن $\neg p$ وتضيف المحلِّلات على $p$ ، لا تحتوي $p$ وهي متساوية في قابلية التحقق مع $S$ ؛ ومن نموذج لها يُحصل على نموذج لـ $S$ باختيار قيمة $p$ .
  تستعمل: 18. سلامة الحلّ. تستند إلى: D (الإسنادات والتطابق). يُبرهن في: طريقة الحلّ.
5. تمام الدحض المنتهي. لكل مجموعة منتهية غير قابلة للتحقق من العبارات دحض، بالاستقراء على عدد المتغيرات: يُحذف الأخير وتُدرج مقدمتا كل محلِّلة.
  تستعمل: 19. حذف متغير. تستند إلى: A (الاستقراء والتراجع). يُبرهن في: طريقة الحلّ.
6. تمام الدحض. تكون مجموعة من العبارات، منتهية أو غير منتهية، غير قابلة للتحقق إذا وفقط إذا كان لها دحض؛ ومن ثم $\Gamma \models \varphi$ إذا وفقط إذا كان لشكل عباري لـ $\Gamma \cup \{\neg\varphi\}$ دحض.
  تستعمل: 16. الشكل العباري, 18. سلامة الحلّ, 20. تمام الدحض المنتهي. تستند إلى: H (التراص). يُبرهن في: طريقة الحلّ.
7. الإشباع يحسم. مع $n$ من المتغيرات، في مجموعة العبارات المشتقة على الأكثر $4^{n}$ عنصر؛ والإشباع ينتهي ويحسم في قابلية التحقق دون جداول، وإن لم يكن دائمًا أسرع منها.
  تستعمل: 18. سلامة الحلّ, 20. تمام الدحض المنتهي. يُبرهن في: طريقة الحلّ.

نهاية الدورة. تنتهي السلسلة حيث يُعرف وجها الدورة علاقةً واحدة، وحيث تتوفر طريقة للحسم فيها. وما يبقى مفتوحًا لم يعد سؤالًا عن منطق القضايا، بل عن كلفته وعن امتداده إلى المكمّمات.