نظرية الإثبات

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

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

على الرغم من أن صياغة المنطق الرسمية قد شهدت تقدماً كبيراً بفضل أعمال شخصيات مثل غوتلوب فريجه ، وجوزيبي بيانو ، وبرتراند راسل ، وريتشارد ديديكيند ، إلا أن تاريخ نظرية البرهان الحديثة يُنسب غالباً إلى ديفيد هيلبرت ، الذي أطلق ما يُعرف ببرنامج هيلبرت في كتابه "أسس الرياضيات" . وتتلخص الفكرة الأساسية لهذا البرنامج في أنه إذا استطعنا تقديم براهين نهائية على اتساق جميع النظريات الرسمية المعقدة التي يحتاجها علماء الرياضيات، فسنتمكن من تأسيس هذه النظريات من خلال حجة ما وراء رياضية، تُظهر أن جميع تأكيداتها الشاملة البحتة (أو بتعبير أدق، تأكيداتها القابلة للإثبات)${\displaystyle \Pi _{1}^{0}}$الجمل صحيحة بشكل نهائي؛ بمجرد أن نثبت ذلك، لا نهتم بالمعنى غير النهائي لنظرياتها الوجودية، ونعتبرها شروطًا زائفة المعنى لوجود الكيانات المثالية.

تم إثبات فشل البرنامج من خلال نظريات عدم الاكتمال لكورت غودل ، والتي بينت أن أي نظرية متسقة من النوع ω قوية بما يكفي للتعبير عن بعض الحقائق الحسابية البسيطة، لا يمكنها إثبات اتساقها الذاتي، والذي هو، وفقًا لصياغة غودل،${\displaystyle \Pi _{1}^{0}}$ ومع ذلك، ظهرت نسخ معدلة من برنامج هيلبرت، وأُجريت أبحاث حول مواضيع ذات صلة. وقد أدى ذلك، على وجه الخصوص، إلى:

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

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

نظرية البرهان البنيوي هي فرع من فروع نظرية البرهان يدرس تفاصيل حسابات البرهان . وأشهر ثلاثة أنماط لحسابات البرهان هي:

• حسابات هيلبرت
• حسابات الاستنتاج الطبيعي
• الحسابات المتسلسلة

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

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

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

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

يدعم حساب الاستدلال الطبيعي لجينتزن مفهوم البرهان التحليلي، كما أوضح داغ براويتز . التعريف أكثر تعقيدًا بعض الشيء: نقول إن البراهين التحليلية هي الأشكال الطبيعية ، المرتبطة بمفهوم الشكل الطبيعي في إعادة كتابة الحدود . كما تدعم حسابات برهان أكثر تعقيدًا، مثل شبكات برهان جان إيف جيرار ، مفهوم البرهان التحليلي.

تُعدّ البراهين المركزة فئةً خاصةً من البراهين التحليلية التي تظهر في المنطق الاختزالي، وهي تُميّز مجموعةً كبيرةً من إجراءات البحث عن البراهين الموجهة نحو الهدف. وتُعتبر القدرة على تحويل نظام البرهان إلى شكلٍ مركّز مؤشراً جيداً على جودته التركيبية، على غرار كيف يُظهر قبول القطع أن نظام البرهان متسقٌ تركيبياً. ^{[ 4 ]}

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

بعض قواعد الاستدلال محلية ، وهي خاصية مرغوبة. ^{[ 5 ]} على سبيل المثال، لنأخذ  قاعدة ! في المنطق الخطي :$${\displaystyle {\frac {\vdash A,?B_{1},\dots ,?B_{n}}{\vdash !A,?B_{1},\dots ,?B_{n}}}}$$للتأكد من  تطبيق قاعدة ! بشكل صحيح على خطوة معينة من حساب التفاضل والتكامل التسلسلي${\displaystyle {\frac {\vdash A,B_{1},\dots ,B_{n}}{\vdash A',B_{1},\dots ,B_{n}}}}$ليس من الضروري فقط التحقق من ذلك${\displaystyle A'=?A}$ولكن من الضروري أيضًا التحقق من أن كل واحد من${\displaystyle B_{i}}$تحتوي على  علامة التعجب (!) كرابط منطقي خارجي. وبهذا المعنى، فإن القاعدة ليست محلية ، لأنه لتطبيقها، يجب التحقق من عدد غير محدود من الصيغ.

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

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

يُعدّ التحليل الترتيبي أسلوبًا قويًا لتقديم براهين الاتساق التوافقي لأنظمة فرعية من الحساب والتحليل ونظرية المجموعات. غالبًا ما تُفسَّر نظرية عدم الاكتمال الثانية لغودل على أنها تُثبت استحالة براهين الاتساق المحدود لنظريات ذات قوة كافية. يسمح التحليل الترتيبي بقياس المحتوى اللانهائي لاتساق النظريات بدقة. بالنسبة لنظرية T متسقة ومُؤَسَّسة بشكل تكراري، يُمكن إثبات في الحساب المحدود أن سلامة أساس عدد ترتيبي مُتجاوز مُعين يستلزم اتساق T. تُشير نظرية عدم الاكتمال الثانية لغودل إلى أنه لا يُمكن إثبات سلامة أساس هذا العدد الترتيبي في النظرية T.

تشمل نتائج التحليل الترتيبي (1) اتساق الأنظمة الفرعية للحساب الكلاسيكي من الدرجة الثانية ونظرية المجموعات بالنسبة للنظريات البنائية، (2) نتائج الاستقلال التوافقي، و(3) تصنيفات الدوال التكرارية الكلية المثبتة والترتيبات المؤسسة بشكل جيد المثبتة.

ابتكر جينتزن التحليل الترتيبي، حيث أثبت اتساق حساب بيانو باستخدام الاستقراء المتسامي حتى الترتيب ε₀ _{. وقد امتد التحليل الترتيبي ليشمل العديد من فروع الحساب من الرتبة الأولى والثانية ونظرية المجموعات. وكان أحد التحديات الرئيسية هو التحليل الترتيبي للنظريات غير التنبؤية. وكان أول إنجاز في هذا الاتجاه هو برهان} تاكيوتي على اتساق Π₁₁ ^- _CA₀ باستخدام طريقة المخططات الترتيبية.

منطق الإثبات هو منطق مشروط ، حيث يُفسَّر عامل المربع على أنه "من الممكن إثبات أن". والهدف هو تجسيد مفهوم محمول الإثبات لنظرية صورية غنية نسبيًا . وكبديهيات أساسية لمنطق الإثبات GL ( غودل - لوب )، الذي يجسد قابلية الإثبات في حساب بيانو ، تُؤخذ نظائر مشروطة لشروط اشتقاق هيلبرت-بيرنايز ونظرية لوب (إذا كان من الممكن إثبات أن قابلية إثبات A تستلزم A، فإن A قابلة للإثبات).

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

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

الرياضيات العكسية هي فرع من فروع المنطق الرياضي يسعى إلى تحديد البديهيات اللازمة لإثبات نظريات الرياضيات. ^{[ 6 ]} أسس هذا المجال هارفي فريدمان . ويمكن وصف منهجها الأساسي بأنه "الرجوع من النظريات إلى البديهيات "، على عكس الممارسة الرياضية التقليدية المتمثلة في اشتقاق النظريات من البديهيات. وقد سبقت نتائج في نظرية المجموعات، مثل النظرية الكلاسيكية التي تنص على تكافؤ بديهية الاختيار ومبرهنة زورن في نظرية مجموعات ZF، ظهور الرياضيات العكسية . مع ذلك، فإن هدف الرياضيات العكسية هو دراسة البديهيات المحتملة لنظريات الرياضيات العادية، وليس البديهيات المحتملة لنظرية المجموعات.

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

لكل نظرية يمكن صياغتها في النظام الأساسي ولكن لا يمكن إثباتها فيه، يكمن الهدف في تحديد نظام البديهيات الخاص (الأقوى من النظام الأساسي) اللازم لإثبات تلك النظرية. ولإثبات أن النظام S مطلوب لإثبات نظرية T ، يلزم برهانان. يُظهر البرهان الأول إمكانية إثبات T من S ؛ وهو برهان رياضي عادي مصحوب بتبرير لإمكانية تنفيذه في النظام S. أما البرهان الثاني، المعروف بالانعكاس ، فيُظهر أن T نفسها تستلزم S ؛ ويُنفذ هذا البرهان في النظام الأساسي. يُثبت الانعكاس أنه لا يمكن لأي نظام بديهيات S ′، الذي يُوسع النظام الأساسي، أن يكون أضعف من S مع قدرته على إثبات T. 

من الظواهر اللافتة في الرياضيات العكسية متانة أنظمة بديهيات الخمسة الكبرى . وتُسمى هذه الأنظمة _، مرتبةً حسب تزايد قوتها، بالاختصارات التالية: RCA₀ ، _WKL₀ ، _ACA₀ ، _ATR₀ ، _و Π₁₁₋CA₀ ^. _{وقد ثبت أن كل نظرية تقريبًا من نظريات الرياضيات العادية التي خضعت للتحليل الرياضي العكسي تُكافئ أحد هذه الأنظمة الخمسة. وقد} ركزت العديد من الأبحاث الحديثة على المبادئ التوافقية التي لا تندرج بسهولة ضمن هذا الإطار، مثل RT₂₂ ⁽ نظرية رامزي للأزواج).

غالباً ما تتضمن الأبحاث في الرياضيات العكسية أساليب وتقنيات من نظرية الاستدعاء الذاتي بالإضافة إلى نظرية البرهان.

التفسيرات الوظيفية هي تفسيرات للنظريات غير البنائية ضمن إطار النظريات الوظيفية. عادةً ما تتم هذه التفسيرات على مرحلتين. أولًا، يتم "اختزال" نظرية كلاسيكية (C) إلى نظرية حدسية (I). أي يتم توفير ربط بنائي يترجم نظريات (C) إلى نظريات (I). ثانيًا، يتم اختزال النظرية الحدسية (I) إلى نظرية دوال خالية من المُكمِّمات (F). تُسهم هذه التفسيرات في شكل من أشكال برنامج هيلبرت، إذ تُثبت اتساق النظريات الكلاسيكية بالنسبة للنظريات البنائية. وقد أسفرت التفسيرات الوظيفية الناجحة عن اختزال النظريات اللانهائية إلى نظريات منتهية، والنظريات غير التنبؤية إلى نظريات تنبؤية.

تُتيح التفسيرات الوظيفية أيضًا استخلاص معلومات بنّاءة من البراهين في النظرية المُختزلة. وكنتيجة مباشرة لهذا التفسير، يُستنتج عادةً أن أي دالة تكرارية يُمكن إثبات كليتها إما في I أو في C، تُمثَّل بحدٍّ من F. وإذا أمكن تقديم تفسير إضافي لـ F في I، وهو أمرٌ ممكنٌ أحيانًا، فإن هذا التوصيف يُثبت عادةً دقته. وغالبًا ما يتضح أن حدود F تتطابق مع فئة طبيعية من الدوال، مثل الدوال التكرارية الأولية أو الدوال القابلة للحساب في زمن متعدد الحدود. كما استُخدمت التفسيرات الوظيفية لتقديم تحليلات ترتيبية للنظريات وتصنيف دوالها التكرارية القابلة للإثبات.

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

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

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

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

• المنطق الوسيط
• نظرية النموذج
• الدليل (الحقيقة)
• أساليب الإثبات
• حساب المتتابعات

• ج. أفيغاد وإي إتش ريك (2001). "توضيح طبيعة اللانهائي: تطور ما وراء الرياضيات ونظرية البرهان ". تقرير كارنيجي ميلون الفني CMU-PHIL-120.
• باروايز، جون (1977). دليل المنطق الرياضي . دراسات في المنطق وأسس الرياضيات. المجلد  90. شركة نورث هولاند للنشر. ISBN 072042285XLCCN 76026032 . OCLC 2347202 .​  ( متاح للزبائن ذوي الإعاقات البصرية )
• S. Buss, ed. (1998) Handbook of Proof Theory . Elsevier.
• ج.جنتزن (1935/1969). " تحقيقات في الاستنباط المنطقي ". في مي زابو، أد. الأوراق المجمعة لجيرهارد جينتزن . شمال هولندا. ترجمة زابو من "Unter suchungen über das logische Schliessen"، Mathematisches Zeitschrift v. 39، الصفحات من  176 إلى 210، 405  431.
• جيرارد، جيه-واي ؛ تايلور، بي؛ لافونت، واي (2003) [1989]. البراهين والأنواع (ملف PDF) . مطبعة جامعة كامبريدج. ISBN 0521371813.
• براويتز، داج (1965). الاستنتاج الطبيعي: دراسة إثباتية نظرية . Acta Universitatis Stockholmiensis؛ دراسات ستوكهولم في الفلسفة، 3 . ستوكهولم، جوتنبرج، أوبسالا: المكفيست وويكسل . او سي ال سي 912927896 . 
• سيمبسون، إس جي (2010). الأنظمة الفرعية للحساب من الدرجة الثانية . منظورات في المنطق (  الطبعة الثانية). مطبعة جامعة كامبريدج. ISBN 9780521150149. OCLC 528432422 . 
• أ. س. ترويلسترا وهـ. شفيتشتنبرغ (1996). نظرية البرهان الأساسية ، سلسلة كامبريدج في علوم الحاسوب النظرية، مطبعة جامعة كامبريدج، رقم ISBN 0-521-77911-1.
• وانغ، هاو (1981). محاضرات مبسطة في المنطق الرياضي . شركة فان نوستراند رينهولد . ISBN 9780442231095. OCLC 6087107 . 

• "نظرية البرهان" ، موسوعة الرياضيات ، دار نشر EMS ، 2001 [1994]
• ج. فون أفلاطون (2008). تطور نظرية البرهان . موسوعة ستانفورد للفلسفة .