בתשובה לאיזור חסר אגו במוחו של אלון עמית, 03/01/10 5:58
שיבושם לך 532732
חידוד קטן: אין בעיה להגדיר "מערכת הוכחה" עבור לוגיקה מסדר שני - למשל, רמאות קטנה שנקראת "הוכחה סמנטית", שבה אומרים שקבוצת פסוקים א' מוכיחה את הפסוק ב' אם כל מודל ל-א' הוא מודל לב' (כלומר, א' גורר סמנטית את ב'). כמובן שזו מערכת הוכחה חסרת כל ערך, אבל מבחינה הגדרתית היא לגיטימית. הבעייתיות הרלוונטית במערכת הזו היא שזו לא מערכת *אפקטיבית*, כלומר דרישת האפקטיביות (שהיא הרי קריטית אצל גדל) היא מה שנכשל הפעם, ולא השלמות (אני רואה את גדל כמעין משפט Trade-off - אי אפשר להיות בו זמנית גם שלמים, גם עקביים וגם אפקטיביים).

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

חזרה לעמוד הראשי המאמר המלא

מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים