لا يفتح طالب المنطق اليوم كتابًا، ولا يشغّل مساعدَ برهنة آليًّا Automated Theorem Provers، ولا يحضر محاضرةً في الاستدلال، إلا ويَدِين لما وضعه هذا الشابّ، واسمُه قليل الشهرة خارج الدوائر الرياضية العالية.
غيرارد غنتزن Gerhard Gentzen أعظم المناطقة الرياضيين في القرن العشرين، إلى حدِّ أنَّ كورت غودل نفسَه عدَّه منطقيًّا أفضلَ منه. كما أن جزءًا كبيرًا مما نصفه بالمنطق الرياضي اليوم يُحاكَم إلى مجموعة ضوابط وشروط، فإنْ وافقها قيل «منطق غنتزن» وإنْ جاوَزَها لم نقُل.
كان ديفيد هلبرت قد سأل في سياق برنامجه الشهير لحلحلة الأزمة التأسيسية للرياضيات: كيف نضمن أن حساب الأعداد لا يقع في تناقض، أي: لا يبرهن قضيةً ونقيضَها معًا؟ وكان ملخَّصُ إجابة غودل سنة 1931 بأن الحساب عاجزٌ عن برهان اتساق نفسه. ثم جاء غنتزن سنة 1936 وهو ابن 26 سنة فبرهن اتساق الحساب من خارجه، وهو ما يسمى إثباتَ اتساقٍ نسبيًّا relative consistency proof: أنْ تردّ اتساق النظام إلى مبدأ لا يملكه النظام نفسُه. والمبدأ الزائد هنا واحد: الاستقراء ما بعد المتناهي transfinite induction.
وعند سنة 1943 كشف عمّا نسمّيه اليوم الرتبة البرهانية proof-theoretic ordinal لحساب بيانو Peano Arithmetic: قاسَ المقدار المطلوب من مبدأ transfinite induction قياسًا دقيقًا. وبيان ذلك أنك بعد 0 و1 و2 و3... تبلغ أولَ عدد لانهائي ω، ثم ω+1، ثم ω+ω، ثم ω×ω، ثم ω^ω، ثم ω^(ω^ω)، وهكذا، لا تقف؛ إلى نهاية هذا التي تسمى ε₀. أثبت غنتزن أن حساب بيانو يبرهن الاستقراءَ عند كل رتبة دون ε₀، ويعجز عنه عند ε₀ نفسها. فصار للحساب عددٌ يقيس قوّته. ومن هنا وُلد التحليل الرتبي ordinal analysis: أن تُعطى كل نظرية رياضية عددًا ترتيبيًّا، فتُقارَن نظريتان متباعدتان بعددين، ويقال: هذه أقوى من تلك بمقدار كذا.
ولهذا القياس أثر مباشر في مسائل معروفة. فمتتالية غودستين Goodstein مثلًا تأخذ عددًا طبيعيًّا وتكتبه بالأساس 2 كتابةً متكرّرة، ثم ترفع الأساس إلى 3 وتنقص واحدًا، ثم إلى 4 وتنقص واحدًا، وهكذا. المتتالية البادئة من العدد 4 وحدَه تبلغ ذروةً مقدارها 3×2⁴⁰²⁶⁵³²¹¹ تقريبًا، وتهبط بعدها إلى الصفر. وكلُّ متتالية غودستين تنتهي إلى الصفر مهما كان مبدؤها. هذه قضية عن الأعداد الطبيعية صحيحة قطعًا، لكن حساب بيانو عاجزٌ عن برهانها. وسبب عجزه محدَّد: برهانها يحتاج الاستقراء عند ε₀، لكنَّ الحساب لا يبلغها، ومثلها لعبة الهيدرا Kirby–Paris ومبرهنة Paris–Harrington.
بل لغنتزن أفضالٌ تصِل لغات البرمجة قبل عصر الحواسيب
فقواعد الاستنباط الطبيعي Natural Deduction التي وضعها سنة 1933 اتضح بعد عشرين سنة أنها هي نفسها قواعد حساب لامدا المُنمَّط simply typed lambda calculus، لا تشبهها، بل تطابقها: القضية proposition تقابل النمط type، والبرهان يقابل برنامجًا، وتبسيط البرهان يقابل تنفيذ البرنامج. سيفهم المشتغلون بنظرية لغات البرمجة Programming Language Theory أنّ ذا هو تطابق Curry–Howard. ولذلك حين نكتب اليوم في مساعدات البرهنة الحوسبية Lean أو Coq أو Agda أو حتى Isabelle فنحن نبرهن ونبرمج بفعل واحد.
كان المنطق قبل غنتزن يُكتَب على طريقة فريجه وراسل: مسلَّمات كثيرة وقاعدة استدلال واحدة، وهي طريقة بعيدة عن استدلال الرياضيّ في عمله الفعليّ. فأراد غنتزن نظامًا يحاكي ما يفعله الرياضي حقًّا: 1) يفترض، و2) يستنتج، ثم 3) يرفع افتراضه. فوضع نظامَيْن للاستنباط الطبيعي، واحدٌ NK وهو للمنطق الكلاسيكي، والثاني NJ للمنطق الحدسي. ووضع معهما حساب المتتاليات LK/LJ لا ليبرهن به، بل ليحلّل البراهين نفسها.
وبحساب المتتاليات أثبت مبرهنته الكبرى Hauptsatz، أي حذف القطع cut elimination. والقطع هو أن تستعين في برهانك بقضية وسيطة لا أثر لها في المطلوب. أثبت غنتزن أن كل برهان يمكن ردّه إلى برهان خالٍ من هذه الوسائط، لا تظهر فيه إلا الصيغ الجزئية subformulas من المطلوب نفسه. ومن هنا صارت البرهنة الآلية ممكنةً أصلًا: من يفتّش عن برهان مع القطع يفتّش في فضاء لا نهائي لأن الوسائط الممكنة لا حصر لها، أما بلا قطع فالمواد كلها محصورة سلفًا في نصّ المطلوب.
فما معنى "منطق غنتزن Gentzen Logic" الذي يُحاكَم إليه كثيرٌ مما يُسمّى منطقًا اليوم؟ معناه أن الرابط المنطقي لا يُقبَل لمجرد أنك كتبت له قواعد، بل يُشترط أن تُعرِّفَهُ قواعدُ إدخاله، وألّا تستخرج منه قواعدُ حذفه أكثر مما أدخلَتْهُ فيه؛ وهذا سمَّاه داغ براويتز Prawitz ومايكل دوميت Dummet التناغمَ harmony. فقد اخترع المنطقي الهولندي بريور Brouwer (وهو من أشد المتأثرين بشوبنهاور ومدافعٌ شرس عنه) رابطًا سماه tonk، قاعدةُ إدخاله مِن: "و" وقاعدة حذفه مِن: "أو"، فصار بوسعك أن تبرهن كل شيء من أي شيء. فهو رابط سليم الشكل، لكنه ليس منطقيًّا، لأن حذفه يستخرج ما لم يُدخِلْه إدخالُه، ولأن النظام معه لا يقبل حذف القطع. فما وافق الشرط فهو منطق، وما جاوزه فلا.
وطريفٌ أن نسخته الأولى من إثبات الاتساق سنة 1935 بلغت المطبعة، فاعترض غودل وبول برنايز Paul Bernays بأن حجّتها ليست إنهائية finitistic بالمعنى الذي اشترطه هلبرت، فسحبها وأعاد بناء الجزء الحرِج ونشر بدلها نسخةً ثانية سنة 1936. وقبلها سنة 1933 اكتشف الترجمة السالبة negative translation، وهي ردّ الحساب من المنطق الكلاسيكي إلى الحدسي، اكتشافًا مستقلًّا عن غودل تمامًا، فلما ظهر بحث غودل سحب بحثه. أما النصّان المسحوبان -النسخةُ الأولى بعينها، وورقةُ الترجمة السالبة- فلم يُنشرا إلا بعد موته بنحو 30 سنة.
وقليل من حياته، أنه دخل كتيبة العاصفة النــــازية (الـSA) سنة 1933 من غير أن يُكرَه على ذلك، ودخل الحزب النــــازي سنة 1937، وأقسم يمين الولاء لهتـــلر سنة 1939 ضمن تعيينه الأكاديمي، وخدم في سلاح الإشارة التابع لWaffen-SS حتى انهار صحيًّا سنة 1942. ثم انتقل سنة 1943 إلى الجامعة الألمانية ببراغ، وهناك اشتغل بعقد من الـSS في حسابات تخصّ مشروع صاروخ V-2. فلمّا وقع ما يُسمى بانتفاضة براغ في 1945، اعتُقل وآخرون معه، وسُلِّم إلى السوفييت، حيث وضعوه في معسكر اعتقال، ومنعوا عنه الطعام حتى مات جوعًا في اليوم الرابع من 08/1945 وعمره 35 سنة، ودُفن في قبر بلا شاهد في مقبرة Ďáblice ببراغ.
قبل اعتقاله بأشهر أخبر زملاءه أنه ظفر بإثبات اتساقية التحليل consistency of analysis، أي الحساب من الرتبة الثانية second-order arithmetic. لكنْ لم يُعثَر على ورقة واحدة من ذلك.
والذي في الصورة كتاب من 450 صفحة، سيرتُه الذاتية مدموجةً بأعماله المنطقية والرياضية، وإني أجدُه من أحلى المكتوب في تاريخ الرياضيات والمنطق الرياضي
غيرارد غنتزن Gerhard Gentzen أعظم المناطقة الرياضيين في القرن العشرين، إلى حدِّ أنَّ كورت غودل نفسَه عدَّه منطقيًّا أفضلَ منه. كما أن جزءًا كبيرًا مما نصفه بالمنطق الرياضي اليوم يُحاكَم إلى مجموعة ضوابط وشروط، فإنْ وافقها قيل «منطق غنتزن» وإنْ جاوَزَها لم نقُل.
كان ديفيد هلبرت قد سأل في سياق برنامجه الشهير لحلحلة الأزمة التأسيسية للرياضيات: كيف نضمن أن حساب الأعداد لا يقع في تناقض، أي: لا يبرهن قضيةً ونقيضَها معًا؟ وكان ملخَّصُ إجابة غودل سنة 1931 بأن الحساب عاجزٌ عن برهان اتساق نفسه. ثم جاء غنتزن سنة 1936 وهو ابن 26 سنة فبرهن اتساق الحساب من خارجه، وهو ما يسمى إثباتَ اتساقٍ نسبيًّا relative consistency proof: أنْ تردّ اتساق النظام إلى مبدأ لا يملكه النظام نفسُه. والمبدأ الزائد هنا واحد: الاستقراء ما بعد المتناهي transfinite induction.
وعند سنة 1943 كشف عمّا نسمّيه اليوم الرتبة البرهانية proof-theoretic ordinal لحساب بيانو Peano Arithmetic: قاسَ المقدار المطلوب من مبدأ transfinite induction قياسًا دقيقًا. وبيان ذلك أنك بعد 0 و1 و2 و3... تبلغ أولَ عدد لانهائي ω، ثم ω+1، ثم ω+ω، ثم ω×ω، ثم ω^ω، ثم ω^(ω^ω)، وهكذا، لا تقف؛ إلى نهاية هذا التي تسمى ε₀. أثبت غنتزن أن حساب بيانو يبرهن الاستقراءَ عند كل رتبة دون ε₀، ويعجز عنه عند ε₀ نفسها. فصار للحساب عددٌ يقيس قوّته. ومن هنا وُلد التحليل الرتبي ordinal analysis: أن تُعطى كل نظرية رياضية عددًا ترتيبيًّا، فتُقارَن نظريتان متباعدتان بعددين، ويقال: هذه أقوى من تلك بمقدار كذا.
ولهذا القياس أثر مباشر في مسائل معروفة. فمتتالية غودستين Goodstein مثلًا تأخذ عددًا طبيعيًّا وتكتبه بالأساس 2 كتابةً متكرّرة، ثم ترفع الأساس إلى 3 وتنقص واحدًا، ثم إلى 4 وتنقص واحدًا، وهكذا. المتتالية البادئة من العدد 4 وحدَه تبلغ ذروةً مقدارها 3×2⁴⁰²⁶⁵³²¹¹ تقريبًا، وتهبط بعدها إلى الصفر. وكلُّ متتالية غودستين تنتهي إلى الصفر مهما كان مبدؤها. هذه قضية عن الأعداد الطبيعية صحيحة قطعًا، لكن حساب بيانو عاجزٌ عن برهانها. وسبب عجزه محدَّد: برهانها يحتاج الاستقراء عند ε₀، لكنَّ الحساب لا يبلغها، ومثلها لعبة الهيدرا Kirby–Paris ومبرهنة Paris–Harrington.
بل لغنتزن أفضالٌ تصِل لغات البرمجة قبل عصر الحواسيب
فقواعد الاستنباط الطبيعي Natural Deduction التي وضعها سنة 1933 اتضح بعد عشرين سنة أنها هي نفسها قواعد حساب لامدا المُنمَّط simply typed lambda calculus، لا تشبهها، بل تطابقها: القضية proposition تقابل النمط type، والبرهان يقابل برنامجًا، وتبسيط البرهان يقابل تنفيذ البرنامج. سيفهم المشتغلون بنظرية لغات البرمجة Programming Language Theory أنّ ذا هو تطابق Curry–Howard. ولذلك حين نكتب اليوم في مساعدات البرهنة الحوسبية Lean أو Coq أو Agda أو حتى Isabelle فنحن نبرهن ونبرمج بفعل واحد.
كان المنطق قبل غنتزن يُكتَب على طريقة فريجه وراسل: مسلَّمات كثيرة وقاعدة استدلال واحدة، وهي طريقة بعيدة عن استدلال الرياضيّ في عمله الفعليّ. فأراد غنتزن نظامًا يحاكي ما يفعله الرياضي حقًّا: 1) يفترض، و2) يستنتج، ثم 3) يرفع افتراضه. فوضع نظامَيْن للاستنباط الطبيعي، واحدٌ NK وهو للمنطق الكلاسيكي، والثاني NJ للمنطق الحدسي. ووضع معهما حساب المتتاليات LK/LJ لا ليبرهن به، بل ليحلّل البراهين نفسها.
وبحساب المتتاليات أثبت مبرهنته الكبرى Hauptsatz، أي حذف القطع cut elimination. والقطع هو أن تستعين في برهانك بقضية وسيطة لا أثر لها في المطلوب. أثبت غنتزن أن كل برهان يمكن ردّه إلى برهان خالٍ من هذه الوسائط، لا تظهر فيه إلا الصيغ الجزئية subformulas من المطلوب نفسه. ومن هنا صارت البرهنة الآلية ممكنةً أصلًا: من يفتّش عن برهان مع القطع يفتّش في فضاء لا نهائي لأن الوسائط الممكنة لا حصر لها، أما بلا قطع فالمواد كلها محصورة سلفًا في نصّ المطلوب.
فما معنى "منطق غنتزن Gentzen Logic" الذي يُحاكَم إليه كثيرٌ مما يُسمّى منطقًا اليوم؟ معناه أن الرابط المنطقي لا يُقبَل لمجرد أنك كتبت له قواعد، بل يُشترط أن تُعرِّفَهُ قواعدُ إدخاله، وألّا تستخرج منه قواعدُ حذفه أكثر مما أدخلَتْهُ فيه؛ وهذا سمَّاه داغ براويتز Prawitz ومايكل دوميت Dummet التناغمَ harmony. فقد اخترع المنطقي الهولندي بريور Brouwer (وهو من أشد المتأثرين بشوبنهاور ومدافعٌ شرس عنه) رابطًا سماه tonk، قاعدةُ إدخاله مِن: "و" وقاعدة حذفه مِن: "أو"، فصار بوسعك أن تبرهن كل شيء من أي شيء. فهو رابط سليم الشكل، لكنه ليس منطقيًّا، لأن حذفه يستخرج ما لم يُدخِلْه إدخالُه، ولأن النظام معه لا يقبل حذف القطع. فما وافق الشرط فهو منطق، وما جاوزه فلا.
وطريفٌ أن نسخته الأولى من إثبات الاتساق سنة 1935 بلغت المطبعة، فاعترض غودل وبول برنايز Paul Bernays بأن حجّتها ليست إنهائية finitistic بالمعنى الذي اشترطه هلبرت، فسحبها وأعاد بناء الجزء الحرِج ونشر بدلها نسخةً ثانية سنة 1936. وقبلها سنة 1933 اكتشف الترجمة السالبة negative translation، وهي ردّ الحساب من المنطق الكلاسيكي إلى الحدسي، اكتشافًا مستقلًّا عن غودل تمامًا، فلما ظهر بحث غودل سحب بحثه. أما النصّان المسحوبان -النسخةُ الأولى بعينها، وورقةُ الترجمة السالبة- فلم يُنشرا إلا بعد موته بنحو 30 سنة.
وقليل من حياته، أنه دخل كتيبة العاصفة النــــازية (الـSA) سنة 1933 من غير أن يُكرَه على ذلك، ودخل الحزب النــــازي سنة 1937، وأقسم يمين الولاء لهتـــلر سنة 1939 ضمن تعيينه الأكاديمي، وخدم في سلاح الإشارة التابع لWaffen-SS حتى انهار صحيًّا سنة 1942. ثم انتقل سنة 1943 إلى الجامعة الألمانية ببراغ، وهناك اشتغل بعقد من الـSS في حسابات تخصّ مشروع صاروخ V-2. فلمّا وقع ما يُسمى بانتفاضة براغ في 1945، اعتُقل وآخرون معه، وسُلِّم إلى السوفييت، حيث وضعوه في معسكر اعتقال، ومنعوا عنه الطعام حتى مات جوعًا في اليوم الرابع من 08/1945 وعمره 35 سنة، ودُفن في قبر بلا شاهد في مقبرة Ďáblice ببراغ.
قبل اعتقاله بأشهر أخبر زملاءه أنه ظفر بإثبات اتساقية التحليل consistency of analysis، أي الحساب من الرتبة الثانية second-order arithmetic. لكنْ لم يُعثَر على ورقة واحدة من ذلك.
والذي في الصورة كتاب من 450 صفحة، سيرتُه الذاتية مدموجةً بأعماله المنطقية والرياضية، وإني أجدُه من أحلى المكتوب في تاريخ الرياضيات والمنطق الرياضي
