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