625 lines
21 KiB
Markdown
625 lines
21 KiB
Markdown
---
|
||
title: לוגיקה מתקדמת
|
||
tags:
|
||
- שנה_ג
|
||
- סמסטר_א
|
||
- פילוסופיה
|
||
- לוגיקה
|
||
- לוגיקה_מתקדמת
|
||
---
|
||
|
||
|
||
!!! info "חומר הקורס"
|
||
[מודל](https://moodle.bgu.ac.il/moodle/course/view.php?id=55543), [סילבוס](https://moodle.bgu.ac.il/moodle/mod/resource/view.php?id=2865244)
|
||
|
||
## תוכן העניינים
|
||
|
||
#### 1. [מבוא]()
|
||
|
||
#### 2. [לוגיקה מודאלית](/פילוסופיה/לוגיקה/מתקדמת/מודאלית)
|
||
|
||
#### 3. [מודלי קריפקה](/פילוסופיה/לוגיקה/מתקדמת/קריפקה)
|
||
|
||
#### 4. [לוגיקה טמפורלית](./טמפורלית)
|
||
|
||
#### 5. [שלילת המודאליות של קווין](./קווין)
|
||
|
||
#### 6. [לוגיקה אינטואיציוניסטית](./אינטואיציוניסטית)
|
||
|
||
#### 7. [לוגיקה פאראקונסיסטנטית](./פאראקונסיסטנטית)
|
||
|
||
|
||
|
||
|
||
## מושגי יסוד
|
||
|
||
למדנו ב[לוגיקה](/פילוסופיה/לוגיקה) ש -
|
||
|
||
**טענות** - אמירות שניתן לקבוע כאמת או שקר
|
||
|
||
**טיעון** - אוסף של טענות ומסקנה
|
||
|
||
**תקפות** - *אם כל ההנחות אמיתיות, המסקנה בהכרח אמיתית*
|
||
|
||
|
||
אבל בעצם, *לא נכון*[^1].
|
||
|
||
העקרונות, ההצרנות, והכללים הללו *פשוט לא תופסים* את הדרך שבה אנחנו חושבים ברוב המקרים.
|
||
|
||
אולי אם נפתח את הכלים הלוגיים הללו, נוכל ללכוד בצורה טובה יותר את האופן שבו אנחנו חושבים.
|
||
|
||
### למה זה לא עובד?
|
||
|
||
#### הכרח
|
||
|
||
נניח ויש לי כאן בקבוק. הוא יכול להיות מלא, או ריק.
|
||
|
||
!!! info ""
|
||
1. אם הבקבוק מלא, אז הוא **בהכרח** לא ריק
|
||
2. הבקבוק מלא
|
||
3. הבקבוק **בהכרח** לא ריק
|
||
|
||
$$
|
||
\begin{align}
|
||
F \to E \\
|
||
F \\
|
||
\neg E \\
|
||
\end{align}
|
||
$$
|
||
|
||
האמנם? אם הבקבוק מלא יש *הכרח* מטאפיזי שהוא יהיה לא ריק? הבקבוק לעולם לא יכול להיות ריק, כחוק טבע? כנראה שלא - הבקבוק *יכול* להיות ריק[^2].
|
||
|
||
ואיפה הבעיה? המילה **בהכרח**.
|
||
|
||
האם נוכל לוותר בהכרח? בפילוספיה, כנראה שלא. זכרו את ההגדרה של תקפות - אם הטיעון תקף, המסקנה *בהכרח* אמיתית.
|
||
|
||
הלוגיקה שלמדנו עד כה לא יודעת לאכול את עניין ה*הכרח*. מה עושים? זה הרבה יותר מורכב ממה שנדמה לנו - חלק מהבעיות האלו היו פתוחות עשורים שלמים!
|
||
|
||
#### תנאי
|
||
|
||
!!! info ""
|
||
אם יש יותר מ70 אנשים בחדר הזה, אז יורד גשם
|
||
|
||
|
||
לפני ששטפו לנו את המוח בתואר, כולנו הבנו שזה לא נכון. אבל מבחינה לוגית, זה תקף, וכולנו החלטנו שזה דווקא כן נכון.
|
||
|
||
| $A$ | $B$ | $A \to B$ |
|
||
| --- | --- | --------- |
|
||
| T | T | T |
|
||
| F | T | T |
|
||
| T | F | F |
|
||
| F | F | T |
|
||
|
||
אבל ברור לנו שזה לא נכון - חייב להיות איזשהו קשר *תוכני* בין הטענות, בלי קשר למה שאומרת טבלת האמת. יש סיבות לכך שדרשנו את זה, אבל עדיין יש כאן בעיה.
|
||
|
||
#### משפטי תנאי נוגדי מציאות
|
||
|
||
!!! info ""
|
||
אם טראמפ לא היה מנצח את מערכת הבחירות, אז בוש היה מנצח.
|
||
|
||
אמיתי? לא. בוש לא התמודד מול טראמפ. אבל -
|
||
!!! info ""
|
||
אם טראמפ לא היה מנצח את מערכת הבחירות, אז האריס הייתה מנצחת.
|
||
|
||
לוגית, המבנה זהה. אבל אחד נוגד מציאות והשני לא - ואנחנו מדברים ככה כל הזמן; איך נפלה ביניהם בכלים לוגיים?
|
||
|
||
!!! success ""
|
||
לדוגמאות נוספות - [Vann McGee's Counterexample to Modus Ponens](https://www.jstor.org/stable/4320663)
|
||
|
||
|
||
#### מסתירה נובע כל דבר
|
||
|
||
*אם ההנחות נכונות, אז המסקנה בהכרח אמיתית*. אם ההנחה שלי נכונה, המסקנה *לא יכולה לסתור אותה*. אז מסתירות נובע כל דבר[^3], אחלה. אבל, *לא נכון* - אנחנו לא חושבים ככה; חייב להיות קשר תוכני!
|
||
|
||
#### תואר הפועל
|
||
|
||
!!! info ""
|
||
1. יוסי רץ במהירות
|
||
2. יוסי רץ
|
||
|
||
$$
|
||
\begin{align}
|
||
Qy \\
|
||
Ry
|
||
\end{align}
|
||
$$
|
||
|
||
מפרדיקט אחד נובע פרידקט אחר - מבחינת הלוגיקה, זה **לא נכון**, אבל *ברור* שאם יוסי רץ במהירות, יוסי רץ; אנחנו מסיקים ככה כל הזמן, ובצדק.
|
||
|
||
#### הקשרים מכוונים
|
||
<small>קונטסקטים אינטציונליים</small>
|
||
|
||
$$ \begin{align}
|
||
a = b \\
|
||
pa\\
|
||
\hline\\
|
||
pb
|
||
\end{align}
|
||
$$
|
||
|
||
!!! info ""
|
||
1. טראמפ יודע שהמורה בקורס בלוגיקה הוא המורה בקורס בלוגיקה
|
||
2. מורה הקורס בלוגיקה הוא אני (רע גולן)
|
||
3. טראמפ יודע שהמורה בקורס בלוגיקה הוא רע גולן
|
||
|
||
מממ, לא.
|
||
|
||

|
||
<small>טראמפ לומד לוגיקה (בינה מלאכותית). לא סביר.</small>
|
||
|
||
|
||
|
||
אי אפשר לוותר על הקשרים מכוונים כמו *יודע ש*, *מאמין ש*, וכדומה. אבל ברגע שגוררים אותם פנימה, הלוגיקה מתפרקת.
|
||
|
||
אנחנו אמנם טועים לפעמים, אבל רוב ההיסקים שלנו - כמו שטראמפ לא מכיר את המרצה שלנו ללוגיקה - הם נכונים; איך אפשר ליישב את הלוגיקה עם החשיבה שלנו?
|
||
|
||
#### כימות
|
||
|
||
!!! info ""
|
||
פגסוס הוא סוס מכונף
|
||
יש דבר כזה שהוא מכונף
|
||
|
||
$$\begin{align}
|
||
Wp\\
|
||
\exists xWx
|
||
\end{align}$$
|
||
|
||
|
||
פגסוס הוא סוס עם כנפיים. אבל פגסוס לא קיים. אבל יש דבר מכונף. אז אנחנו מסכימים שפגסוס קיים אבל לא קיים. יש כל מיני [פתרונות מוצעים](/פילוסופיה/לשון/ראסל#האובייקט-הריק-של-מיינונג), אבל הם מצדיקים את השם הרע שיוצא לפילוסופיה.
|
||
|
||
הפתרון כרוך בהקשר - ברור לנו שפגסוס אמיתי במובן שהוא דבר שיש בראש שלנו, אבל לא *באמת* קיים בחוץ בעולם. אבל כמו שראינו, ברגע שנכנס הקשר, הלוגיקה מתפרקת.
|
||
|
||
#### נוגדי-אפשרות
|
||
<small>Counterpossibles</small>
|
||
|
||
!!! info ""
|
||
אם הייתי מוצא דוגמה נגדית למשפט האחרון של פרמה, הייתי מפורסם.
|
||
|
||
זה משפט אמיתי. אבל
|
||
|
||
!!! info ""
|
||
אם הייתי מוצא דוגמה נגדית למשפט האחרון של פרמה, הירח היה עשוי מגבינה
|
||
|
||
המשפט האחרון לא רק שקרי - *הוא לא יכול להיות נכון לעולם*; אין שום אפשרות כזו - היא נוגדת את חוקי הפיזיקה.
|
||
|
||
|
||
#### דו-ערכיות
|
||
|
||
אריסטו נותן לנו דוגמה -
|
||
|
||
!!! info ""
|
||
מחר יתקיים קרב ימי
|
||
|
||
אנחנו לא יודעים אם מחר יתקיים קרב ימי. אנחנו מניחים שיש לו ערך אמת - כמו שלכל פסוק יש ערך אמת. אבל בעצם יש פה השלכה מטאפיזית מזעזעת -
|
||
|
||
<big><bold>דטרמיניזם</bold></big>
|
||
|
||
|
||
רגע, *מה*? זה שזה נכון או לא נכון זה עיקרון סמנטי - אבל ש*זה* יגרור עיקרון מטאפיזי, כאילו
|
||
אמיתותו של הקרב הימי *כבר* קבועה מראש?
|
||
|
||
|
||
יש גם את העניין של *מחר*. הלוגיקה שלנו צריכה לדעת "לאכול" היבטים טמפורליים - בזמן. אין חיה כזו בינתיים.
|
||
|
||

|
||
<small>קרב ימי. יתקיים מחר?</small>
|
||
|
||
#### פרדוקסיים סמנטיים
|
||
|
||
**פרדוקס סמנטי** הוא פרדוקס שקשור במונחי אמת, שקר, הוראה וכדומה. למשל -
|
||
|
||
!!! warning "המשפט הזה הוא שקר."
|
||
|
||
אם המשפט הזה אמיתי, אז הוא שקרי, אז הוא אמיתי...
|
||
|
||
זו *צרה צרורה*, אומר רע בדרמטיות, *קטסטרופה* - לא להאמין כמה קשה להיפטר מהדבר הזה.
|
||
|
||
מה שלכאורה עולה מ**פרדוקס השקרן** הזה הוא שיש בעיה בערכי האמת שאנחנו מניחים - אמת ושקר - שמוציאים אחד את השני. מושג ה*אמת* נשמע מאוד מאוד חשוב; האתגר כאן הוא להציל את מושג האמת מסתירות ופרדוקסים - באמצעות תיאור הולם.
|
||
|
||
### תורת הקבוצות
|
||
|
||
**תורת הקבוצות** היא תורה מתמטית שפיתח המתמטיקאי הגרמני [גאורג קאנטור](https://en.wikipedia.org/wiki/Georg_Cantor).
|
||
|
||
**קבוצה** היא אוסף של איברים.
|
||
|
||
#### סימון
|
||
|
||
נסמן קבוצה באות גדולה, ונמנה את האיברים בסוגריים מסולסלים.
|
||
|
||
**פינגווינים**
|
||
{ קיסרי, ג'נטו, אדלי ... } = P
|
||
|
||
איברים יהיו אותיות קטנות באנגלית -
|
||
|
||
$$\begin{align}
|
||
P\\
|
||
\{e, g, a\}
|
||
\end{align}
|
||
$$
|
||
#### שייכות
|
||
ושייכות בסימן השייכות -
|
||
|
||
$e \in P$
|
||
|
||
!!! warning ""
|
||
קבוצות יהיו שוות אם ורק אם כל האיברים זהים - נאמר ש$A=P$ אם ורק אם לכל a:
|
||
$a \in A = a \in P$
|
||
|
||
זוהי טענה חשובה פילוסופית!
|
||
|
||
#### חלקיות
|
||
|
||
$A \subseteq P$ אם לכל $a$:
|
||
|
||
אם $a \in B$ אז $a \in P$
|
||
|
||
נאמר שA **חלקי ממש** לP אם $A \subseteq P$ *וגם* יש $a \in P$ כך ש $a \notin A$
|
||
|
||
#### כלליות
|
||
|
||
לפעמים נצא מנקודת ההנחה (הבעייתית!) שיש קבוצה אוניברסלית U - כלומר, הקבוצה של כל האיברים באשר הם.
|
||
|
||
#### קבוצה משלימה
|
||
|
||
עבור קבוצה שכוללת את כל האיברים *שאינם* שייכים לקבוצה, נגיד שהיא קבוצה *משלימה*. למשל, לא-פינגווינים -
|
||
|
||
$A = Pc$
|
||
|
||
|
||
משמע A הוא כל מה שאינו פינגווינים.
|
||
|
||
$Ac = \{ a | a \notin A (a \in A)\}$
|
||
|
||
#### איחוד
|
||
|
||
בהינתן A, P, נוכל לדבר על קבוצת האיחוד - פינגווינים ולא-פינגווינים -
|
||
|
||
$A \cup P = \{ x | x \in A \lor x \in B \}$
|
||
|
||
#### חיתוך
|
||
|
||
מנגד, קבוצת החיתוך היא מה שכוללת לא A ולא P (אם A היא קבוצת הסטודנטים - כל מה שלא סטודנט ולא פינגווין)
|
||
|
||
$A \cap B = \{ x | x \in A \land x \in B \}$
|
||
|
||
#### קבוצה ריקה
|
||
|
||
קבוצה בלי כלום.
|
||
|
||
$\emptyset$
|
||
|
||
#### חוקי דה-מורגן
|
||
|
||
$(A \cup B)\land c \land \subseteq A \land c \cap B \land c$
|
||
|
||
זה מקביל לפסוק הבא מתחשיב הפסוקים:
|
||
|
||
$$\land \neg (p \lor q ) \equiv \neg p \land \neg q$$
|
||
|
||
$$A \land c \cap B \land c \subseteq (A \cup B) \land c $$
|
||
|
||
(כאן הייתה הוכחה, אבל אני מאמין לרע)
|
||
|
||
#### אבל למה?
|
||
|
||
כי מתמטיקאים מאמינים שאובייקטים מתמטיים הם כולם קבוצות - דרך מסוימת לחשוב על הדברים. *מה הקשר?* זה מה שקאנטור הראה, אבל זה נוח גם לנו כפילוסופים - כל מה שיש במתמטיקה, מטאפיזית, הן קבוצות - ולא צריך לריב על כל הישיים האחרים.
|
||
|
||
#### יחסים
|
||
|
||
ביחסים, בניגוד לקבוצות, הסדר משנה - נסמן R כלהיות אבא של -
|
||
|
||
|
||
$R(b,a)$
|
||
$R(a,b)$
|
||
|
||
|
||
מושיק אבא של איציק *ממש לא שווה* לאיציק אבא של מושיק.
|
||
|
||
לכן היחס של R(b,a) הוא **זוג סדור**, שנסמן ב`<>`. כלומר,
|
||
|
||
|
||
$F(x,y) = \{<a,b> |\ a\ is\ the\ father\ of\ b\}$
|
||
|
||
נייצג את זה בתורת הקבוצות -
|
||
|
||
|
||
$<x,y> \equiv \neg \{\{x\}, \{x,y\}\}$
|
||
|
||
|
||
אם `<a,b> = <c,d>`, אז `a=c, b=d`.
|
||
|
||
|
||
!!! warning ""
|
||
אם a≠c אזי {a} ≠ {c}
|
||
אבל אז: {a} = { c,d }
|
||
אז בהכרח: a=c=d כי אלו קבוצות באותו הגודל
|
||
באופן דומה, b=d
|
||
|
||
#### עקרון הקומפרהנציה
|
||
|
||
על פניו, זהו רק שכתוב של תחשיב הפסוקים. הוא נושא את **עקרון הקופמרהנציזה** - *לכל תכונה P(x) יש קבוצה* -
|
||
|
||
$\{x\ |\ P(x)\}$
|
||
|
||
|
||
[**ראסל**](/פילוסופיה/לשון/ראסל) זיהה בעייה. דמיינו שיש קבוצת ספלי תה[^4]. הקבוצה המשלימה - לא-ספלי-תה - אינה ספל תה, ולכן שייכת לעצמה.
|
||
|
||
|
||
```
|
||
R
|
||
|
||
R = {x | x ∉ X}
|
||
האם R ∈ R?
|
||
```
|
||
|
||
|
||
הדבר הזה מתנהג כמו [פרדוקס השקרן](#פרדוקסיים-סמנטיים), ובגללו תורת הקבוצות מורכבת בהרבה היום.
|
||
|
||
!!! warning "הערה על סוגים של יחסים"
|
||
כזכור, יחס R הוא קבוצה של זוגות סדורים:
|
||
|
||
`R = { <x,y> | x עומד ביחס Y עם R}`
|
||
|
||
אפשר לחשוב על זה שכל הפריטים בR עומדים באותו יחס אחד עם השני.
|
||
למשל, *קרוב ל...* - אם Y קרוב לR וX קרוב לR אז X קרוב לY.
|
||
|
||
במצב כזה, היחס יהיה יחס **סימטרי**:
|
||
|
||
אם `xRy -> yRx`
|
||
|
||
מצב נוסף הוא יחס **רפלקסיבי** אם לכל X:
|
||
|
||
`xRX`
|
||
|
||
- יחס R ייקרא **טרנזיטיבי** אם לכל x,y,z:
|
||
|
||
`אם xRy וגם yRz אז xRz`
|
||
|
||
(אם אני שוקל יותר מכלב, וכלב שוקל יותר מפינגווין, אני שוקל יותר מפינגווין).
|
||
|
||
יחס R ייקרא **סדרתי** אם לכל x יש y:
|
||
|
||
`xRy`
|
||
|
||
(לכל מישהו יש מישהו שאוהב אותו, לכל ילד יש הורים).
|
||
|
||
זה האקדח במערכה הראשונה. נחזור לזה.
|
||
|
||
|
||
## תחשיב הפסוקים (כפי שמעולם לא הכרתם אותו)
|
||
|
||
רגע, כבר למדנו [תחשיב הפסוקים](/פילוסופיה/לוגיקה/פסוקים). למה חוזרים לזה עכשיו?
|
||
|
||
בתחשיב יש *מלא* כללים. מי זוכר את כל זה? אולי זה חוטא ל[תער של אוקאם](/פילוסופיה/דת/חובה#התער-של-אוקאם), ואפשר לפשט את זה?
|
||
|
||
אנחנו למדנו **דדוקציה טבעית**. למרבה הצער, אנחנו עדיין *לא* יודעים לעשות לוגיקה מודאלית (קרי: מתקדמת) בדדוקציה טבעית, אלא במערכת אחרת - **מערכת הילברט**, או **אקסיומטית**.
|
||
|
||
החדשות הטובות הן שאנחנו כבר יודעים את הלוגיקה, ויהיו לשיטה החדשה רק ארבע עקרונות. החדשות הרעות הם שהם נבזיים. החדשות הטובות שוב הן שאנחנו נרמה.
|
||
|
||
|
||
### מרכיבי מערכת אקסיומטית
|
||
|
||
1. כללי היסק
|
||
|
||
אלו החברים שאנחנו מכירים - מודוס פוננס וחבריו -
|
||
|
||
$$
|
||
\begin{align}
|
||
A \to B\\
|
||
A\\
|
||
\hline
|
||
B
|
||
\end{align}
|
||
$$
|
||
|
||
|
||
3. אקסיומות
|
||
|
||
אמיתות בסיסיות שאפשר לכתוב בכל שלב בגזירה פורמאלית.
|
||
|
||
שלושת האקסיומות שלנו יהיו כאלו:
|
||
|
||
1. $A \to ( B \to A )$
|
||
2. $( A \to ( B \to C )) \to (( A \to B ) \to (A \to C))$
|
||
3. $( \neg B \to \neg A ) \to ( A \to B )$
|
||
|
||
|
||
|
||
!!! info ""
|
||
למה זה נכון? ככה! זה עובד; אלו טאוטולוגיות. זה הרבה פחות אינטואיטיבי מדדוקציה טבעית, אבל זה תופס - תסמכו על רע.
|
||
|
||
אלו לא לגמרי אקסיומות - הן יותר כמו *סכמות*.
|
||
|
||
!!! success "[העשרה - Relevance Logic](https://plato.stanford.edu/entries/logic-relevance/)"
|
||
|
||
### גזירות פורמאליות
|
||
|
||
!!! danger "עכשיו השלב המגעיל!"
|
||
|
||
נוכיח ש$A \to A$ ללא הנחות:
|
||
|
||
(נסמן $B = A \to A$)
|
||
|
||
| ביטוי | הצדקה |
|
||
| ------------------------------------------------------------------- | ---------------- |
|
||
| $A \to ((A \to A) \to A)$ | אקסיומה 1 |
|
||
| $( A \to (( A \to A) \to A)) \to (A \to (A \to A)) \to (A \to A) )$ | אקסיומה 2 |
|
||
| $( A \to ( A \to A) ) \to (A \to A)$ | Modus Ponnes 1,2 |
|
||
| $A \to (A \to A)$ | אקסיומה 1 |
|
||
| $A \to A$ | Modus Ponnes 3,4 |
|
||
|
||
|
||
אבל רגע. מה זה בכלל גזירה פורמאלית?
|
||
|
||
!!! info "גזירה פורמאלית"
|
||
נאמר שפסוק A גזיר\יכיח **מקבוצת** הנחות Γ במערכת הילברט ( Γ |-[^5] A) אם יש גזירה פורמלית - סדרת פסוקים מהצורה `A1, A2, A3...` כך שלכל פסוק `Ai` בסדרה אחת מהאפשרויות הבאות נכונה:
|
||
|
||
1. `Ai` הוא אקסיומה
|
||
2. `Ai` הוא הנחה
|
||
3. `Ai` התקבל על ידי מודוס פוננס על שורות קודמות
|
||
|
||
|
||
דוגמה נוספת - `A, ~A |- B` (*מסתירה נובע כל דבר*)
|
||
|
||
```
|
||
1. ~A #Assumption
|
||
2. ~A -> (~B -> ~A) #Axiom 1
|
||
3. ~B -> ~A # Modus Ponens 1,2
|
||
4. (~B -> ~A) -> (A -> B) #Axiom 3
|
||
5. A -> B #MP 3,4
|
||
6. A #Assumption
|
||
7. B #MP 5,6
|
||
```
|
||
|
||
|
||
!!! success "עכשיו קיצורי דרך!"
|
||
|
||
|
||
## משפט הדדוקציה
|
||
|
||
!!! info "משפט הדדוקציה"
|
||
`Γ ∪ {A} ⊢ B` אם ורק אם `Γ ⊢ A-> B`
|
||
|
||
דוגמה:
|
||
|
||
`A ⊢ A` ולכן לפי משפט הדדוקציה
|
||
` ⊢ A -> A`
|
||
|
||
|
||
דוגמה שנייה: נוכיח
|
||
|
||
`{ A -> B, B -> C } |- A -> C`
|
||
|
||
לפי משפט הדדוקציה מספיק להראות:
|
||
|
||
`{ A-> B, B-> C, A} |- C`
|
||
|
||
```
|
||
1. A #Assumption
|
||
2. A -> B #Assumption
|
||
3. B #MP 1,2
|
||
4. B -> C #Assumption
|
||
5. C # MP 3,4
|
||
```
|
||
|
||
|
||
למה משפט הדדוקציה נכון?
|
||
|
||
בכיוון הראשון, נניח
|
||
|
||
`Γ |- A-> B`
|
||
|
||
לכן, גם
|
||
|
||
`Γ ∪ {A} |- A -> B`
|
||
|
||
כמו כן,
|
||
|
||
`Γ ∪ {A} |- A`
|
||
|
||
(זו הנחה).
|
||
|
||
וע"י MP נקבל:
|
||
|
||
`Γ ∪ {A} + B`
|
||
|
||
כנדרש.
|
||
|
||
בכיוון השני נתון
|
||
|
||
`Γ ∪ {A} + B`
|
||
|
||
ונוכיח
|
||
`Γ |- A -> B`
|
||
|
||
כבר הוכחנו ש `A, ~A |- B` - עכשיו נבנה הוכחה עבור
|
||
|
||
`~A |- A-> B`
|
||
|
||
```
|
||
1. ~A -> (A -> ~A) # Axiom 1
|
||
2. ~A # Assumption
|
||
3. A -> ~A # MP 1,2
|
||
4. R # Axiom 1 (marking)
|
||
5. R -> (A -> R) # Axiom 1
|
||
6. A -> R # MP 4,5
|
||
7. (A -> B) -> ((A -> ~A) -> (A -> (~B -> ~A)) # Axiom 2
|
||
8. (A -> ~A) -> (A -> (~B -> A)) # MP
|
||
9. A -> ~A # 3.
|
||
10. A -> (~B -> ~A) # MP
|
||
```
|
||
|
||
|
||
וכו' וכו'.
|
||
|
||
## משפט השלילה
|
||
|
||
!!! info "משפט השלילה"
|
||
אם `Γ ∪ {~A}` לא עקבית (מגיעה לסתירה), אז `Γ |- A`.
|
||
|
||
נראה ש:
|
||
`~~A |- A`
|
||
|
||
לפי משפט ההוכחה בשלילה, מספיק להראות שהקבוצה `{~~A, ~A}` לא עקבית. וזה ברור.
|
||
|
||
**הוכחת משפט ההוכחה בשלילה**:
|
||
|
||
נניח `Γ ∪ {~A}` לא עקבית - כלומר אפשר להוכיח ממנה כל פסוק.
|
||
|
||
תהי P אקסיומה כלשהי. אזי: `Γ ∪ {~A} |- ~P`
|
||
|
||
לפי משפט הדדוקציה:
|
||
|
||
`Γ ∪ ~A -> ~P`
|
||
|
||
כמו כן:
|
||
|
||
`Γ |- (~A -> P) -> (P -> A)` (אקסיומה 3)
|
||
|
||
MP:
|
||
|
||
`Γ |- P -> A`
|
||
|
||
אבל
|
||
|
||
`Γ |- P`
|
||
|
||
ולכן MP נותן `Γ |- A` כמו שרצינו.
|
||
|
||
### תחביר וסמנטיקה
|
||
|
||
**תחביר** (סינטקס) הוא הכללים הטכניים שקובעים מהו פסוק וכן מתי אפשר להוכיח פסוק מסוים A מסט הנחות Γ (Γ |- A).
|
||
|
||
**סמנטיקה** היא תורת משמעות. מבחינתו, משמעותו של פסוק היא תנאי האמת שלו - מתי הוא אמיתי ומתי הוא שקרי. אפשר לעשות זאת עם כלים כמו טבלאות אמת -
|
||
|
||
| A | ~ A |
|
||
| --- | --- |
|
||
| T | F |
|
||
| F | T |
|
||
|
||
| A | B | A -> B |
|
||
| --- | --- | ------ |
|
||
| T | T | T |
|
||
| F | T | T |
|
||
| T | F | F |
|
||
| F | F | T |
|
||
|
||
|
||
טיעון מקבוצת הנחות Γ למסקנה A תקף אם בטבלת האמת אין שורה בה כל איברי Γ אמיתיים אבל A שקרי.
|
||
|
||
Γ |=[^6] A
|
||
|
||
מערכת הוכחה תיקרא **נאותה** אם `Γ |- A` אז `Γ |= A`.
|
||
|
||
לעומת זאת, מערכת הוכחה תיקרא **שלמה** אם `Γ |= A` אז `Γ |- A`. זה לא דבר קל - זה אומר שאם טבלאות האמת תקינות (אין מצב שבו כל ההנחות נכונות והמסקנה שקרית), *בהכרח* תהיה הוכחה כזו במערכת, מורכבת ככל שתהיה.
|
||
|
||
|
||
|
||
|
||
|
||
[^1]: ר' גם - [ויטגנשטיין](/פילוסופיה/דת/שפה#ויטגנשטיין).
|
||
[^2]: זכרו, אנחנו לא מערבים כרגע זמן - אז אין דברים כמו *אם הבקבוק מלא עכשיו*...
|
||
[^3]: ר' גם [חוק הסתירה האריסטותלי](/פילוסופיה/יוונית/אריסטו/מטאפיזיקה#חוק-הסתירה).
|
||
[^4]: ראסל היה בריטי.
|
||
[^5]: סימן ה"יכיח" (בר הוכחה). המציא אותו [פרגה](/פילוסופיה/לשון/פרגה).
|
||
[^6]: סימן ה"מוכח" (בדקנו את היכיח, והוא באמת הוכיח). |