לוגיקה מתמטית

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

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

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

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

• תורת הקבוצות
• תורת המודלים
• תורת הרקורסיה
• תורת ההוכחות

ראו גם

• תחשיב הפרדיקטים
• תחשיב פסוקים
• שפה מסדר ראשון
• שפה מסדר שני

קישורים חיצוניים

• עזריאל לוי, דניאלה ליבוביץ, שמואל ברגר, לוגיקה מתימטית, יחידות 1-5, הוצאת האוניברסיטה הפתוחה
• סטיבן בילאניוק, A Problem Course in Mathematical Logic, אוניברסיטת טרנט, קנדה.
• בועז צבאן, מבוא ללוגיקה מתמטית, המחלקה למתמטיקה, אוניברסיטת בר-אילן, הספר מכיל רקע ותרגילים לנושא תחשיב הפסוקים ולוגיקה מסדר ראשון. נכתב במקור על פי מערכי שיעורים של פרופסור חיים יהודה.
• Metamath Proof Explorer: מאגר של משפטים מתמטיים עם הוכחות מלאות בעזרת לוגיקה מתמטית.