الاستنتاج الطبيعي وحساب التتالي

الاستنتاج الطبيعي وحساب التتالي هما نظامان رسميان على غرار غنتسن (Gentzen-style) يمثلان البراهين من خلال قواعد الإدخال والإزالة للروابط المنطقية، ويشكلان الآلية الأساسية لنظرية البرهان الهيكلي.

Definition

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

Scope

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

Core questions

• كيف تمنح قواعد الإدخال والإزالة معنى للروابط المنطقية؟
• ما هو التتالي (sequent) وكيف تختلف قواعده عن قواعد الاستنتاج الطبيعي؟
• كيف يبسط التطبيع براهين الاستنتاج الطبيعي؟
• كيف ترتبط النسخ الكلاسيكية والحدسية لهذه الحسابات؟

Key theories

قواعد الإدخال والإزالة

تخضع كل رابطة لقواعد تُدخلها وقواعد تستغلها، وتناغمها، أي أن الإزالة تستعيد بالضبط ما أدخله الإدخال، يعبر عن معنى الرابطة.

نظرية التطبيع

أظهر براويتز (Prawitz) أنه يمكن اختزال براهين الاستنتاج الطبيعي إلى شكل طبيعي خالٍ من الالتفافات حيث يتم إلغاء الإدخال فورًا بواسطة الإزالة، وهو نظير إزالة القطع (cut-elimination) في الاستنتاج الطبيعي.

مراسلات الحسابين

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

Clinical relevance

تُعد هذه الحسابات الأشكال القياسية لدراسة البراهين هيكليًا: يكمن الاستنتاج الطبيعي وراء نظرية الأنواع ومساعدي البرهان من خلال مراسلات البراهين كبرامج، بينما يُعد حساب التتالي، بخصائص الصيغة الفرعية بعد إزالة القطع (cut-elimination)، أساس البحث التلقائي عن البرهان والجداول التحليلية (analytic tableaux).

History

قدم غنتسن (Gentzen) كلاً من الاستنتاج الطبيعي وحساب التتالي في عامي 1934 و 1935، حيث ابتكر حساب التتالي للحصول على نظرية إزالة القطع (cut-elimination theorem) بعد أن وجد أن الاستنتاج الطبيعي أصعب في التحليل. أحيا براويتز (Prawitz) الاستنتاج الطبيعي في عام 1965 بدراسة تطبيع شاملة، وأصبحت الأنظمة مركزية لتطورات البراهين كبرامج اللاحقة.

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

ما الفرق بين الاستنتاج الطبيعي وحساب التتالي؟

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

لماذا التطبيع مهم؟

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