שינויים
/* הוכחה */
== הוכחה ==
=== מודוס פוננס === '''הוכחה פורמלית''' של פסוק P היא רצף של פסוקים <math>\ P_1,\dots,P_n</math> שכל אחד מהם הוא או אקסיומה, או שאפשר לגזור אותו באופן פורמלי מפסוקים קודמים: אם <math>\ P_k</math> אינו אקסיומה, צריכים להיות קיימים <math>\ i,j</math> כך ש- <math>\ P_k = P_i \rightarrow P_j</math>. הגזירה מתבססת כאן על הכלל הלוגי היסודי הנקרא '''מודוס פוננס''': מ-<math>\ P\rightarrow Q</math> ו-P אפשר לגזור (כלומר להסיק את) Q. בלימודי המתמטיקה תפגשו הוכחות פורמליות לעתים נדירות ביותר. בדרך כלל מסתפקים בהוכחה מדוקדקת שאמנם אינה פורמלית, אבל '''אפשר לתרגם אותה להוכחה פורמלית'''. בכל שלב מהותי של ההוכחה תוכלו לזהות שמגיעים אל המסקנה מתוך שתי עובדות שהוכחו קודם לכן: ההנחה, והטענה שההנחה גוררת את המסקנה. === הוכחת טענות מכומתות === פסוק ללא כמתים אפשר להוכיח באמצעות טבלת אמת. כל הפסוקים מסוג זה נחשבים לאמיתות טריוויאליות, ולכן הם נמצאים בשכבה הראשונה של מאגר האקסיומות. את ההוכחה של פסוקים מורכבים יותר אפשר לתפוס כמשחק בין שני צדדים: ה"מוכיח", וה"יריב".* כדי להוכיח טענה מהסוג <math>\ \forall x: P(x)</math>, על המוכיח להראות את אמיתות הטענה <math>\ P(x)</math>, וזאת לכל x *שבחר היריב*. היריב עשוי לבחור x שעבורו הוכחת הטענה קשה יותר. למוכיח אסור לבחור את x בעצמו, משום שהוא צריך להוכיח את הטענה '''לכל x'''.* כדי להוכיח טענה מהסוג <math>\ \exists x: P(x)</math>, המוכיח צריך להראות את אמיתות הטענה <math>\ P(x)</math> עבור x כלשהו. הדרך הקלה והבטוחה ביותר לעשות זאת היא *להצביע* על x שעבורו הטענה נכונה; זוהי '''הוכחה קונסטרוקטיבית'''. יש גם הוכחות לא קונסטרוקטיביות, אבל בשלבי הלימודים הראשונים תתקלו בהן רק לעתים רחוקות. בדרך כלל המשחק כולל יותר משלב אחד. למשל, כדי להוכיח "לכל x חיובי קיים y חיובי הקטן ממנו", עלינו לאפשר ליריב לבחור x כרצונו; אחר-כך עלינו להראות שקיים y הקטן מן ה-x הזה, וזאת נעשה על-ידי בחירת y מתאים (למשל: <math>\ y = x/2</math>). אפשר לכתוב זאת כך: * יהי <math>\ x>0</math> (היריב בוחר x כרצונו). נבחר <math>\ y = x/2</math>, ואז <math>\ 0<y<x</math> (כאן אנו מראים שעבור y שבחרנו, הטענה אכן מתקיימת). להלן כמה טכניקות הוכחה שכיחות. * "'''מספיק להוכיח ש-'''": לפעמים הדרך הקצרה ביותר להוכיח טענה מסויימת היא הוכחת טענה חזקה יותר. זהו שימוש ישיר במודוס פוננס: במקום להוכיח את Q, אנו מוכיחים את P, כאשר הטענה <math>\ P\rightarrow Q</math> ידועה מראש. למשל, כדי להוכיח "קיים מספר ראשוני הגדול מ-<math>\ 10^{4300}</math>, מספיק להוכיח שקיימים אינסוף ראשוניים".* '''הוכחה בדרך השלילה''' מבוססת על הטאוטולוגיה <math>\ ((\neg P)\rightarrow F) \leftrightarrow P</math>. כדי להוכיח את P, אנו מניחים את לא-P, ומראים שההנחה הזו מביאה לסתירה. '''הפרכה''' של טענה אינה אלא הוכחה שהטענה אינה נכונה. הדוגמא החשובה ביותר היא '''הפרכה על-ידי דוגמא נגדית''': * כדי להפריך את הטענה <math>\ \forall x: P(x)</math>, יש להראות שקיים x שעבורו הטענה <math>\ P(x)</math> אינה נכונה.
== שגיאות נפוצות ==
