 |
בגלל זה דרשנו שאוסף האקסיומות יהיה אפקטיבי: יש אלגוריתם סופי (= נוסחה סופית) המכריע אם נוסחה נתונה היא אקסיומה. גם אם יש אינסוף אקסיומות, יש תכנית מחשב קצרה ופשוטה המזהה אותן.
למשל, ב-PA יש אינסוף אקסיומות:
1. אם הטענה x=x נכונה כש-x=0, ואם נכונות הטענה הזו כש-x=n גוררת את נכונותה כש=x=n+1, אז הטענה x=x נכונה לכל מספר טבעי.
2. אם הטענה x=x+1 נכונה כש-x=0, ואם נכונות הטענה הזו כש-x=n גוררת את נכונותה כש=x=n+1, אז הטענה x=x+1 נכונה לכל מספר טבעי.
3. אם הטענה "2x הוא קטן מארבע או שהוא סכום של שני ראשוניים" נכונה כש-x=0, ואם נכונות הטענה הזו כש-x=n גוררת את נכונותה כש=x=n+1, אז הטענה "2x הוא קטן מארבע או שהוא סכום של שני ראשוניים" נכונה לכל מספר טבעי.
...
כולן זהות, פרט לנוסחה P בעלת משתנה חופשי x המופיעה בהן. לא קשה לכתוב תכנית שתדע לומר אם מחרוזת מסויימת היא אחת האקסיומות בסכימה הזו, ואח"כ אפשר לכתוב *נוסחה* שתהיה נכונה ל-X אם"ם X הוא הקוד של אקסיומה כזו.
|
 |
RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש