פורמליזם (בעברית: הצרנה) הוא שיטה ועמדה לגבי מהות המתמטיקה. הצרנה היא כתיבה של טענות מתמטיות באמצעות סמלים וחוקים בלבד, בלי התייחסות למשמעות חיצונית. לפי הפורמליזם, ניתן לבדוק טענות על ידי הפעלת כללי ההסקה בצורה מכנית.
כמשיטה, הפורמליזם מתמקד במערכת המשוואות, הסמלים וחוקי ההסקה שבאמצעותם מציגים תיאוריה מתמטית. אם יודעים להצרין רישום של הוכחה, אפשר לאמת את תקינותה באופן מכני. זו לא תמיד הדרך הנוחה להוכחות חדשות, אך היא טובה לאישור הוכחות קיימות ולחיפוש הוכחות בעזרת מחשב.
השימוש המוכר ביותר הוא בהצרנת טענות לוגיות כדי לבדוק את המבנה והתוקף שלהן. השיטה שימושית גם בבחינות בדומה לפסיכומטרי, שם בודקים טיעונים לוגיים.
שאלה: "אם ירד גשם, רוני ייקח מטרייה." איזו מהאמירות שקולה לכך?
אם נסמן "ירד גשם" ב-R ו"רוני ייקח מטרייה" ב-U, הנוסחה היא R → U (R גורר U). האפשרויות נצרות כך:
1) U
2) ¬R → ¬U (אם לא ירד גשם אז לא ייקח מטרייה)
3) ¬R → U
4) ¬U → ¬R (אם רוני לא יקח מטרייה אז לא ירד גשם)
רק האפשרות הרביעית שקולה בהיגיון ל-R → U. ניתן לאמת זאת גם בעזרת טבלת אמת, כלי שמראה מתי נוסחה לוגית נכונה.
שורש הרעיון הוא ששינויים מסוימים בטיעון יכולים ליצור טענה שקולה. לדוגמה, הפיכת צדדים, הוספת או הסרת המילה "רק", והפיכת טענות לחיוביות או שליליות. אם עושים שתי פעולות כאלה, לעתים מתקבלת טענה שקולה.
אם a גורר את b ו-b גורר את c, אז a גורר את c. זה כלל פשוט של היסק לוגי.
דויד הילברט טען שהמתמטיקה היא אוסף הנוסחאות והאקסיומות בלבד. כלומר, עצמים מתמטיים מוגדרים רק על פי האקסיומות שהם מקיימים. הילברט רצה להעניק ודאות ושלמות למתמטיקה על ידי ניסוח אקסיומות מושלם.
מאוחר יותר קורט גדל הוכיח את משפטי האי-שלמות שלו. גדל הראה שאי אפשר לבנות תורה אקסיומטית שלמה ועקבית עבור האריתמטיקה. כלומר, יהיו תמיד טענות שאי-אפשר להוכיח או להפריך במסגרת האקסיומות. הממצא הזה שיבש את תוכניתו של הילברט.
למרות כישלונו כעמדה פילוסופית כוללת, הפורמליזם פרח כשיטת עבודה. הוא נותר חלק חשוב מתרבות המתמטיקה, ובעיקר בכלים למעקב, בדיקה ומיכון של הוכחות.
פורמליזם (הצרנה) אומר לכתוב מתמטיקה בסמלים. סמלים הם אותיות ומשפטים קצרים.
הרעיון הוא להציג טענות עם חוקים ברורים. כך אפשר לבדוק אותן בצעד אחר צעד. מחשבים יכולים לעזור למצוא או לבדוק הוכחות.
אמירה: "אם יורד גשם, רוני ייקח מטרייה." נסמן R = יורד גשם, U = רוני ייקח מטרייה. הנוסחה היא R → U.
האפשרות ששקולה לה היא: "אם רוני לא יקח מטרייה, אז לא ירד גשם." זו התשובה הנכונה.
אפשר לשנות משפטים בדרכים שונות ולפעמים להשיג משפט שקול. לדוגמה לשנות משפט לשלילי או להוסיף את המילה "רק".
דויד הילברט רצה שהמתמטיקה תהיה רק מערכת חוקים ברורה. אבל המתמטיקאי קורט גדל הראה שלא אפשר להוכיח הכל בתוך מערכת כזו. כלומר תמיד יהיו משפטים שאי־אפשר להוכיח.
למרות זה, פורמליזם שימושי לעבודת בדיקה. הוא עוזר לאמת הוכחות ולמצוא טעויות.
תגובות גולשים