ملخص تقني: دلالات المذهب المنطقي للمنطق الرتبي الأول الموجه

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

تتناول الورقة التحدي المتمثل في صياغة المساواة الموجهة ضمن إطار منطقي. بينما نجحت منظور "لاوفير" (Lawvere) الفئوي في توصيف المساواة الكلاسيكية كملحق أيسر لعملية التقلص (contraction)، فإن هذا النهج يعتمد على التماثل. أما في نظرية النوع الموجهة، حيث تُفسر الأنواع كفئات (أو رتب مسبقة) بدلاً من فئات غروپية (أو مجموعات)، تصبح المساواة علاقة غير متماثلة (مثل إعادة الكتابة $a \to b$ أو ترتيب $a \le b$).

يكمن الصعوبة الجوهرية في التعامل مع التباين (القطبية/variance). في سياق موجه، قد يظهر المتغير في موضع "سالب" (متضاد التباين، مثل مصدر المورفيزم) أو موضع "موجب" (متوافق التباين، مثل الهدف). تفشل قواعد المساواة المنطقية القياسية (الانعكاسية وقاعدة J/الاستبعاد) في هذا السياق لأنها تفترض ضمناً التماثل أو تسمح للمتغيرات بالظهور في كلتا القطبيتين في آن واحد بطرق قد تؤدي إلى اشتقاق التماثل ($a \le b \vdash b \le a$)، وهو أمر غير صالح في المنطق الموجه. غالباً ما تعاني المحاولات السابقة لنظرية النوع الموجهة من صعوبات في التعامل مع قيود القطبية هذه، لا سيما في سياق المنطق غير المعتد بالبرهان (حيث المساوالة هي قضية وليست نوعاً ذا سكان متعددين).

2. المنهجية

يطور المؤلفون منطقاً رتبياً أولياً موجهاً (dFOL) ودلالاته المذهبية عبر تعميم إطار "لاوفير" للمذهبيات (hyperdoctrines).

بناء الجملة: السياقات المستقطبة

يقدم بناء الجملة سياقاً مستقطباً $[\Theta \mid \Delta \mid \Gamma]$، يقسم المتغيرات إلى ثلاث مجموعات بناءً على تباينها:

• $\Theta$ (السالب): المتغيرات التي تظهر فقط في المواضع متضادة التباين.
• $\Gamma$ (الموجب): المتغيرات التي تظهر فقط في المواضع متوافقة التباين.
• $\Delta$ (الديناتورال/الطبيعي المزدوج): المتغيرات التي تظهر في كلا الموضعين (أو يُسمح بمعاملتها كأمثال).

الميزات التركيبية الرئيسية تشمل:

• المساواة الموجهة ($\le_A$): علاقة أولية $s \le_A t$ حيث يكون $s$ من النوع في السياق السالب و $t$ في السياق الموجب.
• الاستلزام المستقطب: الاستلزام $\psi \Rightarrow \phi$ يقلب قطبية السياق لـ $\psi$ (بنقلها من يسار إلى يمين علامة الالتواء/turnstile)، مما يعكس تضاد التباين للحجة الأولى.
• المسورات المستقطبة: المسورات ($\forall^p, \exists^p$) مفهرسة بالقطبية $p \in \{-, \Delta, +\}$ لتتبع تباين المتغير المرتبط.
• قواعد التعويض: تتعامل آلية تعويض متخصصة (التعريف 2.7) مع إعادة فهرسة الحدود عبر السياقات المستقطبة، مما يضمن تعويض المتغيرات الديناتورال بشكل متسق.

الدلالات: المذهبات الموجهة

يتم التقاط الدلالات عبر المذهبات الموجهة، وهي تعميم لمذهبات "لاوفير".

• الفئة الأساسية: بدلاً من الفئة القياسية للأنواع، الأساس هو فئة استقطاب $ndp(\mathcal{C})$، كائناتها هي ثلاثيات $(\Theta, \Delta, \Gamma)$ ومورفيزماتها تحترم بنية التباين.
• البنية الليفية (Fibered Structure): دالة $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ تربط السياقات المستقطبة بمجموعات جزئية من الصيغ.
• الشروط الرئيسية:
  • عدم تباين الديناتورال (ndv): شرط يضمن أن المتغيرات الديناتورال في المحمولات تنشأ فقط من دمج المتغيرات الموجبة والسالبة، مما يمنع ظهور أنواع ثالثة من التباين.
  • الملحقات النسبية: يتم توصيف المساواة الموجهة ليس كملحق أيسر قياسي، بل كـ ملحق أيسر نسبي لعملية تشبه التقلص تعمل على دمج متغيرين من قطبية متضادة في متغير ديناتورال واحد. هذا يلتقط القيد التركيبي الذي يمنع اشتقاق التماثل.
  • الاستلزام المستقطب: يُوصف كمعتضد نسبي (relative coadjoint).

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

1. بناء جملة dFOL: نظام استنباط طبيعي دقيق للمنطق الرتبي الأول مع المساواة الموجهة، يتميز بنظام صارم للقطبيات مستوحى من الديناتورالية. هذا النظام يمنع صراحةً اشتقاق التماثل للمساواة الموجهة مع الحفاظ على الروابط المنطقية القياسية.
2. توصيف المساواة الموجهة: تعمم الورقة مفهوم "المساواة كملحق أيسر" لـ "لاوفير" إلى المساواة الموجهة كملحق أيسر نسبي. يوفر هذا خاصية كونية فئوية دقيقة للمساواة الموجهة تأخذ في الاعتبار عدم تماثل العلاقة.
3. المذهبات الموجهة: تقديم المذهبات الموجهة كإطار دلالي. يثبت المؤلفون أن بناء جملة dFOL صحي وكامل بالنسبة لهذه الدلالات.
4. اكتمال الرتب المسبقة: تم إثبات نتيجة اكتمال محددة للـ جزئية الكلاسيكية من dFOL بالنسبة للنموذج القياسي لـ الرتب المسبقة ($\mathbf{Preord}$). وهذا يثبت أن أي استلزام صحيح في جميع نماذج الرتب المسبقة هو قابل للاشتقاق في بناء الجملة.
5. التعامل مع القطبية: توضح الورقة كيفية إدارة التباين في إطار غير معتد بالبرهان، بتمييزه عن النظريات النوعية الموجهة المعتدة بالبرهان (مثل تلك الموجودة في $\mathbf{Cat}$) عبر استخدام الألياف الرتيبة (posetal fibrations) والألياف ذات القيم الرتيبة.

4. النتائج

• الصحة والاكتمال: يثبت المؤلفون وجود ملحق ثنائي بين فئة النظريات ($\mathbf{Theory}$) وفئة المذهبات الموجهة ($\mathbf{DDoctrine}$). وهذا يعني أن dFOL هي اللغة الداخلية للمذهبات الموجهة.
• الاكتمال للرتب المسبقة: باستخدام بناء من نمط "هينكن" (Henkin) مكيف للسياقات المستقطبة، تثبت الورقة أن الجزء الكلاسيكي من dFOL كامل بالنسبة لنموذج الرتب المسبقة ($\mathbf{Preord}$). يبني هذا البناء مجال النموذج كمجموعة الحدود المغلقة مرتبة بواسطة اشتقاق المساواة الموجهة ($\le_A$).
• القواعد المشتقة: يدعم النظام القواعد المشتقة للتعدي، والانعكاس، وتطابق (congruence) المساواة الموجهة، بالإضافة إلى قواعد التفاعل بين المسورات المستقطبة والاستلزام.
• الأمثلة المضادة: توضح الورقة أن التماثل ($a \le b \vdash b \le a$) غير قابل للاشتقاق، وأن نموذج الرتب المسبقة يعمل كنموذج مضاد لمثل هذه الاشتقاقات.

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

تدعي الورقة أنها تطور عمل "لاوفير" حول دور التباين ودوال الـ hom. وتحديداً:

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

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