לוגיקה מתמטית – הבדלי גרסאות

תוכן שנמחק תוכן שנוסף
←‏ראו גם: הרחבה
עריכה, הרחבה
שורה 1:
'''לוגיקה מתמטית''' הוא תחום ב[[מתמטיקה]], העוסק במערכות פורמליות ובדרך בה הן מקודדותמגלמות מושגים אינטואיטיביים, כגון [[הוכחה]] או [[חישוביות]]. התחום הוא אחד מקבוצה של תחומים המכונים [[יסודות המתמטיקה]] משום שהם עוסקים בבסיס הפורמלי של המתמטיקה כולה.
לוגיקה מתמטית עוסקת באותם חלקים של ה[[לוגיקה]] שניתן ליצור להם [[מודל מתמטי]]. בעבר נקרא התחום גם בשמות '''לוגיקה סימבולית''' (בשל עיסוקו בטענות המיוצגות בידי סמלים) או '''מטה-מתמטיקה'''. השם השני מתייחס כיום רק ל[[תורת ההוכחות]], אחד התחומים בלוגיקה מתמטית.
 
#בכדי לנתח טענות, הלוגיקה המתמטית דורשת שאלו יעברו [[הצרנה]]: תרגום הטענות בשפה המדוברת לטענות(או בתחשיבבשפה שפההמתמטית) לוגילטענות בתחשיב [[ריגורוזי]], נוקשה וחד משמעי - כלומר על פי חוקי התחביר הלוגי. כאשר טענות אטומיות מסומנות באותיות לטיניות או יווניות. שני התחשיבים הנפוצים הם "[[תחשיב הפסוקים]]" הבסיסי, העוסק בקשר בין ערכי האמת של טענות פשוטות ומורכבות, ו"[[תחשיב הפרדיקטים]]" המתקדם, שמאפשרהמאפשר לטפל גםבמבנה בטענותהפנימי מסוגשל "כלטענות א'ובקשר הואשהן ב'"מביעות אובין "קייםאובייקטים ג'לבין כךהמושגים ש..."(פרדיקטים) החלים עליהם.
השיטה של הלוגיקה המתמטית לניתוח טענות היא כדלהלן:
 
# [[הצרנה]]: תרגום הטענות בשפה המדוברת לטענות בתחשיב שפה לוגי [[ריגורוזי]], נוקשה וחד משמעי - כאשר טענות אטומיות מסומנות באותיות לטיניות או יווניות. שני התחשיבים הנפוצים הם "[[תחשיב הפסוקים]]" הבסיסי ו"[[תחשיב הפרדיקטים]]" המתקדם שמאפשר לטפל גם בטענות מסוג "כל א' הוא ב'" או "קיים ג' כך ש...".
הוכחת טענות בלוגיקה מתמטית היא תהליך שבו מתחילים מאוסף של הנחות יסוד ומסיקים מהן סדרה של מסקנות עד שמגיעים לטענה המבוקשת. הסקת המסקנות מתבססת על אוסף כללי יסוד שאי אפשר להוכיח את נכונותם. כלל יסוד כזה מכונה [[אקסיומה]]. הלוגיקה המתמטית מנתחת את הטענות המוצרנות לפי ה[[אקסיומות]] ו[[כלל היסק|כללי היסק]] של המערכת. ניתוח זה של הוכחות (טיעונים המורכבים ממספר טענות) הוא לא יותר מאשר טיפול פורמלי ב[[מחרוזת (תכנות)|מחרוזות]] וניתן לביצוע במלואו, ללא מעורבות אדם, על ידי [[מחשב]]. מכיוון שטענות מורכבות שמוצרנות במלואן הן בלתי קריאות בפועל למרבית בני האדם (כולל מתמטיקאים), ישנן הוכחות שרק מחשבים יכולים לבצע בפועל. ואולם, מאותה סיבה, הוכחת [[משפט (מתמטיקה)|משפטים]] מתמטיים רבים עדיין נעשית על ידי מתמטיקאים בשפה שהיא שילוב בין השפה היום-יומית לנוסחאות מתמטיות והצרנה לוגית חלקית.
# ניתוח הטענות המוצרנות לפי [[אקסיומות הלוגיקה]] ("כללי המשחק"): עקרונות יסוד, כללי גרירה ו[[כלל היסק|כללי היסק]] (כללי היקש). שלב זה הוא לא יותר מאשר טיפול פורמלי ב[[מחרוזת (תכנות)|מחרוזות]] וניתן לביצוע במלואו, ללא מעורבות אדם, על ידי מחשב.
 
 
כך לדוגמה, את הטענות "כשאני שבע אני מאושר" ו"כשאני מאושר אני פוצח בשיר" ניתן לכתוב כך:
שורה 19 ⟵ 20:
ומכאן אנחנו מסיקים שהטענה "כשאני שבע אני פוצח בשיר" נכונה.
 
הוכחת טענות בלוגיקה מתמטית היא תהליך שבו מתחילים מאוסף של הנחות יסוד ומסיקים מהן סדרה של מסקנות עד שמגיעים לטענה המבוקשת. הסקת המסקנות מתבססת על אוסף כללי יסוד שאי אפשר להוכיח את נכונותם אבל מניחים שהם נכונים. כלל יסוד כזה מכונה [[אקסיומה]].
 
תהליך הוכחה [[ריגורוזי]] מלא בלוגיקה פורמלית כולל את [[הצרנה|הצרנת]] הטענות ל[[תחשיב שפה]] לוגי בעלי כללי דקדוק חד-משמעיים ואז ניתוחן לפי כללי היסק מוגדרים מראש ובדיקת תקפות המעברים. בדיקת תקפות המעברים היא אידאלית עבור [[מחשב]]. מכיוון שטענות שמוצרנות במלואן הן בלתי קריאות בפועל למרבית בני האדם (כולל מתמטיקאים), הוכחת [[משפט (מתמטיקה)|משפטים]] עדיין נעשית על ידי מתמטיקאים בשפה שהיא שילוב בין השפה היום-יומית לנוסחאות מתמטיות והצרנה לוגית חלקית.
 
== ראו גם ==