לוגיקה מתמטית
מתוך ויקיפדיה, האנציקלופדיה החופשית
לוגיקה מתמטית הוא תחום במתמטיקה, העוסק במערכות פורמליות ובדרך בה הן מקודדות מושגים אינטואיביים, כגון הוכחה או חישוביות. התחום הוא אחד מקבוצה של תחומים המכונים יסודות המתמטיקה משום שהם עוסקים בבסיס הפורמלי של המתמטיקה כולה. לוגיקה מתמטית עוסקת באותם חלקים של הלוגיקה שניתן ליצור להם מודל מתמטי. בעבר נקרא התחום גם בשמות לוגיקה סימבולית (בשל עיסוקו בטענות המיוצגות בידי סמלים) או מטה-מתמטיקה. השם השני מתייחס כיום רק לתורת ההוכחות (Proof Theory), אחד התחומים בלוגיקה מתמטית.
השיטה של הלוגיקה המתמטית לניתוח טענות היא כדלהלן:
- הצרנה: תרגום הטענות בשפה המדוברת לטענות בתחשיב שפה לוגי ריגורוזי, נוקשה וחד משמעי - כאשר טענות אטומיות מסומנות באותיות לטיניות או יווניות. שני התחשיבים הנפוצים הם "תחשיב הפסוקים" הבסיסי ו"תחשיב הפרדיקטים" המתקדם שמאפשר לטפל גם בטענות מסוג "כל x הוא y" או "קיים z כך ש...".
- ניתוח הטענות המוצרנות לפי אקסיומות הלוגיקה ("כללי המשחק"): עקרונות יסוד, כללי גרירה וכללי היסק (כללי היקש). שלב זה הוא לא יותר מאשר טיפול פורמלי במחרוזות strings וניתן לביצוע במלואו, ללא מעורבות אדם, על ידי מחשב.
כך לדוגמה, את הטענות "כשאני שבע אני מאושר" ו"כשאני מאושר אני פוצח בשיר" ניתן לכתוב כך:
1. A -> B
2. B -> C
כאשר A משמעותו "אני שבע", B משמעותו "אני מאושר" ו-C משמעותו "אני פוצח בשיר" ואילו החץ (<-) משמעותו היא שאמיתות הטענה בצד שמאל של החץ תגרור את אמיתות הטענה בצד ימין של החץ. כלומר, 1. פירושו "אם אני שבע אז אני מאושר" ו-2. פירושו "אם אני מאושר אז אני פוצח בשיר".
הלוגיקה המתמטית מעניקה כללים בעזרתם ניתן להסיק טענות חדשות מתוך טענות קיימות. לדוגמה, משני הביטויים למעלה ניתן להסיק באמצעות כלל ההיסק "מודוס פוננס" כי:
A -> C
ומכאן אנחנו מסיקים שהטענה "כשאני שבע אני פוצח בשיר" נכונה.
הוכחת טענות בלוגיקה מתמטית היא תהליך שבו אנחנו מתחילים מאוסף של הנחות יסוד ומסיקים מהן סדרה של מסקנות עד שאנחנו מגיעים לטענה המבוקשת. הסקת המסקנות מתבססת על אוסף כללי יסוד שאי אפשר להוכיח את נכונותם אבל אנחנו מניחים שהם נכונים. כלל יסוד כזה מכונה אקסיומה.
תהליך הוכחה ריגורוזי מלא בלוגיקה פורמלית כולל את הצרנת הטענות לתחשיב שפה לוגי בעלי כללי דקדוק חד-משמעיים ואז ניתוחן לפי כללי היסק מוגדרים מראש ובדיקת תקפות המעברים. בדיקת תקפות המעברים היא אידאלית עבור מחשב. מכיוון שטענות שמוצרנות במלואן הן בלתי קריאות בפועל עבור בני אדם ומתמטיקאים, הוכחת משפטים עדיין נעשיית על ידי מתמטיקאים בשפה שהיא שילוב בין השפה היום-יומית לנוסחאות מתמטיות והצרנה לוגית חלקית.
