אינטואיציוניזם

אינטואיציוניזם הוא גישה בפילוסופיה של המתמטיקה הרואה במתמטיקה בנייה מנטלית של האדם.
רק טענות שניתן לבנות מהאקסיומות נחשבות לגיטימיות. אקסיומות = הנחות בסיס שלא מוכחות.
ההוכחות המותרות הן קונסטרוקטיביות, כלומר הן מראיות כיצד לבנות את האובייקט שמתקבל.
בשל כך דוחים האינטואיציוניסטים הוכחות על דרך השלילה ואת כלל השלישי מן הנמנע.
מייסד הגישה הוא ל.א.י. בראואר. מתמטיקאים חשובים נוספים: ארנד הייטינג, אנדריי קולמוגורוב והרמן וייל.

הרעיונות האינטואיציוניסטיים שורשם בחשיבה של קאנט. קאנט ראה את המתמטיקה כחלק מהצורה שבה אנו תופסים זמן וחלל.
בראואר קיבל את הרעיון שהמתמטיקה מנטלית, אך בחר לבסס אותה בעיקר על מושג המספר הטבעי.
לכן בבסיס האינטואיציוניזם עומדים המספרים הטבעיים בלבד, והבניות מתבצעות אינדוקטיבית.

לאינטואיציוניסטים אמת מתמטית היא יחס קונסטרוקטיבי: אמת משמעה שיש בנייה או הוכחה שמראה זאת.
"לא P" מובן כהצגה שבכל הוכחה ל-P אפשר להפיק סתירה. משמעות זו שונה מההבנה בקלאסיקה.
מכאן שיש אסימטריה בין טענות חיוביות ושליליות, וכלל השלישי (P או לא P) אינו מחויב תמיד.
כתוצאה מכך הלוגיקה משתנה, ונולדת הלוגיקה האינטואיציוניסטית שמגבילה שיטות הוכחה מסוימות.

האינטואיציוניזם מבדיל בין אינסוף פוטנציאלי לאינסוף אקטואלי.
אינסוף פוטנציאלי = תהליך שיכול להמשיך תמיד, כמו ספירה 1,2,3,...
אינסוף אקטואלי = אוסף שהוא שלם וכולל את כל האיברים בו, כמו "קבוצת כל המספרים".
בתורת הקבוצות הקלאסית יש התייחסות לאינסוף אקטואלי, כמו בעבודתו של קנטור ובמסגרת ZFC.
האינטואיציוניסטים מקבלים רק אינסוף פוטנציאלי; הם דוחים את ההתייחסות ל"קבוצה אקטואלית" של כל הממשיים.
פיניטיזם היא צורת קיצון שאפילו את האינסוף הפוטנציאלי אינה מקבלת.

דחיית הוכחות בדרך השלילה שינתה את המתמטיקה שנבנתה באינטואיציוניזם.
בהתחלה נדמה היה שהמתמטיקה האינטואיציוניסטית תהיה מצומצמת יותר.
עם הזמן נראו משפטים שונים שהקלאסיקות אינן מקבלות, והמצב הבלתי תלוי בין המערכות התבהר.

האינטואיציוניסטים ניסחו פירוש של מה נחשבת הוכחה אינטואיציוניסטית. פירוש זה נקרא פירוש BHK.
בעיקרו הוא קובע מה פירוש להוכיח ביטויים לוגיים:
- הוכחה ל"A וגם B" צריכה לכלול הוכחה ל-A והוכחה ל-B.
- הוכחה ל"A או B" צריכה לכלול הוכחה לאחד מהם, A או B.
- הוכחה ל"אם A אז B" היא דופן שמשמעה: כל הוכחה ל-A מובילה להוכחה ל-B.
- הוכחה ל"לא A" מראה שכל הוכחה ל-A גוררת סתירה.
- הוכחה ל"קיים x כך ש-A(x)" דורשת לתת דוגמה ספציפית ולהוכיח A עבורה.
- הוכחה ל"לכל x מתקיים A(x)" היא בנייה שהופכת כל אלמנט לראיה לכך ש-A מתקיים.
יש גם הבהרה לגבי הוכחות של טענות אטומיות כ'בניות' מתמטיות.

בקורתית לאינסוף האקטואלי, האינטואיציוניסטים מניחים את קיומם של המספרים הטבעיים כאקסיומה.
הם מקבלים שיטות אינדוקטיביות, ולרבות אינדוקציה במתכונת דומה לזו של פאנו בגרסאות מאוחרות.
עבור טענות על מספרים טבעיים, רוב המשפטים הקלאסיים נשארים בתוקף.

כדי להגדיר ממשיים, בראואר הציע את רעיון "סדרות הבחירה" (choice sequences).
אלה סדרות שרצף האיברים שלהן נקבע לפי כלל או לפי בחירה חופשית.
באמצעותן ניתן להגדיר מספרים ממשיים בלי לדבר על "קבוצת כל הממשיים" כאובייקט שלם.
תוצאה משמעותית היא כי בבניית בראואר כל פונקציה שמוכיחה שהיא מוגדרת על קטע, היא רציפה על קטע זה.
זהו הבדל מהותי מול המתמטיקה הקלאסית, שבה קיימות פונקציות מוגדרות אך לא רציפות.
בראואר הוכיח את הטענה הזו בשנת 1923 בעזרת האופי האלגוריתמי של ההגדרות האינטואיציוניסטיות.

אינטואיציוניזם אומר שמתמטיקה היא בנייה שעושים אנשים בראשם.
אם לא ניתן לבנות דבר זה לא נחשב אמיתי במתמטיקה הזו.
מייסד התנועה הוא ל.א.י. בראואר. גם הייטינג וקולמוגורוב עבדו על זה.

האינטואיציוניסטים מייחסם חשיבות למספרים הטבעיים: 1,2,3,...
מספרים אלה נתפסים כבסיס שאפשר לספור ממנו הלאה.

"אמת" כאן אומרת שיש דרך לבנות או להראות אותה בפועל.
"לא P" פירושו: אם מנסים להוכיח P זה יגרום לסתירה.
לכן לפעמים אי אפשר להחליט אם P או לא P.

יש שני רעיונות לאינסוף. אינסוף פוטנציאלי הוא תהליך שנמשך תמיד, כמו ספירה.
אינסוף אקטואלי הוא "קבוצה של כל האיברים" בו זמנית.
האינטואיציוניסטים מקבלים רק את האינסוף הפוטנציאלי.

יש כללים חדשים למה נחשב הוכחה:
- כדי להוכיח "A וגם B" צריך הוכחה לשניהם.
- כדי להוכיח "A או B" צריך להראות מי מהם נכון.
- כדי להוכיח "אם A אז B" צריך להפוך הוכחה של A להוכחה של B.
- כדי להוכיח "קיים x" צריך לתת דוגמה ממשית.

המספרים הטבעיים נחשבים קיימים מהתחלה.
שיטות כמו אינדוקציה מקובלות, ולכן הרבה משפטים מוכרים נכונים כאן גם כן.

בראואר הציע לבנות מספרים ממשיים כסדרות של בחירות.
כך אפשר לדבר על מספרים ממשיים בלי לומר שיש "את כל הממשיים" בבת אחת.
באינטואיציוניזם, כל פונקציה שמוכחים שהיא מוגדרת על קטע היא גם רציפה.
זה שונה מהמתמטיקה הרגילה, שבה יש פונקציות לא רציפות.