שינויים
/* מודוס פוננס */
=== מודוס פוננס ===
'''הוכחה פורמלית''' של פסוק P היא רצף של פסוקים <math>\ P_1,\dots,P_n</math> שכל אחד מהם הוא או אקסיומה, או שאפשר לגזור אותו באופן פורמלי מפסוקים קודמים: אם <math>\ P_k</math> אינו אקסיומה, צריכים להיות קיימים <math>\ i,j<k</math> כך ש- <math>\ P_k = P_i \rightarrow P_j</math>.
הגזירה מתבססת כאן על הכלל הלוגי היסודי הנקרא '''מודוס פוננס''': מ- <math>\ P\rightarrow Q</math> ו- <math>P</math> אפשר לגזור (כלומר להסיק את) <math>Q</math>.
