ورقة بحثية من 19 صفحة إنْ كنتَ قادرا على دارستها وفهمها فأنت منطقيٌّ حقٌّ وتستطيع مجالسة كارت غودل لو كان حيا!

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

وقد ظهرت عبقرية غنتزن -الذي مات بالجوع وعمره لم يجاوز 36 سنة- في صناعة أنظمة استطاعت الإحاطة بالطريقة الطبيعية التي يتمنطق عبرها الرياضيون محافظةً على الصرامة الرياضية

وأول منجزاته الثورية تمثَّل في الاستنباط الطبيعي Natural Deduction الذي أظهر عبره كيف تُبنَى البراهين المعقدة من قوانين بسيطة وحدسية، فبدلا من البدء من بدهيات معينة، بيَّن غنتزن أن كل مفهوم منطقي (مثل and و or وimplies) يمكن فهمه من خلال قوانين تظهر كيف تدخل تلك المفاهيم وتستبعدها من الإثباتات. وقد عكس هذا كيف يفكر الرياضيون فعلا، فإذا أردت إثبات "A and B" فإنك تثبت بطبيعية A ثم B. وإذا عرفت "A and B"، فإنك تشعر بشكل طبيعي أن عليك استخدام A أو B حسبما هو مطلوب.

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