2025-11-16T01:34:12.228023

Provability Models

Mojtahedi, Miranda
In this paper, we study a new Kripke-style semantics for classical modal logic, named as provability models. We study provability models for the propositional modal logics K, K4, S4 GL, GLP and the interpretability logic ILM. Provability models combine features of Kripke models with the assignment of logics to individual worlds. Originally introduced in [Mojtahedi, 2022], these models allowed the first author to establish arithmetical completeness for intuitionistic provability logic. Interestingly, we show that the ILM is complete for the same provability models of GL. We improve provability models to predicative and decidable provability models in the case of GL and ILM. Furthermore, we prove a soundness and completeness of GLP for provability models.
academic

نماذج الإثباتية

المعلومات الأساسية

  • معرّف الورقة: 2510.06696
  • العنوان: نماذج الإثباتية
  • المؤلفون: موجتبى موجتاهدي (جامعة غنت)، بوريا سييرا ميراندا (جامعة برن)
  • التصنيف: math.LO (المنطق الرياضي)
  • تاريخ النشر: 15 أكتوبر 2025
  • رابط الورقة: https://arxiv.org/abs/2510.06696

الملخص

تدرس هذه الورقة نوعاً جديداً من دلالات كريبكي الشبيهة—نماذج الإثباتية (provability models)—المستخدمة في المنطق المشروط الكلاسيكي. يغطي البحث نماذج الإثباتية للمنطق المشروط الكلاسيكي K و K4 و S4 و GL و GLP وكذلك منطق القابلية للتفسير ILM. تجمع النماذج الإثباتية بين خصائص نماذج كريبكي والطريقة المتمثلة في إسناد منطق لكل عالم على حدة. تم تقديم هذا النموذج في الأصل من قبل موجتاهدي في عام 2022، لإثبات الاكتمال الحسابي لمنطق الإثباتية الحدسي. ومن المثير للاهتمام أن الورقة تثبت أن ILM مكتمل بالنسبة لنماذج الإثباتية ذات الصلة بـ GL. في حالة GL و ILM، تحسّن الورقة النماذج الإثباتية إلى نماذج إثباتية قابلة للتنبؤ والفصل، وتثبت سلامة واكتمال GLP بالنسبة للنماذج الإثباتية.

خلفية البحث والدافع

المشكلة الأساسية

في البحث التقليدي عن منطق الإثباتية، يتم عادة تفسير العامل المشروط كمسند إثباتية في نظام حسابي من الدرجة الأولى أو نظرية مجموعات معينة. ومع ذلك، يمكن أيضاً تفسير □A على أنه L ⊢ A (لنظرية قضايا معينة L). على الرغم من أنه يمكن إثبات أن GL سليم بالنسبة للتفسيرات L لأي منطق L يحتوي على GL، إلا أنه لا يوجد تفسير L واحد يعطي اكتمالاً لـ GL.

أهمية المشكلة

يتناقض هذا الفشل مع التفسيرات المتعلقة بـ PA، وينبع بشكل أساسي من عدم قدرة المنطق L على محاكاة نماذج كريبكي، بينما يمكن لحسابات بيانو أن تستفيد من قدرتها على محاكاة نماذج كريبكي (كما أظهر سولوفاي). لذلك، لا يمكن توقع أن يكون GL منطق إثباتية لمنطق قضايا واحد.

قيود الطرق الموجودة

  1. قيود نماذج كريبكي المعيارية: لا يمكنها التعامل مباشرة مع التفسيرات الحسابية لمنطق الإثباتية
  2. عدم اكتمال تفسيرات الإثباتية القضائية: لا يمكن لمنطق قضايا واحد توفير اكتمال GL
  3. خصائص الإطار المعقدة: مثل خصائص الإطار المعقدة في دلالات Iemhoff التي تجعل إثبات نظريات الاكتمال الحسابي صعباً

دافع البحث

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

المساهمات الأساسية

  1. اقتراح إطار النماذج الإثباتية: تقديم دلالات جديدة بأسلوب كريبكي للمنطق المشروط الكلاسيكي
  2. إثبات اكتمال عدة منطق مشروط: إثبات السلامة والاكتمال لـ K و K4 و S4 و GL بالنسبة للنماذج الإثباتية
  3. بناء نماذج إثباتية مستقلة: خاصة بالنسبة لـ GL و ILM، عرض كيفية بناء نماذج إثباتية مستقلة عن نماذج كريبكي المعيارية
  4. تحقيق القابلية للفصل: في حالة GL و ILM، بناء نماذج إثباتية قابلة للفصل
  5. التوسع إلى المنطق متعدد المشروط: إثبات السلامة والاكتمال لـ GLP (منطق الإثباتية متعدد المشروط) بالنسبة للنماذج الإثباتية
  6. إثبات اكتمال ILM: إثبات أن منطق القابلية للتفسير ILM مكتمل بالنسبة للنماذج الإثباتية ذات الصلة بـ GL

شرح الطريقة

تعريف المهمة

دراسة النماذج الإثباتية كدلالات للمنطق المشروط، حيث:

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

معمارية النموذج

تعريف النموذج الإثباتي المسبق

النموذج الإثباتي المسبق P = (W, <, {Lw}w∈W, V) يحتوي على:

  • W: مجموعة عوالم غير فارغة
  • <: علاقة ثنائية على W
  • Lw: منطق لكل عالم w يمكن الوصول إليه بـ <
  • V: علاقة الإسناد للقضايا الذرية

تعريف الصحة

بالنسبة للصيغة A، يتم تعريف P, w |= A بشكل استقرائي:

  • متبادل مع الروابط البوليانية
  • P, w |= □A إذا وفقط إذا ∀u ⪯ w (⊢u A)

شروط النموذج الإثباتي

يصبح النموذج الإثباتي المسبق نموذجاً إثباتياً عند تحقق:

  • الاكتمال المشروط: لكل صيغة مشروط نقي A، إذا كان P, w |=+ A فإن ⊢w A

نقاط الابتكار التقني

1. تنطيق شروط الإطار

يمكن للنماذج الإثباتية امتصاص شروط الإطار كقواعد استدلال للمنطق المسند لعوالم فردية:

  • يمكن استبدال التعدية بقاعدة الضرورة
  • يمكن استبدال عدم الأساس العكسي بقاعدة Löb

2. الطريقة البنائية

بالنسبة لـ GL و ILM، توفر طرقاً بنائية لبناء النماذج الإثباتية:

النظرية 4.4: لكل نموذج إثباتي مسبق لشجرة عكسية غير أساسية P، يوجد نموذج إثباتي P̄ بقاعدة الضرورة، بحيث:

  • P̄ له قاعدة الضرورة
  • P ⊆ P̄
  • P̄ هو أصغر نموذج إثباتي يحتوي على P

3. ضمان القابلية للفصل

إذا كان P ثنائي محدود، فإن P̄ قابل للفصل، حيث يعني ثنائي محدود أن W وكل Axiom(Lw) لـ w∈W محدود.

إعداد التجربة

إطار التحقق النظري

تجري الورقة بشكل أساسي إثباتات نظرية، ويتضمن إطار التحقق:

1. إثبات السلامة

بالنسبة لمختلف المنطق المشروط، إثبات أنه إذا كان المنطق ⊢ A، فإن P |= A لجميع النماذج الإثباتية المقابلة P.

2. إثبات الاكتمال

إثبات أنه إذا كان P |= A لجميع النماذج الإثباتية المقابلة P، فإن المنطق ⊢ A.

3. الاكتمال القوي

خاصة بالنسبة لـ GL، إثبات الاكتمال القوي: Γ |=P A يستلزم Γ ⊢GL A.

التحقق من الطرق البنائية

من خلال البناء الملموس، تم التحقق من:

  • وجود نماذج إثباتية محدودة
  • تحقيق القابلية للفصل
  • الاستقلالية (عدم الاعتماد على نماذج كريبكي المعيارية)

نتائج التجربة

النتائج الرئيسية

1. اكتمال المنطق المشروط الأساسي

  • K: سليم ومكتمل بالنسبة للنماذج الإثباتية (النظرية 3.6، 3.7)
  • K4: سليم ومكتمل بالنسبة للنماذج الإثباتية بقاعدة الضرورة أو التعدية (النظرية 3.8، 3.9)
  • S4: سليم ومكتمل بالنسبة للنماذج الإثباتية الانعكاسية والمتعدية بقاعدة الضرورة والاكتمال المحلي (النظرية 3.11، 3.12)

2. نتائج منطق الإثباتية GL

  • السلامة: GL سليم بالنسبة للنماذج الإثباتية غير الأساسية العكسية بقاعدة الضرورة وقاعدة Löb (النظرية 3.14)
  • الاكتمال: GL مكتمل بالنسبة للنماذج الإثباتية المحدودة المتعدية غير الانعكاسية (النظرية 3.17)
  • الاكتمال القوي: GL قوي مكتمل بالنسبة للنماذج الإثباتية بقاعدة الضرورة وقاعدة Löb (النظرية 3.18)
  • اكتمال المحدودية: GL مكتمل بالنسبة للنماذج الإثباتية المحدودة (النظرية 4.6)

3. نتائج منطق القابلية للتفسير ILM

  • السلامة: ILM سليم بالنسبة للنماذج الإثباتية غير الأساسية العكسية بقاعدة الضرورة (النظرية 5.6)
  • الاكتمال: ILM مكتمل بالنسبة للنماذج الإثباتية لشجرة محدودة غير أساسية عكسية بقاعدة الضرورة (النظرية 5.10)
  • اكتمال المحدودية: ILM مكتمل بالنسبة للنماذج الإثباتية المحدودة (النظرية 5.13)

4. نتائج منطق الإثباتية متعدد المشروط GLP

  • السلامة والاكتمال: GLP سليم وقوي مكتمل بالنسبة لنماذج GLP الإثباتية متعددة المشروط (النظرية 6.2، 6.3)

النتائج البنائية

تم بناء نماذج إثباتية مستقلة بنجاح عن نماذج كريبكي المعيارية، خاصة:

  • بالنسبة لأي إطار شجرة عكسية غير أساسية وأي إسناد لمجموعة صيغ للعقد، يمكن بناء أصغر نموذج إثباتي
  • في الحالة ثنائية المحدودة، النموذج المبني قابل للفصل

الأعمال ذات الصلة

البحث التقليدي في منطق الإثباتية

  • Solovay (1976): إثبات منطق الإثباتية لـ PA
  • Boolos (1995)، Smoryński (1985): كتب مدرسية كلاسيكية في منطق الإثباتية
  • Artemov و Beklemishev (2004): مسح شامل

طرق الدلالات

  • دلالات كريبكي المعيارية: المستخدمة في مختلف المنطق المشروط
  • نماذج Veltman: المستخدمة في منطق القابلية للتفسير ILM
  • الدلالات الطوبولوجية: توفير الاكتمال لـ GLP

منطق الإثباتية الحدسي

  • Iemhoff (2001-2003): تقديم دلالات Iemhoff
  • Mojtahedi (2022): استخدام النماذج الإثباتية لأول مرة لإثبات الاكتمال الحسابي لمنطق الإثباتية الحدسي

الخلاصة والمناقشة

الاستنتاجات الرئيسية

  1. إطار موحد: توفر النماذج الإثباتية إطار دلالات موحد لعدة منطق مشروط
  2. البناء: خاصة بالنسبة لـ GL و ILM، يمكن بناء نماذج إثباتية مستقلة بشكل بنائي
  3. القابلية للفصل: في الظروف المناسبة، النماذج الإثباتية قابلة للفصل
  4. المرونة: يمكن استبدال شروط الإطار بخصائص منطقية، مما يوفر مرونة أكبر

القيود

  1. قيود GLP: بالنسبة لـ GLP، لم يتم العثور بعد على فئة نماذج إثباتية قابلة للفصل
  2. تعقيد البناء: قد يكون تعقيد بعض البناءات (مثل النموذج الكنسي لـ GLP) غير بنائي
  3. نطاق التطبيق: ينطبق بشكل أساسي على المنطق ذي الخصائص الإثباتية

الاتجاهات المستقبلية

تطرح الورقة بوضوح عدة مسائل مفتوحة:

  1. توسيع منطق الإثبات: تعريف نماذج بأسلوب الإثباتية لمنطق الإثبات LP و JGL
  2. المنطق المشروط الحدسي: تعريف نماذج إثباتية للمنطق المشروط الحدسي بعاملين مشروطين □ و◇
  3. نماذج GLP القابلة للفصل: البحث عن فئة نماذج إثباتية قابلة للفصل لـ GLP
  4. تبسيط الاكتمال الحسابي: استكشاف ما إذا كان يمكن تبسيط إثبات الاكتمال الحسابي لـ ILM من خلال النماذج الإثباتية

التقييم المتعمق

المميزات

  1. الابتكار النظري: اقتراح إطار دلالات جديد تماماً يوحد معالجة عدة منطق مشروط
  2. العمق التقني: توفير إثباتات رياضية مفصلة وطرق بناء
  3. القيمة العملية: التحسينات خاصة في جانب القابلية للفصل ذات أهمية كبيرة
  4. النظامية: معالجة منهجية لحالات متنوعة من المنطق المشروط الأساسي إلى منطق الإثباتية المعقد

أوجه القصور

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

التأثير

  1. المساهمة النظرية: توفير اتجاه بحثي جديد لدلالات المنطق المشروط
  2. القيمة المنهجية: طريقة تنطيق شروط الإطار ذات أهمية عامة
  3. البحث اللاحق: توفير أدوات جديدة لأبحاث المنطق الحدسي ومنطق الإثبات وغيرها

السيناريوهات المناسبة

  1. بحث منطق الإثباتية: مناسب بشكل خاص للأبحاث التي تتطلب الاكتمال الحسابي
  2. دلالات المنطق المشروط: توفير طرق دلالات جديدة للمنطق المشروط المعقد
  3. المنطق الحسابي: قيمة محتملة في التطبيقات التي تتطلب القابلية للفصل

المراجع

تستشهد الورقة بمراجع غنية ذات صلة، بما في ذلك:

  • الأدبيات الكلاسيكية في منطق الإثباتية (Boolos, Smoryński, Solovay وغيرهم)
  • الأعمال المهمة في دلالات المنطق المشروط (Blackburn وغيرهم)
  • البحث الرئيسي في منطق القابلية للتفسير (Berarducci, Shavrukov وغيرهم)
  • الأعمال ذات الصلة في منطق الإثباتية الحدسي (Iemhoff وغيرهم)

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