עצמאות (לוגיקה מתמטית) – הבדלי גרסאות
תוכן שנמחק תוכן שנוסף
אין תקציר עריכה |
|||
שורה 1:
ב[[לוגיקה מתמטית]], טענה שאפשר [[הוכחה פורמלית|להוכיח]] אותה או את שלילתה מתוך [[תורה (לוגיקה מתמטית)|מערכת]] נתונה של [[אקסיומה|אקסיומות]], היא טענה '''בת הכרעה'''. טענה שאי אפשר להוכיח לא אותה ולא את שלילתה, היא '''לא בת הכרעה'''.
ישנן כמה דוגמאות מפורסמות לבעיות לא בנות הכרעה:
[[קטגוריה:חישוביות]]▼
* [[אקסיומת המקבילים]] הקובעת שדרך כל נקודה מחוץ לישר עובר קו מקביל אחד ויחיד - אינה בת הכרעה במסגרת ה[[אקסיומה|אקסיומות]] האחרות של [[גאומטריית המישור]] (וראו גם [[גאומטריה לא אוקלידית]]).
* [[אקסיומת הבחירה]] אינה בת הכרעה במסגרת האקסיומות הרגילות של [[תורת הקבוצות האקסיומטית|תורת הקבוצות]], [[אקסיומות צרמלו פרנקל]].
* [[השערת הרצף]] אינה בת הכרעה במסגרת של [[אקסיומות צרמלו פרנקל]] יחד עם [[אקסיומת הבחירה]].
המתמטיקאי ה[[אוסטריה|אוסטרי]]-[[ארצות הברית|אמריקאי]] [[קורט גדל]] הוכיח ב-[[1931]] שבכל [[תורה (לוגיקה מתמטית)|תורה]] [[תורה אפקטיבית|אפקטיבית]] [[עקביות (לוגיקה מתמטית)|עקבית]] המבוססת על [[שפה מסדר ראשון]] שיש בה מספיק מושגים כדי לנסח טענות על כפל במספרים השלמים, יש נוסחאות שאינן בנות הכרעה. מכאן ששפה אפקטיבית חזקה מספיק, אינה יכולה להיות עקבית ו[[שלמות (לוגיקה מתמטית)|שלמה]]. חוק זה נקרא [[משפט אי השלמות של גדל]], ובעקבותיו השתנתה ההתייחסות לתוכנית של [[דויד הילברט]] לבסס את כל ה[[מתמטיקה]] על [[קבוצה סופית]] של אקסיומות.
משפט אי-השלמות השני של גדל טוען שלא ניתן להוכיח את העקביות של תורה (אפקטיבית וחזקה מספיק) במסגרת האקסיומות של התורה עצמה. לפעמים אפשר להוכיח את העקביות של מערכת על-ידי בניית [[מודל (לוגיקה מתמטית)|מודל]] שלה במסגרת מערכת אחרת. למשל, [[אקסיומות פאנו]] מתארות את המספרים השלמים, וניתן לבנות מודל שלהן במסגרת תורת הקבוצות. לכן, אם תורת הקבוצות חסרת סתירות, אז כך גם מערכת פאנו.
[[en:Decidability (logic)]]
| |||