בתשובה לאלון עמית, 15/07/05 18:00
מינוס אחת 317098
לא הבנתי משהו. הנוסחה המתוארת את "X הוא אקסיומה" יכולה להיות בעלת אורך אינסופי? כי הרי יש אינסוף אקסיומות, ולכן אם תכתוב נוסחה בסגנון "X שווה 1 או X שווה 2 או..." לא תגמור אף פעם.
מינוס אחת 317102
בגלל זה דרשנו שאוסף האקסיומות יהיה אפקטיבי: יש אלגוריתם סופי (= נוסחה סופית) המכריע אם נוסחה נתונה היא אקסיומה. גם אם יש אינסוף אקסיומות, יש תכנית מחשב קצרה ופשוטה המזהה אותן.

למשל, ב-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 הוא הקוד של אקסיומה כזו.
מינוס אחת 317106
לא. דרישת האפקטיביות היא בדיוק שניתן לכתוב נוסחה סופית שאומרת "X הוא אקסיומה" ו"X הוא היסק תקף".

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

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