دليل جينتزن على الاتساق

يُعدّ برهان اتساق جنتزن نتيجةً لنظرية البرهان في المنطق الرياضي ، وقد نشره غيرهارد جنتزن عام ١٩٣٦. يُبيّن هذا البرهان أن بديهيات بيانو للحساب من الرتبة الأولى لا تحتوي على تناقض (أي أنها " متسقة ")، طالما أن نظامًا آخر مُستخدمًا في البرهان لا يحتوي على أي تناقضات أيضًا. هذا النظام الآخر، الذي يُطلق عليه اليوم " الحساب الاستقرائي البدائي مع مبدأ إضافي للاستقراء المتسامي الخالي من المُكمِّمات حتى الترتيب ε₀ _" ، ليس أضعف ولا أقوى من نظام بديهيات بيانو. جادل جنتزن بأنه يتجنب أنماط الاستدلال المشكوك فيها الواردة في حساب بيانو، وبالتالي فإن اتساقه أقل إثارةً للجدل.

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

أثبت جنتزن أن اتساق بديهيات بيانو من الرتبة الأولى قابل للإثبات على أساس نظرية الحساب التكراري البدائي، مع مبدأ إضافي للاستقراء المتجاوز الخالي من المُكمِّمات حتى الترتيب ε₀ _. يُعد الحساب التكراري البدائي شكلاً مبسطاً للغاية من الحساب، وهو غير مثير للجدل إلى حد كبير. ويعني المبدأ الإضافي، بشكل غير رسمي، وجود ترتيب جيد على مجموعة الأشجار الجذرية المنتهية . أما ε₀، _فهو الترتيب الأول.${\displaystyle \alpha }$بحيث${\displaystyle \omega ^{\alpha }=\alpha }$أي نهاية المتتالية

${\displaystyle \omega ,\ \omega ^{\omega },\ \omega ^{\omega ^{\omega }},\ \ldots }$

هو عدد ترتيبي قابل للعد أصغر بكثير من الأعداد الترتيبية الكبيرة القابلة للعد . وللتعبير عن الأعداد الترتيبية بلغة الحساب، نحتاج إلى ترميز ترتيبي ، أي طريقة لتخصيص أعداد طبيعية للأعداد الترتيبية الأقل من _ε₀ . يمكن القيام بذلك بطرق مختلفة، ومنها على سبيل المثال نظرية كانتور للصيغة الطبيعية . يعتمد برهان جنتزن على الافتراض التالي: لأي صيغة خالية من المُكمِّمات A(x)، إذا وُجد عدد ترتيبي a < ε₀ _تكون A(a) خاطئة عنده، فإنه يوجد عدد ترتيبي أصغر من هذا النوع.

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

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

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

تنص صيغة قوية لنظرية عدم الاكتمال الثانية، التي أثبتها بافيل بودلاك ^{[ 2 ] ،} مستندًا إلى عمل سابق لسولومون فيفرمان [ ^{3 ]،} على أنه لا يمكن لأي نظرية متسقة T تحتوي على حساب روبنسون ، Q، أن تفسر Q + Con(T)، أي العبارة التي تنص على أن T متسقة. في المقابل، تفسر Q + Con(T) نظرية T، وذلك من خلال صيغة قوية لنظرية الاكتمال الحسابي . لذا، فإن Q + Con(T) أقوى دائمًا (بمعنى وجيه) من T. لكن نظرية جنتزن تفسر Q + Con(PA) بشكل بديهي، لأنها تحتوي على Q وتثبت Con(PA)، وبالتالي تفسر نظرية جنتزن نظرية PA. ولكن، وفقًا لنتيجة بودلاك، لا يمكن لنظرية PA أن تفسر نظرية جنتزن، لأن نظرية جنتزن (كما ذُكر آنفًا) تفسر Q + Con(PA)، وقابلية التفسير متعدية. بمعنى آخر: إذا فسّر حساب بيانو نظرية جنتزن، فإنه سيفسّر أيضًا Q+Con(PA)، وبالتالي سيكون غير متسق، وفقًا لنتيجة بودلاك. لذا، من حيث قوة الاتساق، كما تتميز بقابلية التفسير، فإن نظرية جنتزن أقوى من حساب بيانو.

أدلى هيرمان فايل بالتعليق التالي في عام 1946 بشأن أهمية نتيجة الاتساق التي توصل إليها جنتزن في أعقاب التأثير المدمر لنتيجة عدم الاكتمال التي توصل إليها غودل عام 1931 على خطة هيلبرت لإثبات اتساق الرياضيات. ^{[ 4 ]}

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

أدلى كلين (2009 ، ص 479) بالتعليق التالي في عام 1952 حول أهمية نتيجة جنتزن، لا سيما في سياق البرنامج الشكلي الذي بدأه هيلبرت. 

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

في المقابل، علق بيرنايز (1967) على ما إذا كان اقتصار هيلبرت على الأساليب المحدودة مقيدًا للغاية:

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

لم تُنشر النسخة الأولى من برهان جينتزن على الاتساق خلال حياته، وذلك لاعتراض بول بيرنايز على طريقة استُخدمت ضمنيًا في البرهان. أما البرهان المُعدَّل، الموصوف أعلاه، فقد نُشر عام ١٩٣٦ في مجلة "حوليات الرياضيات" . ثم نشر جينتزن برهانين آخرين على الاتساق، أحدهما عام ١٩٣٨ والآخر عام ١٩٤٣. جميع هذه البراهين موجودة في ( جينتزن وسزابو ١٩٦٩ ) .

أعاد كورت غودل تفسير برهان غنتزن لعام 1936 في محاضرة ألقاها عام 1938، فيما عُرف لاحقًا بتفسير انعدام الأمثلة المضادة. ويمكن فهم كل من البرهان الأصلي وإعادة صياغته من منظور نظرية الألعاب. ( تيت 2005 ) .

في عام 1940 نشر ويلهلم أكرمان برهانًا آخر على الاتساق لحساب بيانو، باستخدام الترتيب ε ₀ أيضًا .

وقد نشر IN Khlodovskii دليلاً آخر على اتساق الحساب في عام 1959.

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

في هذه اللغة، يثبت عمل جنتزن أن الترتيب الإثباتي لحساب بيانو من الدرجة الأولى هو ε ₀ .

أثبت لورانس كيربي وجيف باريس في عام 1982 أن نظرية غودستين لا يمكن إثباتها في حساب بيانو. واستند برهانهما إلى نظرية جنتزن. ^{[ 5 ]}

• إدواردز، بول، محرر. (1967). "بول بيرنايز". موسوعة الفلسفة . المجلد  3. ماكميلان وفري برس. ص  502.
• فيفرمان، سولومون (1960). "تطبيق الحساب على ما وراء الرياضيات في سياق عام" . مجلة Fundamenta Mathematicae . 49 (1): 35-92 . doi : 10.4064/fm-49-1-35-92 . ISSN 0016-2736 . 
• Gentzen، Gerhard (1936)، “Die Widerspruchsfreiheit derrainen Zahlentheorie” ، Mathematische Annalen ، 112 : 493–565 ، دوى : 10.1007 / BF01565428 ، S2CID 122719892 – تُرجمت إلى "اتساق الحساب"، في ( جينتزن وسزابو 1969 ) .
• Gentzen، Gerhard (1938)، “Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie”، Forschungen zur Logik und zur Grundlegung der Exakten Wissenschaften ، 4 : 19– 44– تُرجمت إلى "نسخة جديدة من برهان الاتساق لنظرية الأعداد الأولية"، في ( Gentzen & Szabo 1969 ) .
• جنتزن، جيرهارد (1969)، سابو، م. إ . (محرر)، الأوراق المجمعة لجيرهارد جنتزن ، دراسات في المنطق وأسس الرياضيات (  طبعة غلاف مقوى)، أمستردام: نورث هولاند، رقم ISBN 978-0-7204-2254-2- ترجمة إنجليزية للأوراق البحثية.
• غودل، ك. (2001) [1938]، "محاضرة في زيلسل" ، في فيفرمان، سولومون (محرر)، كورت غودل: الأعمال الكاملة ، المجلد  الثالث: مقالات ومحاضرات غير منشورة (  طبعة غلاف ورقي)، مطبعة جامعة أكسفورد، الصفحات 87-113 ، ISBN  978-0-19-514722-3
• جيرفيل، هيرمان روج (1999)، دورة في نظرية البرهان (مسودة كتاب مدرسي  )، مؤرشف من الأصل في 2011-06-07
• خلودوفسكي، إي إن (1959)، "برهان جديد على اتساق الحساب" (ملف PDF) ، أوسبيخي مات. ناوك ، 14 (6 ( 90)): 105-140
• كيربي، ل .؛ باريس، ج. (1982)، "نتائج الاستقلال المتاحة لحساب بيانو" (ملف PDF) ، نشرة جمعية لندن الرياضية ، 14 (4): 285-293 ، CiteSeerX 10.1.1.107.3303 ، doi : 10.1112/blms/14.4.285 ، مؤرشف من النسخة الأصلية (ملف PDF) بتاريخ 12 سبتمبر 2014 
• كلين، ستيفن كول (2009) [1952]. مقدمة في ما وراء الرياضيات . دار إيشي للنشر الدولية. ISBN 978-0-923891-57-2.
• بودلاك، بافيل (1 يونيو 1985). "القطع، وبيانات الاتساق، والتفسيرات" . مجلة المنطق الرمزي . 50 (2): 423-441 . doi : 10.2307/2274231 . ISSN 0022-4812 . JSTOR 2274231 .  
• تايت، دبليو دبليو (2005)، "إعادة صياغة غودل لأول برهان اتساق لجينتزن في الحساب: تفسير انعدام الأمثلة المضادة" (ملف PDF) ، نشرة المنطق الرمزي ، 11 (2): 225-238 ، doi : 10.2178/bsl/1120231632 ، ISSN 1079-8986 ، S2CID 9481361  
• ويل، هيرمان (2012). مستويات اللانهاية: مختارات من كتابات في الرياضيات والفلسفة . نيويورك: منشورات دوفر. ISBN 978-0-486-48903-2.