ملخص تقني: الاستيفاء عبر التقسيم المعمم

بيان المشكلة

تتناول الورقة البحثية الإثبات البرهاني لـ مبرهنة ليندون للاستيفاء (Lyndon interpolation theorem). وبينما تم إثبات الاستيفاء في مختلف المنطقات (الكلاسيكي، الحدسي، الجهاتي، الخطي) باستخدام طرق نموذجية، أو آلية، أو نحوية، فإن النهج البرهاني الأكثر شيوعاً يعتمد على طريقة ماهارا (Maehra's method). تقوم هذه الطريقة باستخراج "المستوفي" (interpolant) جراحياً من برهان تسلسل (sequent proof) خالٍ من القطع (cut-free). ومع ذلك، فإن نهج ماهارا والمتغيرات الحديثة منه غالباً ما تفتقر إلى الوحدوية (modularity)؛ حيث إن التغييرات الطفيفة في نظام البرهان (مثل إضافة قواعد جديدة) تتطلب غالباً إعادة إجراء إثبات الاستيفاء بأكتها من البداية. علاوة على ذلك، يخلط نظام التسلسل التقليدي بين القواعد المنطقية "الجوهرية" والقواعد الهيكلية (مثل التضعيف والتقلص)، مما يجعل من الصائع فصل الجوهر المنطقي للاستنتاج عن جوانب إدارة الموارد الخاصة به.

يقترح المؤلف طريقة جديدة تتجنب نظام التسلسل تماماً، مستخدمةً تقنيات الاستدلال العميق (deep inference). والهدف هو صياغة الاستيفاء ليس مجرد وجود صيغة، بل كتحلل بنيوي للاستنتاج، وبالتالي تحقيق تقنية برهانية أكثر وحدوية وعمومية.

المنهجية

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

1. لمة التقسيم المعمم (Generalized Splitting Lemma):
   تنص لمة التقسيم القياسية في الاستدلال العميق على أنه إذا كانت الصيغة $(A \otimes B) \parr K$ قابلة للإثبات، فإنه يمكن تقسيم السياق $K$ إلى $K_A$ و $K_B$ بحيث تكون $A \parr K_A$ و $B \parr K_B$ قابلتين للإثبات. يعمم المؤلف هذا على الاستدلالات ذات مقدمة تعسفية $J$ (بدلاً من مجرد الوحدة $1$). وتحديداً، إذا كان$J \vdash (A \otimes B) \parr K$، فيمكن تفكيك الاستدلال إلى "جزء علوي" (يستنتج سياقاً مقسوماً من$J$) و"جزء سفلي" (يستنتج$K$من السياق المقسوم)، مع عزل الاستدلالات الفرعية لـ$A$و$B$في آن واحد. ومن الأهمية بمكان أن هذا التعميم يتطلب قواعد محددة (يُرمز لها بـ$p'{\downarrow}, d'{\downarrow}, d'_{0\downarrow}$) ليست ضرورية تماماً للاكتمال ولكنها أساسية لعملية التفكيك.

2. الفصل بين الجوهر وغير الجوهر (Core/Non-Core Separation):
   يتم تفكيك أنظمة البرهان إلى جزء جوهري (يحتوي على القواعد المنطقية وقواعد هيكلية محددة مثل $p'_{\downarrow}$) وجزء غير جوهري (يحتوي على القواعد الهيكلية القياسية مثل التضعيف، والتقلص، والترقية). توضح لمة رئيسية أن أي استدلال في النظام الكامل يمكن تحويله إلى شكل يتم فيه تطبيق الجزء الجوهري أولاً، يليه الجزء غير الجوهري، مع الحفاظ على البنية الضربِيّة للنتيجة. يسمح هذا الفصل لجعل إثبات الاستيفاء وحدوياً: حيث يتولى الجزء الجوهري عملية التقسيم المنطقي، بينما يتولى الجزء غير الجوهري إدارة الموارد.

3. لمة القلب (Flipping Lemma):
   بناءً على التقسيم المعمم، يقدم المؤلف آلية "قلب". تسمح هذه اللمة بتحويل استدلال يكون فيه "الجزء العلوي" (المشابه لإدخال القطع) فوق "جزء سفلي" (المشابه لإزالة القطع) إلى استدلال جديد يتم فيه عكس الأدوار أو إعادة الهيكلة. وتحديداً، يمكن تحويل استدلال من $H$ إلى $F \parr K$ عبر جزء علوي وجزء سفلي، إلى استدلال من $F^\perp \otimes H$ إلى $K$ عبر جزء علوي وجزء سفلي مقلوبين، مما يؤدي إلى إدخال صيغة وسيطة $I$.

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

1. منهج برهاني جديد للاستيفاء:
   تقدم الورقة إثباتاً لمبرهنة ليندون للاستيفاء لا يعتمد على نظام التسلسل. بدلاً من ذلك، تستخدم لمة التقسيم المعمم ولمة القلب ضمن أنظمة الاستدلال العميق. ينظر هذا النهج إلى الاستيفاء كعملية تفكيك لاستدلال إلى جزء علوي وجزء سفلي يفصل بينهما المستوفي $I$.

2. النظرية 1 (نظرية التفكيك):
   تنص النتيجة المركزية على أن كل استدلال $A \vdash_X B$ يمكن تفكيكه إلى:
   $$A \xrightarrow{\delta_1} I \xrightarrow{\delta_2} B$$
   حيث يستخدم $\delta_1$ فقط القواعد من الجزء العلوي ($X^\uparrow$) ويستخدم $\delta_2$ فقط القواعد من الجزء السفلي ($X^\downarrow$). تعمل الصيغة $I$ كمستوفي ليندون. تُقدم هذه النظرية كتقوية لنظرية الاستيفاء القياسية (بتوفير براهين صريحة لـ $A \vdash I$ و $I \vdash B$) وكتعميم لنظرية إزالة القطع.

3. أنظمة برهانية مبتكرة للمنطقات الجهاتية:
   يقدم المؤلف أنظمة برهان استدلال عميق خالية من القطع للمنطقات الجهاتية K, KT, K4, S4. فقد اعتُبرت أنظمة الاستدلال العميق الموجودة للمنطق الجهاتي غير كافية للمنهج المقترح (تحديداً لافتقارها إلى الفصل بين الجوهر وغير الجوهر أو خصائص إزالة القطع). تسمح هذه الأنظمة الجديدة بتوسيع نتائج الاستيفاء من المنطق الخطي والكلاسيكي إلى هذه المنطقات الجهاتية.

4. وحدوية البرهان:
   تؤسس المنهجية لبنية وحدوية لبراهين الاستيفاء. نظرًا لأن الجزء الجوهري يحقق لمة التقسيم المعمم بشكل مستقل عن الجزء غير الجوهري، فإن التغييرات الطفيفة في نظام البرهان (مثل إضافة جهات جديدة أو قواعد هيكلية) لا تتطلب إعادة اشتقاق كاملة لمبرهنة الاستيفاء، طالما تم الحفاظ على الفصل بين الجوهر وغير الجوهر.

النتائج

تنجح الورقة في إثبات مرونة هذا النهج من خلال تطبيقه على:

• المنطق الخطي: إثبات الاستيفاء للأنظمة التي تشمل الأجزاء الضربِيّة، والجمعِيّة، والأسّيّة (MELL).
• المنطق الكلاسيكي: إظهار أن نتائج المنطق الخطي تستلزم نتائج المنطق الكلاسيكي عبر ترجمة، وتقديم برهان مباشر للنظام SKS.
• المنطقات الجهاتية: إثبات الاستيفاء لـ K, KT, K4, S4 باستخدام أنظمة البرهان المصممة حديثاً.

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

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

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

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

أخيراً، تضع هذه الورقة عملها كخطوة نحو فهم الاستيفاء في المنطقات التي لا يوجد لها نظام تسلسل، مما يشير إلى أن الفصل بين الجوهر وغير الجوهر قد يكون معياراً عاماً لوجود الاستيفاء في الأنظمة المنطقية الأخرى. ويشير المؤلف بتواضع إلى أنه رغم قوة المنهج، إلا أنه يعتمد حالياً على خيارات تصميم محددة في قواعد الاستدلال (مثل تضمين $p'_{\downarrow}$) لتحقيق التفكيك اللازم، وأن هناك حاة لمزيد من العمل لتوسيع هذه النتائج إلى المنطق من الدرجة الأولى والمنطقات الجهاتية الأخرى.