Support is Search

إليك ملخص تقني مفصل لورقة "الدعم هو بحث" (Support is Search) للباحث ألكسندر ف. غيورغيو.

1. بيان المشكلة

تتناول الورقة فجوة تأسيسية في دلالات تمديد القاعدة (Base-Extension Semantics - B-eS) للمنطق القضايا الحدسي (Intuitionistic Propositional Logic)، والتي طورها ساندكفيست.

• سؤال العالمي مقابل المحلي: أسس عمل ساندكفيست الأصلي مبرهنة اكتمال عالمية: تكون الصيغة $\phi$ صالحة حدسياً إذا وفقط إذا كانت "مدعومة" ($\Vdash_B \phi$) في كل قاعدة $B$ ممكنة. ومع ذلك، تحدد الورقة نقصاً في فهم السؤال المحلي: بالنسبة لقاعدة $B$ ثابتة، ما الذي تقصده علاقة الدعم $\Vdash_B \phi$ حسابياً بالضبط؟
• التوتر الواقعي (Realist Tension): يتضمن التعريف القياسي للدعم استقلالاً عن التكميم الشامل على جميع تمديدات القواعد ($C \supseteq B$) والذرات. عند قراءته بطريقة نموذجية كلاسيكية، يوحي هذا بوجود "مجموع مكتمل" من المجموعات اللانهائية، مما يتعارض مع الأسس المناهضة للواقعية (Anti-realist) للدلالات الإثباتية. تبدو الدلالات وكأنها تعتمد على حقائق عالمية غير بنائية بدلاً من إجراءات إثبات محلية وظاهرة.
• التحدي: يهدف المؤلفون إلى تقديم تفسير بنائي وحسابي كامل لـ $\Vdash_B \phi$ يتجنب الاستناد إلى اللانهايات المكتملة، وبالتالي إثبات صحة الموقف المناهض للواقعية وفقاً لمعاييره الخاصة.

2. المنهجية

يستخدم المؤلفون نهجاً حسابياً عن طريق ترميز الصيغ المنطقية إلى برامج منطقية من نوع هاروب الوراثي (Hereditary Harrop - HH) من الدرجة الثانية.

• الأنظمة الذرية كبرامج منطقية:

  • تعامل الورقة "القواعد" ($B$) ليس كمجموعات مجردة من القواعد، بل كبرامج في لغة برمجة منطقية.
  • تستخدم الورقة أنظمة ذرية عالية المستوى، حيث يمكن للقواعد تفريغ الفرضيات (مثل قواعد من الشكل $[A] \vdash B \implies C$). يتم رسم هذه القواعد إلى صيغ هاروب الوراثية (تحديداً الجمل المحددة ذات الاستلزامات المتداخلة).
  • للتعامل مع القواعد اللانهائية (المطلوبة للاكتمال) دون افتراض وجود لانهايات مكتملة، قدم المؤلفون كميات من الدرجة الثانية ($\forall X$) فوق المتغيرات الذرية. يسمح هذا بتمثيل القواعد المخططية (مثل "لكل الذرات $X$") بشكل منتهٍ.

• ترميز أسلوب تمرير الاستمرارية (Continuation-Passing Style - CPS):

  • الابتكار التقني الجوهري هو قراءة البنود الدلالية للدعم بأسلوب تمرير الاستمرارية (CPS).
  • بدلاً من تعريف الدعم مباشرة، يعرّف المؤلفون دالة ترميز $\llbracket \phi \rrbracket$ تربط الصيغة $\phi$ بهدف برمجة منطقية.
  • الترميزات الرئيسية:
    • الاستلزام ($\to$): $\llbracket \phi \to \psi \rrbracket = \llbracket \phi \rrbracket \supset \llbracket \psi \rrbracket$
    • الاقتران ($\land$): يُرمز له كـ $\forall X ((\llbracket \phi \rrbracket \supset \llbracket \psi \rrbracket \supset X) \supset X)$. يعامل هذا الاقتران كاستمرارية تأخذ برهاناً لكل من المكونين لإنتاج نتيجة.
    • الفصل ($\lor$): يُرمز له كـ $\forall X ((\llbracket \phi \rrbracket \supset X) \supset (\llbracket \psi \rrbracket \supset X) \supset X)$. هذا يحاكي تعريف CPS للفصل، حيث يكون البرهان على $\phi \lor \psi$ عبارة عن دالة تأخذ استمراريات لكل من $\phi$ و $\psi$ لإنتاج نتيجة.
    • الخُلو (Falsum - $\bot$): يُرمز له كـ $\forall X (X)$.
  • الدلالات التشغيلية:
    • تُعرف الورقة علاقة حكم تشغيلية $\vdash_O$ (البحث عن البرهان) لهذه البرامج المنطقية.
    • من الضروري أن الكميات الشاملة في الترميز يتم التعامل معها عبر انضباط متغيرات الخصائص الذاتية (eigenvariable discipline) (قيود الحداثة). عند إثبات $\forall X G$، يختار النظام ذرة جديدة $A$ ويثبت $G[A/X]$. هذا يتجنب الحاجة إلى فحص "كل" الذرات، التزاماً بالمبادئ البنائية.

3. المساهمات الرئيسية

1. مبرهنة التناظر المحلي: تؤسس الورقة لتكافؤ دقيق بين الدعم الدلالي والبحث عن البرهان التشغيلي:
   $$\Vdash_B \phi \iff B \vdash_O \llbracket \phi \rrbracket$$
   وهذا يعني أن التحقق مما إذا كانت صيغة مدعومة في قاعدة ما يكافئ تماماً تشغيل إجراء البحث عن البرهان (resolution) ضد تلك القاعدة.
2. التفسير البنائي للكميات: توضح الورقة أن الكميات الشاملة فوق تمديدات القاعدة والذرات في التعريف الدلالي لا تتراوح فوق مجال مكتمل. بدلاً من ذلك، يتم ضبطها بواسطة انضباط متغيرات الخصائص الذاتية في إجراء البحث عن البرهان. وهذا يحل التوتر بين الدلالات والأسس المناهضة للواقعية.
3. رفض "التسطيح" (Flattening): اعتمدت المقاربات المحلية السابقة (مثل Gheorghiu & Pym) على "تسطيح" الصيغ إلى ذرات، مما طمس البنية المنطقية. تحافظ هذه الورقة على بنية $\phi$ من خلال ترميزها مباشرة كهدف، مما يحافظ على تناظر مباشر بين الروابط المنطقية وخطوات البحث عن البرهان.

4. النتائج

• المبرهنة 4.6 (الصحة والاكتمال): لأي قاعدة $B$ وصيغة $\phi$، تكون $\phi$ مدعومة في $B$ إذا وفقط إذا نجح البرنامج المنطقي $B$ في حل الهدف $\llbracket \phi \rrbracket$.
• استراتيجية الإثبات: يسير الإثبات عبر استقراء متزامن على بنية $\phi$.
  • الصحة (Soundness): إذا كان $\Vdash_B \phi$، فإن الدلالات التشغيلية يمكنها اشتقاق $\llbracket \phi \rrbracket$. يعتمد هذا على رتابة علاقة الدعم والقواعد التشغيلية (Augment, Backchain, Generic).
  • الاكتمال (Completeness): إذا كان $B \vdash_O \llbracket \phi \rrbracket$، فإن $\Vdash_B \phi$. يعتمد هذا على ليمّا الاستبدال وحقيقة أن القواعد التشغيلية (تحديداً التعامل مع الذرات الجديدة) تحاكي المتطلبات الدلالية لتمديدات القاعدة.
• دور القواعد عالية المستوى: تعتمد النتيجة بشكل حاسم على وجود القواعد الذرية عالية المستوى (القواعد التي تفرغ الفرضيات). إذا اقتصر النظام على القواعد من المستوى الأول (Horn clauses)، فإن ترميز CPS يفشل، وتنهار الدلالات إلى المنطق الكلاسيكي بدلاً من المنطق الحدسي.

5. الأهمية

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

باختصار، تحول الورقة التعريف المجرد (والذي قد يكون غير بنائي) لدلالات تمديد القاعدة إلى إجراء بحث عن برهان ملموس وقابل للتنفيذ، مثبتة أن "معنى" الصيغة في قاعدة ما هو بالضبط قابليتها للحوسبة كهدف برمجة منطقية.