نظرية غودل للاكتمال

تُعد نظرية غودل للاكتمال نظرية أساسية في المنطق الرياضي تُثبت وجود علاقة بين الحقيقة الدلالية وإمكانية الإثبات النحوي في منطق الرتبة الأولى .

تنطبق نظرية الاكتمال على أي نظرية من الدرجة الأولى : إذا كانت T نظرية من هذا النوع، و φ جملة (باللغة نفسها)، وكان كل نموذج من T نموذجًا لـ φ ، فإنه يوجد برهان (من الدرجة الأولى) لـ φ باستخدام عبارات T كمسلمات . يُقال أحيانًا عن هذا "أي شيء صحيح في جميع النماذج قابل للإثبات". (لا يتعارض هذا مع نظرية عدم الاكتمال لغودل ، التي تتعلق بصيغة φ _u غير قابلة للإثبات في نظرية معينة T ولكنها صحيحة في النموذج " القياسي " للأعداد الطبيعية: φ _u خاطئة في بعض النماذج الأخرى "غير القياسية" لـ T. [ ^{1 ] )}

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

أثبتها كورت غودل لأول مرة عام 1929. ثم بُسّطت عندما لاحظ ليون هينكين في أطروحته للدكتوراه أن الجزء الصعب من البرهان يمكن تقديمه على شكل نظرية وجود النموذج (التي نُشرت عام 1949). ^{[ 2 ]} وقد بسّط جيسبرت هاسينياغر برهان هينكين عام 1953. ^{[ 3 ]}

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

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

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

نبدأ أولاً بتحديد نظام استنتاجي لحساب التفاضل والتكامل من الدرجة الأولى، باختيار أي من الأنظمة المتكافئة المعروفة. وقد افترض برهان غودل الأصلي نظام برهان هيلبرت - أكرمان .

شكل أكثر عمومية

يمكن التعبير عن النظرية بشكل أعم من حيث النتيجة المنطقية . نقول إن الجملة s هي نتيجة نحوية لنظرية T ، ويرمز لها بـ${\displaystyle T\vdash s}$إذا كان من الممكن إثبات s من T في نظامنا الاستنتاجي، نقول إن s هي نتيجة دلالية لـ T ، ونرمز لها بـ${\displaystyle T\models s}$إذا تحققت s في كل نموذج من T. تنص نظرية الاكتمال إذن على أنه لأي نظرية من الدرجة الأولى T ذات لغة قابلة للترتيب الجيد ، وأي جملة s في لغة T ،

لو${\displaystyle T\models s}$، ثم${\displaystyle T\vdash s}$.

وبما أن العكس (السلامة) صحيح أيضاً، فإنه يترتب على ذلك أن${\displaystyle T\models s}$إذا وفقط إذا${\displaystyle T\vdash s}$وبالتالي فإن النتيجة النحوية والدلالية متكافئة بالنسبة لمنطق الرتبة الأولى.

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

تم استنتاج الصيغة الأصلية لغودل من خلال أخذ الحالة الخاصة لنظرية بدون أي بديهيات.

نظرية وجود النموذج

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

لو${\displaystyle T}$إذا كان متسقًا نحويًا، فإن${\displaystyle T}$لديه نموذج.

وتقول نسخة أخرى، مرتبطة بنظرية لوفنهايم-سكوليم :

كل نظرية من الدرجة الأولى متسقة نحوياً وقابلة للعد لها نموذج محدود أو قابل للعد.

بناءً على نظرية هينكين، يمكن إثبات نظرية الاكتمال على النحو التالي: إذا${\displaystyle T\models s}$، ثم${\displaystyle T\cup \lnot s}$لا توجد نماذج. وبحسب عكس نظرية هينكين، إذن${\displaystyle T\cup \lnot s}$غير متسق نحوياً. لذا فهو تناقض (${\displaystyle \bot }$) يمكن إثباته من${\displaystyle T\cup \lnot s}$في النظام الاستنتاجي. ومن ثم${\displaystyle (T\cup \lnot s)\vdash \bot }$ثم بناءً على خصائص النظام الاستنتاجي،${\displaystyle T\vdash s}$.

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

يتناقض هذا مع المعنى المباشر لمفهوم النتيجة الدلالية، الذي يحدد كمياً جميع البنى في لغة معينة، وهو ما ليس تعريفاً تكرارياً بشكل واضح.

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

تُظهر نظريات عدم الاكتمال لغودل وجود قيود متأصلة على ما يمكن إثباته ضمن أي نظرية من الدرجة الأولى في الرياضيات. ويشير مصطلح "عدم الاكتمال" في اسمها إلى معنى آخر لكلمة " اكتمال " (انظر نظرية النموذج - استخدام نظريات التراص والاكتمال ): نظرية${\displaystyle T}$تكون كاملة (أو قابلة للتقرير) إذا كانت كل جملة${\displaystyle S}$بلغة${\displaystyle T}$إما أن يكون قابلاً للإثبات (${\displaystyle T\vdash S}$) أو قابلة للدحض (${\displaystyle T\vdash \neg S}$).

تنص نظرية عدم الاكتمال الأولى على أن أي${\displaystyle T}$يجب أن تكون الجملة المتسقة والقابلة للحساب والتي تحتوي على حساب روبنسون (" Q ") غير مكتملة بهذا المعنى، وذلك من خلال بناء جملة صريحة${\displaystyle S_{T}}$ذلك الذي لا يمكن إثباته أو دحضه بشكل قاطع في غضون${\displaystyle T}$تُوسّع نظرية عدم الاكتمال الثانية هذه النتيجة من خلال إظهار أن${\displaystyle S_{T}}$يمكن اختيارها بحيث تعبر عن اتساق${\displaystyle T}$نفسها.

منذ${\displaystyle S_{T}}$لا يمكن إثبات ذلك في${\displaystyle T}$، تنص نظرية الاكتمال على وجود نموذج لـ${\displaystyle T}$في أي${\displaystyle S_{T}}$هذا غير صحيح. في الواقع،${\displaystyle S_{T}}$هي جملة من نوع Π ₁ ، أي أنها تنص على أن خاصية محدودة ما صحيحة لجميع الأعداد الطبيعية؛ لذا إذا كانت خاطئة في نموذج ما، فإن أحد الأعداد الطبيعية في هذا النموذج يُعد مثالًا مضادًا. إذا وُجد هذا المثال المضاد ضمن الأعداد الطبيعية القياسية، فإن وجوده سينفي صحة هذه الخاصية.${\displaystyle S_{T}}$داخل${\displaystyle T}$لكن نظرية عدم الاكتمال أثبتت استحالة ذلك، لذا يجب ألا يكون المثال المضاد عددًا قياسيًا، وبالتالي فإن أي نموذج من${\displaystyle T}$في أي${\displaystyle S_{T}}$خطأ، يجب أن يتضمن أرقامًا غير قياسية .

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

أيضًا، إذا${\displaystyle T}$إذا كانت أقوى قليلاً على الأقل من Q (على سبيل المثال إذا كانت تتضمن الاستقراء للصيغ الوجودية المحدودة)، فإن نظرية تيننباوم تُظهر أنها لا تحتوي على نماذج غير قياسية متكررة.

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

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

وعلى العكس من ذلك، بالنسبة للعديد من الأنظمة الاستنتاجية، من الممكن إثبات نظرية الاكتمال كنتيجة فعالة لنظرية التراص.

يمكن قياس عدم فعالية نظرية الاكتمال من خلال الرياضيات العكسية . عند النظر إليها على لغة قابلة للعد، تكون نظريتا الاكتمال والتراص متكافئتين، ومكافئتين أيضًا لشكل ضعيف من الاختيار يُعرف باسم " ليمة كونيغ الضعيفة" ، حيث يمكن إثبات التكافؤ في RCA _{0 (وهو شكل من أشكال} حساب بيانو من الدرجة الثانية يقتصر على الاستقراء على صيغ Σ ⁰ ₁ ). يمكن إثبات "ليمة كونيغ الضعيفة" في ZF، وهو نظام نظرية مجموعات زيرميلو-فرانكل بدون بديهية الاختيار، وبالتالي يمكن إثبات نظريتي الاكتمال والتراص للغات القابلة للعد في ZF. مع ذلك، يختلف الوضع عندما تكون اللغة ذات عدد عناصر كبير جدًا، فحينها، على الرغم من أن نظريتي الاكتمال والتراص تظلان متكافئتين بشكل قابل للإثبات في ZF، إلا أنهما تصبحان أيضًا متكافئتين بشكل قابل للإثبات لشكل ضعيف من بديهية الاختيار يُعرف باسم "ليمة المرشح الفائق" . على وجه الخصوص، لا يمكن لأي نظرية توسع ZF أن تثبت إما نظرية الاكتمال أو نظرية التراص على لغات عشوائية (ربما غير قابلة للعد) دون إثبات ليمّا المرشح الفائق على مجموعة من نفس العدد.

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

تنص نظرية ليندستروم على أن منطق الرتبة الأولى هو أقوى منطق (مع مراعاة قيود معينة) يحقق كلاً من التراص والاكتمال.

يمكن إثبات نظرية الاكتمال للمنطق الموجه أو المنطق الحدسي فيما يتعلق بدلالات كريپكي .

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

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

• قم بتطبيق نظرية هينكين، من خلال ضمان أنه لكل صيغة${\displaystyle \psi (x)}$هناك ثابت${\displaystyle c_{\psi }}$والمسلمة${\displaystyle \exists _{x}\psi (x)\to \psi (c_{\psi })}$.
• قم بتطبيق ليمّة ليندنبوم للحصول على امتداد كامل.
• قم ببناء نموذج المصطلح المرتبط. ^{[ 4 ]}

قام جيمس مارجيتسون (2004) بتطوير برهان رسمي محوسب باستخدام برنامج إثبات نظرية إيزابيل . ^{[ 5 ]} وهناك براهين أخرى معروفة أيضًا.

• البرهان الأصلي لنظرية غودل في الاكتمال
• نظرية تراختنبروت

• جودل، ك (1929). Über die Vollständigkeit des Logikkalküls (أطروحة). أطروحة دكتوراه. جامعة فيينا.أول برهان لنظرية الاكتمال.
• جودل ، ك (1930). "Die Vollständigkeit der Axiome des logischen Funktionenkalküls". Monatshefte für Mathematik (باللغة الألمانية). 37 (1): 349-360 . دوى : 10.1007 / BF01696781 . جي اف ام 56.0046.04 . S2CID 123343522 .  نفس المادة التي وردت في الرسالة، باستثناء البراهين الموجزة، والشروحات الأكثر إيجازًا، وحذف المقدمة المطولة.
• هانز هيرمس (1973). مقدمة في المنطق الرياضي . سلسلة هوخشولتكست (دار نشر سبرينغر). لندن: سبرينغر. ISBN 3540058192ISSN 1431-4657​​ الفصل الخامس: "نظرية غودل في الاكتمال" .

• موسوعة ستانفورد للفلسفة : " كورت غودل " - بقلم جولييت كينيدي .
• سيرة ماك تيوتور: كورت غودل. مؤرشفة بتاريخ 13 أكتوبر 2005 في أرشيف الإنترنت (Wayback Machine).
• ديتلوف، فيلنيس، وبودنيكس، كارليس، " مقدمة في المنطق الرياضي " .