תורת החישוביות/משפט הרקורסיה: הבדלים בין גרסאות בדף

תוכן שנמחק תוכן שנוסף
Gran (שיחה | תרומות)
מ ←‏משפט הרקורסיה: בדוגמאות הקידוד מופיע לפני הקלט
Gran (שיחה | תרומות)
שורה 104:
 
===משפט האי־שלמות של גדל===
בעבר, חשבו שיש ביכולת המתמטיקה להוכיח כל '''טענה''' שהיא "נכונה" (או להפריך טענה שגויה, כלומר להוכיח שהטענה ההפכית היא נכונה). משפט האי-שלמות (הראשון) של גדל שם קץ לדרך מחשבה זו והראה שבכל מערכת הוכחה חזקה דיו, תמיד יהיו טענות שלא ניתן להוכיח לא אותן ולא את ההופכי שלהן. בחלק זה נראה הוכחה פשוטה יחסית למשפט אי השלמות של גדל, המבוסס על משפט הרקורסיה. השלב המסובך בהוכחה הוא דווקא שלב ההגדרות: מהי "מערכת הוכחה חזקה דיו" מהי "טענה" ומה הכוונה להאם הטענה נכונה או לא. מכיוון שעיקר הפרק הוא לעסוק במשפט הרקורסיה, לא נהיה מדוייקים לחלוטין בנושא ההגדרות, ויש חלקים שישארו עמומים במכוון.
 
====מערכת הוכחה====
מערכת הוכחה F היא קבוצה של אקסיומות "Axiom" וקבוצה של כללי היסק לוגיים "Rules". דוגמא לאקסיומה יכולה להיות "היום יום ראשון". ודוגמא לכלל היסק לוגי יכול להיות "אם טענה A גוררת את טענה B, וגם ידוע ש־A טענה נכונה, אז גם B טענה נכונה" (מודוס פונוס).
 
אנחנו אומרים שניתכן להוכיח את הטענה <math>S</math> ע״י המערכת F אם <math>S</math> היא אקסיומה בעצמה, או אם ניתן להסיק את הטענה S מתוך האקסיומות וכללי ההיסק. מסמנים <math>F \vdash S</math> (S יכיחה ב־F).
 
נאמר שמערכת F היא:
# '''עקבית''': כאשר לא קיימת טענה S כך <math>F\vdash S</math> וגם <math>F \vdash \neg S</math>
# '''שלמה''': אם לכל טענה S, או ש<math>F \vdash S</math> או ש<math>F\vdash \neg S</math>
 
משמעות העקביות היא שלא ניתן להוכיח טענות "שגויות". אם ניתן להוכיח טענה וגם היפוכה, המערכת מאבדת את ההגיון שבה, כי ניתן להוכיח בעזרה ששקר(False) הוא טענת-אמת (<math>F\vdash False</math>), ומכאן ניתן להוכיח כל טענה (כי <math>False \Rightarrow S</math> הוא טענת אמת).
 
משמעות השלמות היא שכל טענה היא או "נכונה" או "שקרית" כלומר, ניתן הוא להוכיח אותה, או להוכיח את שלילתה.
 
{{משפט|שם=משפט האי-שלמות הראשון של גדל|
תוכן= לכל מערכת הוכחה F חזקה דיו ועקבית, F אינה שלמה.{{רווח קשיח|5}}}}
 
{{להשלים}}