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