מה זה לוגיקה פורמלית? מבוא למונח בדגש על תכנות

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

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

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

ספרות ה Mathematics Subject Classification (מהדורת 2010) כוללת חלוקה פרקטית של יסודות המתמטיקה ומתמטיקה לכמה עשרות תחומים ראשיים; שלושת התחומים הראשונים בחלוקה זו (מתוך 97) הם:

1. מבוא כללי ("General")
2. היסטוריה וביוגרפיה
3. לוגיקה מתמטית ויסודות; אשר כולל: היבטים פילוסופיים, לוגיקה מתמטית, תורת המודלים, חישוביות ורקורסיה, תורת הסטים, תורת ההוכחות ומתמטיקה קונסטרוקטיבית, לוגיקה אלגברית ומודלים לא סטנדרטיים

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

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

לוגיקה פרטית

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

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

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

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

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

ניתן לתאר לוגיקה פרטית או קולקטיבית בתורה לוגית-פורמלית.

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

תורה לוגית

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

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

לעתים, לוגיקה פרטית, לוגיקה קולקטיבית ובהן גם תורה לוגית, משקפות במידת מה, ככלל, את הלוגיקה הטהורה ביקום - כלומר את הכמות האמיתית של האובייקט הפיזיקלי או תהליכים בו, באם לוגיקה כזו קיימת.

מונחים נפוצים בלוגיקה פורמלית

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

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

אופרטור לוגי

אופרטור לוגי הוא סימן המהווה חלק מתחביר של שפה מסוימת ומסמל מצב או פעולה מסוימ\ת.

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

בשפות מחשב רבות, אופרטור לוגי נפוץ הוא סימן השוויון (=).
סימן זה משמש הן להשמה (assignment) כמו כאשר רוצים לשים למשתנה ערך ולשוויון, כמו כאשר רוצים לבדוק אם A שווה ל B;
השמה נכתבת לרוב עם סימן שוויון בודד (=) והשוואה נכתבת לרוב עם סימן שוויון פעמיים (==) או שלוש פעמים (===) בתלות בסוג ההשוואה (השוואה רפויה או נוקשה; עניין שלא אפרט עליו במאמר זה).

אופרטור לוגי שאני אוהב ללמד עליו הוא XOR.

הכלה והכללה

הכלה מתאר משהו שכלול בתוך משהו; למשל, גפרור בתוך קופסת גפרורים בתוך קופסת פלסטיק.
בלוגיקה פורמלית, סט שני יכול להיות מוכל בתוך סט ראשון.

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

פרט, כלל ויחס ביניהם

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

הערות כלליות

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

לוגיקה טהורה

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

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

אולי הגדרה טובה לכך היא "חוקי לוגיקה המהווים חלק מן הפיזיקה עצמה"