Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

ملخص تقني: أربع مفارقات ومساعد برهان

بيان المشكلة
تتناول الورقة الحدود التأسيسية لحساب التكوينات الاستقرائية (CIC)، وهو نظرية النوع التي تشكل البنية التحتية لمساعد البرهان "روك" (Rocq) (المعروف سابقاً باسم Coq). وبينما يُعد اتساق CIC أمراً راسخاً، فإن القرارات التصميمية المحددة التي تمنع عدم الاتساق — لا سيما فيما يتعلق بالاستدلال غير المحدد (impredicativity)، وقيود الأكوان (universe constraints)، والاستبعاد الكبير (large elimination) — غالباً ما تُعامل كقيود هندسية مجردة. تحتوي مكتبة coq-paradoxes، الموزعة مع Rocq، على أربعة اشتقاقات آلية لـ False (بورا-فورتي، دياكونيسكو، رينولدز، وهوركنز) تعتمد على فرضيات يرفضها نواة (kernel) Rocq. وتتمثل المشكلة المركزية في تفسير هذه الاشتقاقات ليس مجرد كفضول تاريخي أو حالات عدم اتساق معزولة، بل كـ "مواصفة سلبية" تحدد بدقة أين يجب على النواة رسم خطوطها للحفاظ على السلامة (soundness).

المنهجية
تعتمد الورقة على قراءة فاحصة للكود المصدري داخل مكتبة coq-paradoxes، من خلال تحليل أربعة ملفات تحديداً: BuraliForti.v و diaconescu.v و Reynolds.v و Hurkens_Set.v. تتضمن المنهجية ما يلي:

1. تفكيك الآليات المشتركة: تحليل Logics.v لفهم محدد الوصول (ACC) والبنية التحتية للترتيب الجيد (well-foundedness) المستخدمة في عدة مفارقات.
2. تتبع الاشتقاقات: تتبع الخطوات المنطقية في كل ملف لتحديد الفرضية المحددة (مثل: نوع عالمي للعلاقات، أو مبدأ اختيار، أو حقن من Prop إلى قضية واحدة) التي تؤدي إلى تناقض.
3. الربط بالرفض من قِبل النواة: ربط نقطة التناقض في الصياغة الرسمية بآلية محددة في نواة Rocq (حساب الأكوان، قواعد الاستبعاد، أو فحوصات الاستدلال غير المحدد) التي تمنع بناء الهيكل.
4. توليف القرارات التصميمية: تجميع النتائج لاستخراج ثلاثة شروط حدودية موحدة تحكم سلوك النواة.

المساهمات والنتائج الرئيسية

تحلل الورقة أربع مفارقات محددة، مظهرةً كيف يكشف كل منها عن ثغرة متميزة في نظرية النوع إذا تم تغيير بعض الخيارات التصميمية:

1. مفارقة بورا-فورتي (BuraliForti.v):

   • الآلية: تفترض وجود نوع عالمي للعلاقات $A_0$ وحقن $i_0$ يربط العلاقات بعناصر في $A_0$. يسمح هذا ببناء "ترتيب لجميع الترتيبات" ($\Omega$) يتم تضمينه في نفسه.
   • الرفض من قِبل النواة: تعتمد المفارقة على إحداث نسخة من $A_0$ لنفسها. تفرض نواة Rocq تسلسلاً صارماً للأكوان ($Type_j < Type_i$) لمنع النوع من احتواء صورته الخاصة. يؤدي هذا البناء إلى خطأ "عدم اتساق الكون" (Universe Inconsistency) لأن مستوى الكون المطلوب للنوع الداخلي يجب أن يكون على الأقل بقدر الكون الخاري، مما ينتهك القيود التراكمية للنواة.
   • النتيجة: تثبت ضرورة قيود تسلسل الأكوان لمنع التعريفات النوعية ذاتية المرجعية التي تؤدي إلى تناقضات النقطة الثابتة.

2. مفارقة دياكونيسكو (diaconescu.v):

   • الآلية: تستخدم نسخة نمطية من بديهية الاختيار (Tchoice) على علاقة تكافؤ فوق bool معرفة بواسطة قضية $P$. يُستخدم دالة الاختيار $f: bool \to bool$ لتقرير $P$ عبر مقارنة $f(\text{true})$ و $f(\text{false})$.
   • الرفض من قِبل النواة: تستخرج الحجة قراراً حوسبياً (دالة في Set) من برهان وجودي في Prop. هذا يشكل "استبعاداً كبيراً" (large elimination) من Prop إلى Set.
   • النتيجة: توضح أن السماح ببديهية الاختيار في Set (أو الاستبعاد الكبير من Prop إلى Set) يفرض قانون الثالث المرفوع (LEM) في النظام البنائي. تقيد النواة الاستبعاد الكبير لمنع استيراد المنطق الكلاسيكي إلى الطبقة الحوسبية.

3. مفارقة رينولدز (Reynolds.v):

   • الآلية: تعيد صياغة نتيجة رينولدز بأن نظام F ليس له نموذج نظري للمجموعات. تفترض حقناً $I: Prop \to Heyt$ (حيث $Heyt$ هي قضية واحدة) وتبني جبرًا قبليًا (ترميز كيرك - Church encoding) لدالة $\Phi$. باستخدام مبرهنة لافير للنقطة الثابتة، تشتق نقطة ثابتة للنفي، مما يؤدي إلى False.
   • الرفض من قِبل النواة: يعتمد البناء على عدم تحديد (impredicativity) الـ Prop (الاستدلال الكمي على جميع القضايا داخل Prop). ومع ذلك، تتطلب المفارقة حقناً من Prop إلى قضية واحدة، وهو ما ترفضه النواة على أسس كونية قبل الوصول إلى التناقض المنطري.
   • النتيجة: تسلط الضوء على دور الاستدلال غير المحدد في Prop. بينما Prop غير محدد، تمنع النواة عمليات الحقن الهيكلية التي قد تسمح لبرهان كانتور القطري بانهيار كون القضايا.

4. مفارقة هوركنز (Hurkens_Set.v):

   • الآلية: تعديل لتبسيط هوركنز لمفارقة جيرارد. تفترض وجود تراجع (retract) بين Prop و bool (عبر النفي المزدوج) وتستخدم عدم تحديد Set (إذا تم تفعيله) مع الاستبعاد الكبير لبناء علاقة ذاتية المرجعية مرتبة جيداً تؤدي إلى False.
   • الرفض من قِبل النواة: تتطلب المفارقة كلاً من عدم تحديد في Set و الاستبعاد الكبير (استخراج القيم البوليانية من المحتوى القضوي). تحافظ نواة Rocq الافتراضية على كون Set محدداً (predicative) وتقيد الاستبعاد من Prop.
   • النتيجة: تظهر أن الجمع بين عدم التحديد والاستبعاد الكبير في Set يتنافى مع المنطق الكلاسيكي (LEM). قرار النواة بإبقاء Set محدداً وتقييد الاستبعاد هو صمام الأمان.

الأهمية والادعاءات

تجادل الورقة بأن حزمة coq-paradoxes تعمل كـ مواصفة سلبية لنواة Rococ. فبدلاً من مجرد سرد حالات عدم الاتساق، تقدم الحزمة برهاناً رسمياً عن طريق "المثال الفاشل" لسلامة النواة.

• ثلاثة شروط حدودية: تلخص الورقة المفارقات الأربع في ثلاثة قرارات تصميمية تفرضها النواة:

  1. تسلسل الأكوان: يمنع الأنواع من الاستدلال الكمي على نفسها بطريقة تخلق نقاطاً ثابتة (بورا-فورتي).
  2. وضع الاستدلال غير المحدد: يحصر الاستدلال غير المحدد في Prop (ويمكن لـ Set مع تحفظات)، مما يمنع تناقضات رينولدز وهوركنز.
  3. ضبط الاستبعاد الكبير: يقيد استخراج المحتوى الحوسبي (مثل bool أو الدوال في Set) من البراهين القضوية، مما يمنع تناقضات دياكونيسكو وهوركنز.

• الدور الميتا-رياضي: تدعي الورقة أن الحزمة هي قطعة فريدة من الرياضيات الميتافيزيقية المكتوبة داخل النظام الذي توثقه. هي لا تثبت نظريات للتطبيق، بل تثبت عدم قابلية تحقق فرضيات معينة. ويُظهر "رفض" النواة أنه نتيجة لسياسات موحدة (حساب الأكوان، قواعد الاستبعاد) وليس مجرد إصلاحات عشوائية.

• الخلاصة: تكمن الأهمية في إظهار أن رفض نواة Rococ لبناء هذه الهياكل ليس عشوائياً، بل هو الآلية الهيكلية الدقيقة المطلوبة للحفاظ على اتساق CIC. وتؤكد الحزمة أن قرارات تصميم النواة قد اتُخذت "للأسباب الصحيحة"، حيث ترسم حدود النظام من الخارج إلى الداخل.