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