حساب البرهان

في المنطق الرياضي ، يتم بناء حساب البرهان أو نظام البرهان لإثبات العبارات .

يتضمن نظام الإثبات المكونات التالية: ^{[ 1 ] [ 2 ]}

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

البرهان الرسمي لصيغة سليمة في نظام البرهان هو مجموعة من البديهيات وقواعد الاستدلال الخاصة بنظام البرهان والتي تستنتج أن الصيغة السليمة هي نظرية لنظام البرهان. ^{[ 2 ]}

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

أكثر حسابات البرهان شهرة هي تلك الحسابات الكلاسيكية التي لا تزال مستخدمة على نطاق واسع:

• فئة أنظمة هيلبرت ، ^{[ 2 ]} والتي يُعد نظام هيلبرت-أكرمان لعام 1928 لمنطق الرتبة الأولى مثالها الأكثر شهرة ؛
• حساب جيرهارد جينتزن للاستنتاج الطبيعي ، وهو أول شكل رسمي لنظرية البرهان الهيكلي ، والذي يمثل حجر الزاوية في تطابق الصيغ كأنواع الذي يربط المنطق بالبرمجة الوظيفية ؛
• حساب التفاضل والتكامل المتتالي لجينتزن ، وهو الشكل الأكثر دراسة لنظرية البرهان الهيكلي.

كانت العديد من حسابات البرهان الأخرى، أو ربما كانت، أساسية، ولكنها لا تستخدم على نطاق واسع اليوم.

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

تزخر الأبحاث الحديثة في مجال المنطق بحسابات البرهان المتنافسة:

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

• طريقة الجداول التحليلية
• إجراءات الإثبات
• نظام إثبات القضايا
• القرار (المنطق)