إزالة القطع
إزالة القطع هي مبرهنة جينتزن التي تنص على أن قاعدة القطع، التي تضفي الطابع الرسمي على استخدام الليمات (المبرهنات المساعدة)، يمكن إزالتها من أي برهان حساب المتتاليات، تاركةً برهانًا مبنيًا فقط على الصيغ التي تتعلق بها.
Definition
إزالة القطع هي المبرهنة والإجراء البنائي الذي يوضح أن أي اشتقاق لحساب المتتاليات يستخدم قاعدة القطع يمكن تحويله إلى اشتقاق لا يستخدمها، بحيث يكون لكل متتالية قابلة للإثبات برهان تظهر فيه فقط الصيغ الفرعية للمتتالية النهائية.
Scope
يغطي هذا الموضوع قاعدة القطع ودورها في حساب المتتاليات، وإجراء إزالة القطع وإنهاءه، وخاصية الصيغة الفرعية للبراهين الخالية من القطع، والنتائج المترتبة على الاتساق والقابلية للتقرير، والحدود على حجم البرهان التي يمكن أن تترتب على الإزالة.
Core questions
- ماذا تعبر قاعدة القطع ولماذا إزالتها مهمة؟
- كيف ينتهي إجراء إزالة القطع؟
- ما هي خاصية الصيغة الفرعية وماذا تعني للبحث عن البرهان؟
- ما هي التكلفة الحسابية لإزالة القطع؟
Key theories
- مبرهنة جينتزن الرئيسية (Gentzen Hauptsatz)
- تنص مبرهنة جينتزن الرئيسية على أن قاعدة القطع مقبولة في حساب المتتاليات، بحيث يمكن تحويل أي برهان يستخدم القطع إلى برهان خالٍ من القطع لنفس المتتالية النهائية.
- خاصية الصيغة الفرعية
- كل صيغة تظهر في برهان خالٍ من القطع هي صيغة فرعية للمتتالية النهائية، مما يقيد شكل البرهان ويشكل أساس إجراءات القرار وحجج الاتساق.
- الاتساق عبر إزالة القطع
- نظرًا لاستحالة وجود برهان خالٍ من القطع للمتتالية الفارغة، فإن إزالة القطع تؤدي إلى برهان مباشر على أن الحساب، وبالتالي النظرية التي يضفي عليها الطابع الرسمي، متسق.
Clinical relevance
إزالة القطع هي نتيجة أساسية ذات عواقب واسعة: فهي تؤدي إلى براهين الاتساق، وخاصية الصيغة الفرعية الضرورية لإثبات المبرهنات الآلي وطرق الجداول، ومبرهنات الاستيفاء، ومن خلال مراسلات البراهين كبرامج، تطبيع البرامج المكتوبة.
History
أثبت جينتزن إزالة القطع، أو مبرهنته الرئيسية (Hauptsatz)، في عام 1934 للمنطق من الدرجة الأولى، وأصبحت هذه الطريقة حجر الزاوية في نظرية البرهان الهيكلية. قام تايت وجيرارد بتوسيع التقنية لتشمل أنظمة أقوى ومنطق من الدرجات العليا، وأصبحت حدود نمو حجم البرهان تحت إزالة القطع موضوع دراسة بحد ذاتها.
Key figures
- Gerhard Gentzen
- William Tait
- Jean-Yves Girard
- Gaisi Takeuti
Related topics
Seminal works
- takeuti1987
- troelstra2000
- negri2001
Frequently asked questions
- ما هو القطع في البرهان؟
- تسمح قاعدة القطع بإثبات ليمة (مبرهنة مساعدة) ثم استخدامها: من اشتقاق يؤسس صيغة وآخر يستخدم تلك الصيغة كفرضية، تستنتج النتيجة المجمعة. توضح إزالة القطع أنه يمكن دائمًا إزالة هذه الليمات الوسيطة من حيث المبدأ.
- لماذا يمكن أن تؤدي إزالة القطع إلى إطالة البراهين بشكل كبير؟
- قد تتطلب إزالة القطع تكرار أجزاء كبيرة من الاشتقاق، وتكرار ذلك يمكن أن يزيد حجم البرهان بشكل هائل بمقدار برج من الأسس. لذا فإن البراهين الخالية من القطع أبسط من الناحية المفاهيمية ولكن يمكن أن تكون أكبر بكثير من البراهين الأصلية التي تحتوي على قطع.