בתשובה לגדי אלכסנדרוביץ', 15/07/05 18:05
מינוס אחת 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 הוא הקוד של אקסיומה כזו.

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

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