نظرية البرهان
تدرس نظرية البرهان البراهين الصورية ككائنات رياضية قائمة بذاتها، وتحلل بنيتها وتحولاتها وقوة النظريات التي تنتجها.
Definition
نظرية البرهان هي فرع المنطق الرياضي الذي يتعامل مع البراهين في الأنظمة الصورية ككائنات توافقية محدودة، ويدرس كيفية تحويلها وتطبيعها وما تكشفه وجودها عن اتساق وقوة النظريات الأساسية.
Scope
يغطي هذا المجال الحسابات الصورية مثل الاستنتاج الطبيعي وحساب المتتاليات، ونظريات إزالة القطع والتطبيع، ونظريات عدم الاكتمال لغودل، وقياس قوة النظريات بتحليل الترتيب، والمحتوى البنائي والحسابي للبراهين الذي تكشفه المراسلات بين البراهين والبرامج.
Sub-topics
Core questions
- كيف يمكن تمثيل البراهين الصورية ومعالجتها ككائنات توافقية؟
- ما هي التحويلات التي يمكن إزالتها بشكل منهجي من البراهين، وماذا يكشف ذلك؟
- ما هي الحدود المتأصلة لما يمكن لنظرية صورية أن تثبته عن نفسها؟
- كيف يمكن قياس قوة النظرية بدقة؟
Key theories
- نظرية إزالة القطع
- أظهر غنتسن أن أي برهان في حساب المتتاليات يمكن تحويله إلى برهان بدون قاعدة القطع، مما ينتج براهين ذات خاصية الصيغة الفرعية ونتائج اتساق مباشرة.
- نظريات عدم الاكتمال لغودل
- تحتوي أي نظرية صورية متسقة وقوية بما يكفي للتعبير عن الحساب على جمل صحيحة لا يمكنها إثباتها ولا يمكنها إثبات اتساقها الخاص، مما يحدد قيودًا أساسية على الصياغة الرسمية.
- مراسلات كاري-هاورد
- تتوافق البراهين في الاستنتاج الطبيعي مع مصطلحات حساب لامدا المكتوب، ويتوافق تطبيع البرهان مع الحساب، مما يربط نظرية البرهان بنظرية لغات البرمجة.
Clinical relevance
تكمن نظرية البرهان في أساس تحليل الاتساق والمحتوى البنائي في الرياضيات وتوفر الأساس النظري لنظرية الأنواع، والبرمجة الوظيفية، ومساعدي البرهان الآلي، حيث تعمل البراهين كبرامج قابلة للتحقق.
History
تأسست نظرية البرهان على يد هيلبرت كجزء من برنامجه لتأمين الرياضيات ببراهين اتساق محدودة. أظهرت نظريات عدم الاكتمال لغودل عام 1931 أن البرنامج الأصلي لا يمكن أن ينجح بالكامل، وأعادت إزالة القطع لغنتسن وبرهان الاتساق للحساب عبر الاستقراء الفوق متناهي توجيه المجال نحو تحليل الترتيب، ولاحقًا، نموذج البراهين كبرامج.
Key figures
- David Hilbert
- Gerhard Gentzen
- Kurt Goedel
- Jean-Yves Girard
Related topics
Seminal works
- troelstra2000
- takeuti1987
- girard1989
Frequently asked questions
- كيف تختلف نظرية البرهان عن نظرية النموذج؟
- تدرس نظرية النموذج البنى وحقيقة الجمل فيها، وهو منظور دلالي، بينما تدرس نظرية البرهان الاشتقاقات الصورية وتحولاتها النحوية. تربط نظرية الاكتمال لغودل بين الاثنين، لكن أساليبهما وأسئلتهما متميزة.
- ما هو برنامج هيلبرت؟
- كان اقتراحًا لإثبات اتساق جميع الرياضيات باستخدام استدلال محدود وغير مثير للجدل فقط. أظهرت نظرية عدم الاكتمال الثانية لغودل أنه لا يمكن لأي نظرية قوية بما فيه الكفاية إثبات اتساقها الخاص، لذلك لا يمكن تنفيذ البرنامج بشكله الأصلي، على الرغم من أن الإصدارات المعدلة لا تزال مؤثرة.