תורת החישוביות/משפט הרקורסיה: הבדלים בין גרסאות בדף

תוכן שנמחק תוכן שנוסף
Gran (שיחה | תרומות)
Gran (שיחה | תרומות)
שורה 110:
 
אנחנו אומרים שניתכן להוכיח את הטענה <math>S</math> ע״י המערכת F אם <math>S</math> היא אקסיומה בעצמה, או אם ניתן להסיק את הטענה S מתוך האקסיומות וכללי ההיסק. מסמנים <math>F \vdash S</math> (S יכיחה ב־F).
'''הוכחה''' היא למעשה מחרוזת שמסבירה איך מסיקים את 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.
 
נאמר שמערכת F היא: