الدلالات القائمة على نظرية البرهان

النظام الذري هو مجموعة محدودة أو غير محدودة من القواعد التي تُطبق على مجموعة من الجمل الذرية (غير المنطقية). ويُقبل عادةً نوعان من القواعد: قواعد بدون مقدمات من الشكل التالي:

${\displaystyle {\frac {}{P}}\qquad {\text{and}}\qquad {\frac {P_{1}\quad \cdots \quad P_{n}}{P}}}$

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

تأخذ العبارات الدلالية التي تحكم الثوابت المنطقية الشكل التالي، حيث${\displaystyle {\mathcal {B}}}$نطاقات على القواعد: ^{[ 4 ] [ 5 ]}

${\displaystyle \Vdash _{\mathcal {B}}P\quad {\text{iff}}\quad \vdash _{\mathcal {B}}P\qquad (P{\text{ atomic}})}$

${\displaystyle \Vdash _{\mathcal {B}}\varphi \wedge \psi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi {\text{ and }}\Vdash _{\mathcal {B}}\psi }$

${\displaystyle \Vdash _{\mathcal {B}}\varphi \to \psi \quad {\text{iff}}\quad \varphi \Vdash _{\mathcal {B}}\psi }$

${\displaystyle \Vdash _{\mathcal {B}}\forall x\,\varphi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi [x\mapsto t]{\text{ for every closed term }}t}$

${\displaystyle \Delta \Vdash _{\mathcal {B}}\varphi \quad {\text{iff}}\quad {\text{لكل }}{\mathcal {C}}\supseteq {\mathcal {B}},\ {\text{إذا كان }}\Vdash _{\mathcal {C}}\psi {\text{لكل }}\psi \in \Delta ,\ {\text{ثم }}\Vdash _{\mathcal {C}}\varphi }$

ثم يتم تحديد النتيجة من خلال التحديد الكمي على أساسات:${\displaystyle \Gamma \Vdash \varphi }$تحسباً لأي طارئ${\displaystyle \Gamma \Vdash _{\mathcal {B}}\varphi }$لكل${\displaystyle {\mathcal {B}}}$في الفئة المختارة. التحديد الكمي على الامتدادات${\displaystyle {\mathcal {C}}\supseteq {\mathcal {B}}}$إن بنود الاستدلال هي نظير هيكلي للرتابة المضمنة في دلالات كريپكي للمنطق الحدسي ، وتضمن الحفاظ على النتيجة عند إضافة قواعد ذرية جديدة.

تستحق عبارات الفصل والوجود والعبث تعليقًا منفصلاً، إذ أن أكثر القراءات الطبيعية لهذه الروابط لا تُميّز المنطق الحدسي. ^{[ 6 ]} القراءة

${\displaystyle \Vdash _{\mathcal {B}}\varphi \vee \psi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi {\text{ or }}\Vdash _{\mathcal {B}}\psi }$

يؤكد هذا صحة بديهية كريزل-بوتنام ، وهي مخطط مقبول ولكنه غير قابل للاستنتاج في حساب القضايا الحدسي؛ وقد حدد ويل ستافورد المنطق الناتج على أنه شكل من أشكال المنطق الاستقصائي. ^{[ 7 ]} وبناءً على ذلك، اقترح ساندكفيست عبارة بديلة مصممة على غرار تعريف الفصل من الدرجة الثانية المألوف من النظام F ومن أطروحة براويتز:

${\displaystyle \Vdash _{\mathcal {B}}\varphi \vee \psi \quad {\text{iff}}\quad {\text{for every }}{\mathcal {C}}\supseteq {\mathcal {B}}{\text{ and every atom }}P,\ {\text{if }}\varphi \Vdash _{\mathcal {C}}P{\text{ and }}\psi \Vdash _{\mathcal {C}}P,\ {\text{then }}\Vdash _{\mathcal {C}}P}$

تُحكم جملة موازية المُكمِّم الوجودي، ويتم التعبير عن ex falso quodlibet من خلال اشتراط أن${\displaystyle \Vdash _{\mathcal {B}}\bot }$تحسباً لأي طارئ${\displaystyle \Vdash _{\mathcal {B}}P}$لكل ذرة${\displaystyle P}$بموجب هذه البنود، يحدد اختيار الأسس المقبولة - سواء كان الأساس يقبل قواعد مع تفريغ الفرضيات، وعلى أي مستوى - المنطق الذي يتم التقاطه بواسطة علاقة الدعم. ^{[ 5 ]}

أظهر ساندكفيست أن منطق القضايا الحدسي سليم وكامل بالنسبة لعلاقة الدعم عندما يسمح الأساس بقواعد مع تفريغ الافتراضات الذرية، وأن المنطق الكلاسيكي المقتصر على الاستلزام والعبثية والمكمّم الكلي يكون سليمًا وكاملاً عندما يقتصر الأساس على قواعد بدون تفريغ. ^{[ 4 ] [ 8 ]}

حُسمت مسألة المنطق من الدرجة الأولى الكاملة - الكلاسيكية والحدسية على حد سواء - على يد ألكسندر ف. جورجيو عام ٢٠٢٥، الذي أرسى دلالات سليمة وكاملة لتوسيع القاعدة لمنطق الدرجة الأولى بنوعيه، وذلك بوسائل أولية وبنائية وأصلية من الناحية البرهانية. ^{[ ٥ ]} وتكتسب هذه النتيجة أهمية بالغة من عدة جوانب. فهي تعالج المنطقين ضمن إطار موحد، لا يختلفان إلا في الأساس المقبول. كما أنها تستغني عن تقنيات الاستقراء الشريطي التي تطلبتها برهنة ساندكفيست الكلاسيكية السابقة. وعلى عكس برهان ديفيد ماكينسون السابق على اكتمال منطق القضايا الكلاسيكي - الذي اختزل المسألة إلى دلالات دالة الصدق من خلال إظهار تطابق بين الأسس والتقييمات الكلاسيكية ^{[ ٩ ]} - فإنها تُثبت الاكتمال دون اللجوء إلى القراءة النموذجية للمنطق الكلاسيكي، وبالتالي تُظهر الموارد الاستدلالية للإطار وفقًا لشروطها الخاصة.

تعتمد البرهنة على تقنية محاكاة ، تعود في الأصل إلى ساندكفيست في حالة الاستدلال الحدسي الافتراضي، وقد وُسِّعت بشكل كبير لتشمل الحالة الكلاسيكية من الدرجة الأولى. بفرض نتيجة مُحتملة، يُنشأ أساسٌ تُحاكي قواعده الذرية خطوات الإدخال والحذف في نظام هيلبرت على الصيغ الفرعية للصيغ المعنية؛ وتتولى أدواتٌ إضافية، بما في ذلك استخدام متغيرات ذاتية مُستمدة من مجموعة ثوابت محفوظة، محاكاة قواعد المُكمِّمات والصيغ المفتوحة. ومن برهانٍ مُفترضٍ على صحة النتيجة، يُستخلص اشتقاقٌ في حساب التفاضل والتكامل البديهي المُناسب.

يُعدّ اختزال الفرق بين المنطق الكلاسيكي والمنطق الحدسي من الدرجة الأولى إلى اختلاف في الأساس المقبول أحد أبرز سمات هذا الإطار. فالعبارات الدلالية للروابط متطابقة في الحالتين؛ أما الطابع المنطقي للنتيجة فيُحدّد بالكامل على المستوى ما قبل المنطقي، من خلال الموارد الاستدلالية للأنظمة الذرية نفسها.

قدّم غيرهارد جنتزن في أطروحته للدكتوراه (1934-1935)، بعنوان " دراسات في الاستدلال المنطقي "، مفهوم الاستدلال الطبيعي وحساب المتتاليات، وأرسى نظرية حذف القطع لهذا الأخير. ^{[ 10 ]} وفي فقرةٍ أثّرت في الفكر اللاحق، أشار جنتزن إلى أن قواعد إدخال الرابط تمثل "بمعنى ما، تعريفات الرموز المعنية"، بينما قواعد الحذف "ليست، في التحليل النهائي، سوى نتائج هذه التعريفات". وتُعدّ أطروحة أن قواعد الإدخال تُحدّد المعنى وأن قواعد الحذف تخضع لها، هي النواة التي نما منها علم الدلالة القائم على نظرية البرهان.

يعود الفضل في أول محاولة لتطوير نظرية دلالية على غرار جينتزن إلى داغ براويتز ، الذي أثبت في كتابه "الاستنتاج الطبيعي: دراسة نظرية البرهان" (1965) نظرية التطبيع : كل اشتقاق في الاستدلال الطبيعي الحدسي يختزل إلى شكل طبيعي لا تُدخل فيه أي صيغة أولًا ثم تُحذف فورًا. ^{[ 11 ]} ومن النتائج المترتبة على ذلك أن كل اشتقاق مغلق يختزل إلى اشتقاق تكون خطوته الأخيرة قاعدة إدخال، وهي نتيجة تقع في صميم تناظر كاري-هوارد ونظرية النوع الحدسية .

في كتابه "أفكار ونتائج في نظرية البرهان" (1971)، اقترح براويتز مفهومًا لصحة الحجج - وهي عبارة عن أشجار من الصيغ تُبنى باستخدام خطوات استدلالية لا يشترط أن تكون قواعد لأي نظام شكلي مُعطى - مُعرَّفًا بالنسبة إلى نظام ثابت من القواعد الذرية وفئة من عمليات الاختزال المسموح بها. ^{[ 12 ]} افترض براويتز أن الاستدلال الطبيعي الحدسي كامل فيما يتعلق بهذا المفهوم: إذ يمكن تكرار كل حجة صحيحة كاشتقاق في النظام. وقد دُحض هذا الافتراض لاحقًا من قِبل بيشا، ودي كامبوس سانز، وشرودر-هايستر، الذين أظهروا أن التعبير الشكلي الأكثر مباشرة لفكرة براويتز يُنتج منطقًا أقوى بكثير من المنطق الحدسي. ^{[ 6 ]} درس ألكسندر ف. جورجيو وديفيد بيم العلاقة بين صحة نظرية البرهان بمفهوم براويتز ودلالات امتداد القاعدة المستخدمة حاليًا بشكل عام، وحددا الشروط التي يتطابق فيها المفهومان. ^{[ 13 ]}

طوّر مايكل دوميت الآثار الفلسفية لبرنامج جنتزن-براويتز على مدى عقود، وبلغت ذروتها في كتابه " الأساس المنطقي للميتافيزيقا" . ^{[ 3 ]} انطلاقًا من اقتراح نويل بيلناب، المستوحى من حالة " الرابط المنطقي "، قدّم دوميت مفهوم الانسجام المنطقي : يكون نظام قواعد الاستدلال متناغمًا عندما يكون من الممكن دائمًا استخلاص براهين تحليلية من أي برهان، كما هو مضمون لحساب التتابع عن طريق حذف القطع، وللاستنتاج الطبيعي عن طريق التطبيع. اللغة التي تفتقر إلى الانسجام تسمح بأشكال استدلال غير متماسكة وتكون عرضة للتناقض. اتخذ دوميت هذا الإطار لدعم مفهوم مناهض للواقعية للمعنى، حيث يُحدد معنى العبارة بشروط قابليتها للتأكيد لا بشروط صحتها، وجادل - بإسهاب، وبشكل مثير للجدل - بأن الموقف الناتج يدعم بشكل طبيعي المبادئ الحدسية بدلًا من المبادئ الكلاسيكية.

صاغ بيتر شرودر-هايستر مصطلح "الدلالات البرهانية النظرية" في محاضراته خلال ثمانينيات القرن العشرين، ونُشر في كتاباته عام ١٩٩١. ^{[ ١٤ ] [ ١٥ ]} وقد أكد شرودر-هايستر أن هذا المشروع لا يعكس العلاقة التقليدية بين الاشتقاق الرسمي والاستلزام الدلالي - إذ تبقى السلامة والكمال من السمات المرغوبة في الأنظمة الرسمية - بل يعيد بناء المفهوم الدلالي للنتيجة من حيث البراهين، حيث لم تعد البراهين تُفهم حصريًا على أنها اشتقاقات رسمية، بل على أنها تُشكل معاني الثوابت المنطقية. كما طور شرودر-هايستر، بالتعاون مع لارس هالناس ، مفهوم " الانعكاس التعريفي" ، وهو تعميم لمبدأ براويتز العكسي ليشمل المسندات المُعرَّفة استقرائيًا، مما يوفر جسرًا بين الدلالات البرهانية النظرية والبرمجة المنطقية . ^{[ ١٦ ]}

لطالما شكلت العلاقة بين دلالات نظرية البرهان والمنطق الكلاسيكي مصدرًا للصعوبات، إذ يُنظر غالبًا إلى فرضية "قواعد الإدخال كتعريفات" على أنها تدعم المبادئ الحدسية. وقد وصف دوميت التوفيق بين الاستدلال الكلاسيكي والدلالات الاستدلالية بأنه من بين أهم المشكلات الأساسية في نظرية المعنى. ^{[ 18 ]} بيّن ساندكفيست أن جزءًا من منطق المسند الكلاسيكي سليم وكامل لدلالات توسيع القاعدة عندما تقتصر القواعد على قواعد بدون تفريغ، ^{[ 8 ]} ثم أظهر ماكينسون لاحقًا وجود تطابق بين القواعد بمفهوم ساندكفيست والتقييمات الكلاسيكية. ^{[ 19 ]} وتُكمل نتيجة جورجيو من الدرجة الأولى هذا المسار بإثبات اكتمال المنطق الكلاسيكي الكامل من الدرجة الأولى بوسائل نظرية البرهان الأصلية. ^{[ 5 ]}

قام تيمو إيكهارت وديفيد بيم بتطوير دلالات توسيع القاعدة للمنطق الموجه ، حيث تلعب القواعد دور العوالم الممكنة وترتبط ببعضها البعض من خلال علاقة إمكانية الوصول الخاضعة لقيود تعكس الطابع الجزئي للقواعد بوصفها أوصافًا لحالات الأمور. ^{[ 20 ]} يوفر هذا الإطار دلالات سليمة وكاملة للمنطق الموجه العادي المحدد بواسطة البديهيات K وT و4 و5؛ ويؤدي تعديل لاحق للشروط المفروضة على علاقة إمكانية الوصول إلى دلالات سليمة وكاملة لـ S5 وتعميماتها متعددة الوسائط.

قام كلٌّ من جورجيو، وتاو غو ، وبيم بتكييف هذا الإطار مع المنطق البنيوي الفرعي ، حيث تُقيَّد قواعد الانكماش والتضعيف البنيوية القياسية. ^{[ 21 ]} وتتمثل الفكرة الأساسية في جعل الأنظمة الذرية حساسة للموارد - مما يسمح بتنفيذ فرضية واحدة فقط - وإثراء علاقة الدعم بمعامل صريح للموارد الذرية. وتكون الدلالات الناتجة سليمة وكاملة للمنطق الخطي الحدسي المضاعف ، ومع إضافة بنود جمعية أخرى، لتوسيعه بروابط جمعية؛ ومع تضمين أولي ثانٍ ومُكوِّن سياق مصاحب، يُنتج هذا البناء دلالات لمنطق التضمينات المجمعة .