Glivenko's theorems from an ecumenical perspective

ملخص تقني: نظريات جليفنكو من منظور توفيقي

بيان المشكلة
تتناول الورقة العلاقة التأسيسية بين المنطق الكلاسيكي (CL) والمنطق الحدسي (IL)، وتحديداً إعادة فحص نظريات جليفنكو. تُثبت هذه النظريات أنه إذا كانت الصيغة قابلة للإثبات كلاسيكياً، فإن نفيها المزدوج يكون قابلاً للإثبات حدسياً، وإذا كانت الصيغة المنفية قابلة للإثبات كلاسيكياً، فهي أيضاً قابلة للإثبات حدسياً. وبينما تُعد هذه النتائج مفهومة جيداً في سياق الأنظمة المنطقية المنفصلة، تبحث هذه الورقة في كيفية تجلي هذه العلاقات داخل الأنظمة التوفيقية (Ecumenical Systems). الأنظمة التوفيقية هي أطر موحدة حيث يتعايش المنطق الكلاسيكي والمنطق الحدسي بسلام دون أن ينهار أحدهما في الآخر، وذلك غالباً عن طريق تمييز الروابط (مثل: التشتت الكلاسيكي مقابل التشتت الحدسي) أو عن طريق وسم الصيغ للإشارة إلى طبيعتها المنطقية. المشكلة المركزية هي تحديد كيفية ترجمة نتائج نوع جليفنكو عندما يتم دمج الاستدلال الكلاسيكي والحدسي في نظام استدلالي واحد، وتحليل الاختلافات بين نهجين رئيسيين للتوفيق: النهج "الاستدلالي" (تمييز الروابط) والنهج "العام" (تمييز الصيغ عبر الوسوم).

المنهجية
يستخدم المؤلفون تحليلاً نظرياً للاستدلال باستخدام أنظمة الاستنباط الطبيعي. وهم يفحصون ثلاثة أطر توفيقية محددة:

1. نظام NE (نظام برافيتز): نهج استدلالي حيث يتشارك المناطقة الكلاسيكيون والحدسيون روابط محايدة (الوصل، المسور العام، النفي، الاستحالة)، ولكنهم يمتلكون نسخاً متميزة من الروابط غير المحايدة (الاستلزام، الفصل، المسور الوجودي).
2. نظام ECI (نظام باروسو-ناسيمنتو): نهج عام يستخدم مجموعة واحدة من الروابط، ولكن يتم وسم الصيغ بوسم $c$ (على سبيل المثال $A^c$) للدلالة على السلوك الكلاسيكي. هذا النظام مبني على الاستنباط الطبيعي الحدسي المعزز بقواعد الإدخال ($I_C$) والحذف ($E_C$) للوسم.
3. نظام NEK (نظام مستوحى من كراوس): نسخة متغيرة من نظام برافيتز تتضمن وصلاً كلاسيكياً ($\land_c$) ومسوراً عاماً كلاسيكياً ($\forall_c$)، بناءً على عمل كراوس غير المنشور.

تتضمن المنهجية:

• تعريف نظريات داخلية من نوع جليفنكو داخل هذه الأنظمة (ربط الروابط/الصيغ الكلاسيكية بنظائرها الحدسية).
  ما يلي:
• بناء اشتقاقات لإثبات هذه العلاقات الداخلية.
• تعريف دوال الترجمة ($t_{ECI}$ و $t_{NEK}$) لربط الصيغ بين الأنظمة.
• استقصاء التكافؤ الاستدلالي لهذه الأنظمة، لا سيها في الجزء القضاياوي مقابل الجزء من الدرجة الأولى الذي يتضمن المسور العام.

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

1. نظريات جليفنكو الداخلية في NE:
   يوضح المؤلفون أنه في نظام برافيتز (NE)، حيث توجد روابط متميزة، تتحقق علاقة "نوع جليفنكو" داخلياً. لأي صيغة $C$ يكون الرابط الرئيسي فيها كلاسيكياً، فإن $C \vdash_{NE} \neg\neg C^*$، حيث $C^*$ هي الصيغة التي تم استبدال الرابط الكلاسيكي فيها بنظيره الحدسي. ينطبق هذا على الفصل الكلاسيكي ($\lor_c$)، والاستلزام ($\to_c$)، والمسور الوجودي ($\exists_c$). وتتحقق نتيجة مماثلة للصيغ المنفية: $\neg C \vdash_{NE} \neg C^*$.

2. تجزؤ نتائج جليفنبو في ECI:
   في نظام ECI، تكون العلاقة بين الصيغة الكلاسيكية $A^c$ ونظيرتها الحدسية بديهية من الناحية الهيكلية. إذ تؤدي قواعد النظام مباشرة إلى $A^c \vdash_{ECI} \neg\neg A$. وبناءً على ذلك، فإن ترجمة $t_{ECI}$، التي تربط $A^c$ بـ $\neg\neg A$، تختزل مشكلة التطبيع (Normalization) في ECI إلى المنطق الحدسي. ويُظهر المؤلفون أنه بينما تعمل هذه الترجمة في المنطق القضاياوي، إلا أنها تحجب الموقع المحدد للاستدلال الكلاسيكي في الاشتقاق ما لم يتم إعادة بناء الاشتقاق بعناية لتتبع "الطبيعة الكلاسيكية" للصيغ المستمدة.

3. حالة الوصل الكلاسيكي و NEK:
   تقدم الورقة نظام NEK، الذي يضيف وصلاً كلاسيكياً ($\land_c$) إلى نظام برافيتز. يثبت المؤلفون أن $\land_c$ يحقق نظريات جليفنكو الداخلية ($B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$). كما يبينون أنه في الجزء القضاياوي (أو منطق الدرجة الأولى بدون مسور عام)، يتكافئ NEK و ECI استدلالياً. ويتم إثبات هذا التكافؤ عبر ترجمة $t_{NEK}$ التي تربط الروابط الكلاسيكية في NEK بالصيغ الموسومة في ECI.

4. التباعد مع المسور العام:
   تتمثل النتيجة الحاسمة في فشل التكافؤ الاستدلالي بين NEK و ECI عند إدخال المسور العام.

• في NEK، يتم تعريف المسور العام الكلاسيكي $\forall_c$ عبر قواعد تتناغم مع المنطق الحدسي. ومع ذلك، تفشل نظرية جليفنكو الداخلية بالنسبة لـ $\forall_c$: إذ أن $\vdash_{NEK} \forall_c x A(x)$ لا تستلزم $\vdash_{NEK} \neg\neg \forall_i x A(x)$.
• في ECI، يتصرف المسور العام الموسوم $(\forall x A(x))^c$ بشكل مختلف. فبسبب قواعد النظام، يتحقق $(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$.
  يفسر المؤلفون هذا التباين بأن $\forall_c x A(x)$ في NEK تُفسر على أنها $\neg \exists x \neg A(x)$، بينما في ECI، يُفسر $(\forall x A(x))^c$ فعلياً على أنه $\neg\neg \forall x A(x)$. وهذان التفسيران غير متكافئين حدسياً. وتجادل الورقة بأن "تجزؤ" نتائج جليفنكو في ECI بالنسبة للمسورات العامة ينبع من كون الوسم $c$ يفرض تفسيراً بالنفي المزدوج لا يتوافق مع السلوك الدلالي للمسور العام في النهج الاستدلالي.

الأهمية والادعاءات
تدعي الورقة أن المنظور التوفيقي يقدم فهماً أعمق للتفاعل بين الاستدلال الكلاسيكي والحدسي. ومن خلال المقارنة بين النهجين "الاستدلالي" (NE/NEK) و"العام" (ECI)، يسلط المؤلفون الضوء على فرق مفاهيمي دقيق وجوهري:

• الأنظمة الاستدلالية (Pravitz/Krauss) تغير معنى الروابط مباشرة عبر تقديم قواعد إدخال وحذف متميزة للروابط الكلاسيكية.
• الأنظمة العامة (ECI) تغير مستوى البرهان، حيث تجهز المنطق الحدسي بوسائل برهان كلاسيكية (عبر الوسم $c$) تغير معنى الروابط بشكل غير مباشر.

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