תורת החישוביות/משפט הרקורסיה: הבדלים בין גרסאות בדף
תוכן שנמחק תוכן שנוסף
שורה 107:
====מערכת הוכחה====
מערכת הוכחה F היא קבוצה של אקסיומות "Axiom" וקבוצה של כללי היסק לוגיים "Rules". דוגמא לאקסיומה יכולה להיות "היום יום ראשון". ודוגמא לכלל היסק לוגי יכול להיות "אם טענה A גוררת את טענה B, וגם ידוע ש־A טענה נכונה, אז גם B טענה נכונה" ([[w:מודוס
* אנחנו אומרים
* '''הוכחה''' היא למעשה מחרוזת שמסבירה איך מסיקים את S מתוך האקסיומות וכללי ההיסק. <sub>(הוכחה סתמית לדוגמא יכולה להראות כך: "קח את האקסיומה הראשונה והשניה, הפעל עליהם את כלל ההיסק השלישי ותקבל טענה <math>S_1</math>. הפעל את כלל ההיסק החמישי על <math>S_1</math> ותקבל טענה <math>S_2</math>. הפעל את כלל ההיסק השלישי על <math>S_2</math> ועל האקסיומה החמישית, ותקבל את <math>S</math>")</sub>
* חשוב לציין שבהנתן טענה (מחרוזת S) והוכחה (מחרוזת x) קל לוודא האם x היא הוכחה ל־S. כלומר קיימת מ״ט שעל קלט <math>(S,x)</math> עוצרת ועונה כן/לא בהתאם להאם x היא הוכחה של S. ▼
▲חשוב לציין שבהנתן טענה (מחרוזת S) והוכחה (מחרוזת x) קל לוודא האם x היא הוכחה ל־S. כלומר קיימת מ״ט שעל קלט <math>(S,x)</math> עוצרת ועונה כן/לא בהתאם להאם x היא הוכחה של S.
נאמר שמערכת F היא:
# '''עקבית''': כאשר לא קיימת טענה S כך ש־<math>F\vdash S</math> וגם <math>F \vdash \neg S</math>
# '''שלמה''': אם לכל טענה S, או
משמעות העקביות היא שלא ניתן להוכיח טענות "שגויות". אם ניתן להוכיח טענה וגם היפוכה, המערכת מאבדת את ההגיון שבה, כי ניתן להוכיח בעזרה ששקר(False) הוא טענת-אמת (<math>F\vdash False</math>), ומכאן ניתן להוכיח כל טענה (כי <math>False \Rightarrow S</math> הוא טענת אמת).
| |||