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