ההוכחה האונטולוגית של גדל

ממוזער|שמאל|קורט גדל.
**ההוכחה האונטולוגית של גדל** (באנגלית: **Gödel's ontological proof**) היא טיעון לוגי פורמלי לקיומו של האלוהים, אשר נוסח על ידי המתמטיקאי והלוגיקן קורט גדל. הוכחה זו מהווה חוליה בשרשרת שתחילתה בטיעון האונטולוגי של אנסלם מקנטרברי (המאה ה-11), המשכה בשיפורים של רנה דקארט (המאה ה-17) והיא הורחבה משמעותית על ידי גוטפריד לייבניץ (המאה ה-18), שאת גרסתו גדל חקר וניסה להבהיר באמצעות כלים לוגיים מודרניים. גדל נמנע מלפרסם את ההוכחה במהלך חייו מחשש שיחשבו שהוא מאמין דתי אדוק, בעוד שהוא ראה בכך מחקר לוגי גרידא המבקש לבחון אם מערכת אקסיומטית קלאסית יכולה להוביל למסקנה כזו.

## רקע היסטורי והקשר מדעי

ההוכחה האונטולוגית של גדל נשענת על מסורת פילוסופית ארוכה. הטיעון המקורי של אנסלם גרס כי "אלוהים, מעצם הגדרתו כישות שאין גדולה ממנה, חייב להתקיים במציאות ולא רק בהבנה, שכן קיום במציאות גדול יותר מקיום בהבנה בלבד". לייבניץ, במאה ה-18, זיהה חסר בטיעונים של קודמיו וטען כי עליהם להראות תחילה כי מושג ה"ישות המושלמת ביותר" הוא מושג עקבי ואפשרי.

גדל, שהושפע עמוקות מלייבניץ, ביקש להפוך את הטיעון לפורמלי לחלוטין תוך שימוש בלוגיקה מודאלית מסדר גבוה. מעבר לעבודתו הלוגית-פילוסופית, גדל עסק רבות גם בפיזיקה ותורת היחסות, שם הציע מודלים קוסמולוגיים של "יקום מסתובב".

### "ניסוי הטיל" המחשבתי והקשר לקוסמולוגיה
בהקשר של עבודתו הקוסמולוגית (ולא ישירות בתוך ההוכחה האונטולוגית הלוגית), גדל הציע מודל פיזיקלי המאפשר מסע בזמן. הוא העריך כי באמצעות "סבב בתוך ספינת טיל (rocket ship) במסלול רחב מספיק", ניתן להגיע לכל אזור בעבר, בהווה או בעתיד. גדל אף ביצע הערכה גסה של המהירות הנדרשת לטיל כזה ושל כמות הדלק הדרושה למסע. ניסוי מחשבתי זה נועד להראות כי מבנה הזמן והמרחב ביקום מאפשר פתרונות שבהם הזמן מאבד את כיוונו הייחודי, דבר המעניק לזמן אופי "גאומטרי" בדומה למרחב. אף שזהו מחקר פיזיקלי, הוא משקף את גישתו הכוללת של גדל לחיפוש אחר אמיתות אובייקטיביות במערכות פורמליות, בין אם בלוגיקה ובין אם בפיזיקה.

## מבנה ההוכחה הפורמלית

ההוכחה מבוססת על הגדרת "תכונות חיוביות" (positive properties). גדל אינו מגדיר מהי תכונה חיובית באופן מהותי, אלא קובע מערכת אקסיומות עבורן.

### אקסיומות והגדרות יסוד
# אקסיומה 1: עבור כל תכונה, או שהיא חיובית או ששלילתה חיובית, אך לא שתיהן (כלומר P(\neg \phi) \leftrightarrow \neg P(\phi)).
# אקסיומה 2: תכונה הנובעת בהכרח מתכונה חיובית היא בעצמה חיובית.
# הגדרה 1 (דמוי-אל): ישות x היא "דמוית-אל" (God-like) אם ורק אם היא מחזיקה בכל התכונות החיוביות.
# אקסיומה 3: התכונה של להיות דמוי-אל היא חיובית בעצמה.
# אקסיומה 4: תכונה חיובית היא חיובית באופן הכרחי.
# הגדרה 2 (מהות): תכונה \phi היא המהות (Essence) של x אם x מחזיק ב-\phi, ו-\phi גוררת בהכרח את כל שאר התכונות של x.
# הגדרה 3 (קיום הכרחי): ישות x קיימת באופן הכרחי אם כל מהות שלה ממומשת בהכרח (כלומר, קיימת בכל עולם אפשרי).
# אקסיומה 5: קיום הכרחי הוא תכונה חיובית.

### משפטים מרכזיים
* משפט 1: כל תכונה חיובית היא עקבית לוגית (כלומר, ייתכן שיש ישות המחזיקה בה).
* משפט 2: אם ישות היא דמוית-אל, אזי התכונה של להיות דמוית-אל היא המהות של אותה ישות.
* משפט 3: בהכרח, קיימת ישות דמוית-אל.

## ביקורת וניתוח לוגי

הביקורת המפורסמת ביותר על ההוכחה הועלתה על ידי ג'ורדן הווארד סובל, אשר הראה כי האקסיומות של גדל חזקות מדי ומובילות למה שמכונה קריסה מודאלית (Modal Collapse).

### קריסה מודאלית
סובל הוכיח כי במערכת של גדל, כל טענה שהיא אמת היא בהכרח אמת (p \equiv \Box p). המשמעות הפילוסופית של קריסה זו היא ביטול האפשרות של בחירה חופשית או מקרים של "מקריות" (contingency) בעולם, שכן הכל הופך להכרחי. קריסה זו נובעת מהשילוב של אקסיומה 1 (הקובעת שכל אמת היא תכונה חיובית במובן מסוים) והגדרת ה"אל" כמי שמחזיק בכל התכונות הללו.

### תיקוני אנדרסון (Emendations)
הפילוסוף  הציע גרסה מתוקנת להוכחה המנסה להתחמק מהקריסה המודאלית. אנדרסון שינה את הגדרת ה"מהות" ואת הגדרת הישות הדמוית-אל, כך שהיא מחזיקה בתכונות חיוביות באופן הכרחי בלבד, ולא בכל תכונה חיובית שהיא. תיקונים אלו הופכים את המערכת לעקבית עם קיומן של אמיתות מקריות, ובכך "מצילים" את ההוכחה מהביקורת של סובל.

## אוטומציה של ההוכחה

בשנים האחרונות, התקדמות בתחום הבינה המלאכותית ומוכיחי משפטים ממוחשבים אפשרה לאמת את ההוכחה של גדל באופן אוטומטי.

החוקרים כריסטוף בנצמילר וברונו וולצנלוגל פלאו השתמשו במוכיחי משפטים מסדר גבוה כגון LEO-II ו-Satallax כדי לאמת את השרשרת הלוגית של גדל (בגרסת דנה סקוט). המחשב אישר כי המסקנה "בהכרח קיים אל" אכן נובעת מהאקסיומות, אך גם אימת את טענת הקריסה המודאלית של סובל. בנוסף, המחשב גילה כי הלוגיקה המודאלית KB מספיקה להוכחה, ואין צורך במערכת החזקה יותר S5, כפי שחשבו בעבר.

## סיכום וחשיבות

ההוכחה האונטולוגית של גדל מייצגת ניסיון נועז לגשר בין מטפיזיקה לבין דיוק מתמטי קר. בעוד שהאקסיומות עצמן נותרות שנויות במחלוקת פילוסופית, המבנה הלוגי של ההוכחה נמצא תקף ואף הוכח ככזה על ידי מערכות חישוביות מודרניות. גדל עצמו ראה בעולם המושגים המתמטיים ישויות אובייקטיביות הקיימות ללא תלות בבני האדם, וגישתו זו ("פלאטוניזם") היא שעמדה בבסיס אמונתו כי ניתן להוכיח אמיתות רוחניות באמצעים לוגיים.

## ראו גם
* הגיונות על הפילוסופיה הראשונית
* לוגיקה מודאלית
* קורט גדל
* הטיעון האונטולוגי
* יקום גדל

## לקריאה נוספת

* Sobel, Jordan Howard (2004). *Logic and Theism: Arguments For and Against Beliefs in God*. Cambridge University Press.
* Fitting, Melvin (2002). *Types, Tableaus, and Gödel’s God*. Kluwer Academic Publishers.
* Gödel, Kurt (1995). *Collected Works, Volume III: Unpublished Essays and Lectures*. Oxford University Press.

## הערות שוליים

קטגוריה:לוגיקה
קטגוריה:פילוסופיה
קטגוריה:טיעונים לקיום אלוהים