انتقل إلى المحتوى
Topos Uranos
العربية

مبرهنة التراص

ملخص

الاستنتاج متتالية منتهية ولا يستعمل إلا عددًا منتهيًا من المقدمات؛ أما تحقيق مجموعة غير منتهية من الصيغ فيتطلب إسنادًا واحدًا يعطي القيمة 11 لصيغ غير منتهية العدد في آن واحد، ولا شيء في تعريفه يقول إنه يكفي فحص أجزاء منتهية. وتؤكد مبرهنة التراص أن ذلك يكفي: تكون مجموعة من الصيغ قابلة للتحقق إذا وفقط إذا كانت كل مجموعة من مجموعاتها الجزئية المنتهية قابلة للتحقق. ويبرهن هذا الدرس عليها بحجة دلالية مباشرة، دون المرور بالاستنتاج: تُثبَّت قيم المتغيرات v1,v2,…v_1, v_2, \ldots واحدةً بعد أخرى، مع الحفاظ في كل خطوة على اللامتغيّر القائل إن كل مجموعة جزئية منتهية من المجموعة تبقى قابلة للتحقق بإسناد يحترم ما ثُبّت من قبل؛ ولو لم يحافظ عليه أيٌّ من الاختيارين الممكنين، لناقض اتحادُ الشاهدين المنتهيين على هذا الإخفاق اللامتغيّرَ السابق، وفي النهاية تتحقق كل صيغة بتوطئة التطابق، لأن فيها عددًا منتهيًا من المتغيرات. ولأن المتغيرات مرقّمة، لا يحتاج البناء إلى مسلّمة الاختيار. ومن التراص تلزم صوره المتكافئة (تكون المجموعة غير قابلة للتحقق إذا وفقط إذا كان جزء منتهٍ ما منها غير قابل للتحقق؛ وتكون الصيغة نتيجة لمجموعة إذا وفقط إذا كانت نتيجة لجزء منتهٍ ما منها)، ومع التمام للمقدمات المنتهية من الدرس السابق، يلزم التمام القوي: Γ⊨φ\Gamma \models \varphi يستلزم Γ⊢φ\Gamma \vdash \varphi لكل مجموعة Γ\Gamma، ومن ثم يتطابق الاستنتاج والنتيجة الدلالية دائمًا. ويختم الدرس بتطبيقات توافقية: تلوين البيانات غير المنتهية انطلاقًا من تلوينات أجزائها المنتهية، والحدود العليا المنتهية التي تختبئ في العبارات غير المنتهية، وحدود ما تستطيع مجموعة من الصيغ أن تعبّر عنه.

أهداف التعلم

  1. تعريف المجموعات القابلة للتحقق منتهيًا والبرهنة على مبرهنة التراص بالتثبيت المتتابع لقيم المتغيرات، مع شرح دور اللامتغيّر وحجة الشاهدين وتوطئة التطابق، ولماذا لا يحتاج البناء إلى مسلّمة الاختيار.
  2. صياغة الصور المتكافئة للتراص، صورة عدم القابلية للتحقق وصورة النتيجة، والبرهنة عليها وتطبيقها، والانتقال من كل واحدة منها إلى الأخريين.
  3. استنتاج التمام القوي من التراص، ومن التمام للمجموعات المنتهية من المقدمات، ومن الرتابة، واستخلاص تطابق الاستنتاج مع النتيجة الدلالية وتطابق الاتساق مع القابلية للتحقق منه.
  4. ترميز مسائل توافقية عن مجموعات غير منتهية (التلوينات، والترتيبات، والمزاوجات) في مجموعات من الصيغ وحلّها بالتراص، مع التمييز بين ما تضمنه المبرهنة وما لا تضمنه.

ما يُستعمل من الدروس السابقة

يعمل هذا الدرس كله تقريبًا في الدلالة، ويستعمل منها ما يلي. الإسناد دالة v ⁣:V→{0,1}v\colon V \to \{0, 1\} على المجموعة VV للمتغيرات v1,v2,v3,…v_1, v_2, v_3, \ldots، تمتدّ بطريقة وحيدة إلى جميع الصيغ؛ ويقال إن إسنادًا يحقق مجموعة Γ\Gamma من الصيغ، v⊨Γv \models \Gamma، إذا أعطى القيمة 11 لكل واحدة منها، وتكون Γ\Gamma قابلة للتحقق إذا حققها إسناد ما، وغير قابلة للتحقق في الحالة المعاكسة. وكل ذلك في الدرس عن دلالات منطق القضايا، مع الأداة المركزية لهذا الدرس، توطئة التطابق: إذا تطابق إسنادان على متغيرات φ\varphi، وهي مجموعة منتهية V(φ)V(\varphi)، فإنهما يعطيان φ\varphi القيمة نفسها.

ومن الدرس عن النتيجة الدلالية والتكافؤ الدلالي يُستعمل تعريف Γ⊨φ\Gamma \models \varphi (كل إسناد يحقق Γ\Gamma يحقق φ\varphi)، وخواصها البنيوية، ولا سيما الرتابة (إذا Γ⊆Δ\Gamma \subseteq \Delta وΓ⊨φ\Gamma \models \varphi، فإن Δ⊨φ\Delta \models \varphi) والخاصية الخامسة (المجموعة غير القابلة للتحقق تلزم عنها كل صيغة)، ومبرهنة «النتيجة وعدم القابلية للتحقق»: Γ⊨φ\Gamma \models \varphi إذا وفقط إذا كانت Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} غير قابلة للتحقق. ومن الدرس عن قوانين دي مورغان وقوانين التوزيع المعمّمة تُستعمل توطئة القيمة: تأخذ ⋀i=1nφi\bigwedge_{i=1}^{n} \varphi_i القيمة 11 إذا وفقط إذا أخذت جميع حدودها القيمة 11، وتأخذها ⋁i=1nφi\bigvee_{i=1}^{n} \varphi_i إذا وفقط إذا أخذ حدّ منها القيمة 11. وأخيرًا، ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) تحصيل حاصل و⊥:=¬⊤\bot := \neg\top تناقض.

ومن جهة الاستنتاج، برهن الدرس عن الأنظمة الاستنتاجية الصورية على الرتابة (رتابة: إذا Γ⊆Δ\Gamma \subseteq \Delta وΓ⊢φ\Gamma \vdash \varphi، فإن Δ⊢φ\Delta \vdash \varphi) وعلى الطابع المنتهي (تناهي: إذا Γ⊢φ\Gamma \vdash \varphi، فإن مجموعة جزئية منتهية ما Γ0\Gamma_0 من Γ\Gamma تستوفي الشرط Γ0⊢φ\Gamma_0 \vdash \varphi)، وتحقّق الدرس عن أربع تقنيات للاستنتاج من أنهما تصحّان في نظام الدورة (المخططات A1 وA2 وA3، وقاعدة الوضع، وإبدال النفي المزدوج)، الذي يشير إليه الرمز ⊢\vdash فيما يلي. وأخيرًا، برهن الدرس عن السلامة والتمام على مبرهنة السلامة (Γ⊢φ\Gamma \vdash \varphi يستلزم Γ⊨φ\Gamma \models \varphi، لكل Γ\Gamma) وعلى التمام للمجموعات المنتهية من المقدمات: إذا {γ1,…,γk}⊨φ\{\gamma_1, \ldots, \gamma_k\} \models \varphi، فإن {γ1,…,γk}⊢φ\{\gamma_1, \ldots, \gamma_k\} \vdash \varphi.