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

השאלה בתחשיב היחסים. א. הוכיחו או הפריכו כל אחת מהטענות הבאות: $M$ מודל, $s$ השמה ו-$\varphi(x)$ נוסחה. a. אם $M \models_s \exists x \varphi(x)$ אז $M \models_s \varphi(x)$ b. אם $\models \varphi(x)$ אז $\not\models \neg\varphi(x)$ ב. במידה והפסוק הבא אמיתי לוגית כתבו סידרת הוכחה, אם לא תנו דוגמא נגדית. $\vdash \exists x P(x) \to (\exists x Q(x) \to \exists x (P(x) \to Q(x)))$

רמז: א. עבור סעיף a, חשבו על מודל עם שני איברים, כאשר הנוסחה $\varphi(x)$ נכונה רק עבור אחד מהם, וההשמה $s$ בוחרת עבור $x$ את האיבר השני. עבור סעיף b, השתמשו בהגדרת התקפות ובהגדרת הסיפוק של נוסחת שלילה. ב. כדי להוכיח $A \to (B \to C)$, ניתן להניח את $A$ ו-$B$ ולנסות לגזור את $C$. שימו לב שאם ידוע שקיים איבר $a$ המקיים $Q(a)$, ניתן להסיק מכך מסקנה ישירה לגבי הגרירה $P(a) \to Q(a)$.

פתרון: א. a. הטענה **אינה נכונה**. נפריך אותה על ידי דוגמה נגדית. ניקח **מבנה** $M$ שבו: * התחום (דומיין) הוא $D^M = \{1, 2\}$. * השפה מכילה סימן יחס חד-מקומי $P$. * ה**פירוש** של $P$ הוא $P^M = \{1\}$. * הנוסחה היא $\varphi(x) = P(x)$. * ניקח **השמה** $s$ המקיימת $s(x) = 2$. נבדוק את הנחת הטענה: $M \models_s \exists x P(x)$. לפי הגדרת **הסיפוק** של **כמת קיומי**, $M \models_s \exists x P(x)$ אם ורק אם קיים איבר $a \in D^M$ כך ש-$M \models_{s[x \mapsto a]} P(x)$. נבחר $a=1$. התנאי $M \models_{s[x \mapsto 1]} P(x)$ מתקיים אם ורק אם $s[x \mapsto 1](x) \in P^M$. מהגדרת ההשמה המעודכנת, $s[x \mapsto 1](x) = 1$. מכיוון ש-$1 \in P^M$ לפי הגדרת המבנה, התנאי מתקיים. לכן, $M \models_s \exists x P(x)$ היא טענה אמיתית, וההנחה מתקיימת. כעת נבדוק את מסקנת הטענה: $M \models_s P(x)$. לפי הגדרת הסיפוק, $M \models_s P(x)$ אם ורק אם $s(x) \in P^M$. לפי הגדרת ההשמה שבחרנו, $s(x) = 2$. אך $2 \notin P^M$ (מכיוון ש-$P^M=\{1\}$). לכן, $M \not\models_s P(x)$, והמסקנה אינה מתקיימת. מצאנו מבנה והשמה עבורם ההנחה מתקיימת והמסקנה לא. לפיכך, הטענה הופרכה. $\blacksquare$ b. הטענה **נכונה**. נוכיח אותה. נניח כי $\models \varphi(x)$. לפי הגדרת **תקפות לוגית**, לכל מבנה $M$ ולכל השמה $s$, מתקיים $M \models_s \varphi(x)$. לפי הגדרת **הסיפוק** של נוסחת שלילה, הטענה $M \models_s \varphi(x)$ שקולה לוגית לטענה $M \not\models_s \neg\varphi(x)$. לכן, מהנחתנו נובע כי לכל מבנה $M$ ולכל השמה $s$, מתקיים $M \not\models_s \neg\varphi(x)$. כעת, עלינו להוכיח כי $\not\models \neg\varphi(x)$. לפי הגדרה, $\not\models \neg\varphi(x)$ פירושו שקיים מבנה $M$ וקיימת השמה $s$ כך ש-$M \not\models_s \neg\varphi(x)$. מכיוון שהראנו כי *לכל* מבנה והשמה מתקיים $M \not\models_s \neg\varphi(x)$, אז בוודאי קיים לפחות זוג אחד כזה של מבנה והשמה (בהנחה הסטנדרטית בקורס שקיים לפחות מבנה אפשרי אחד). לכן, $\not\models \neg\varphi(x)$ מתקיים. $\blacksquare$ ב. הפסוק הוא **אמיתי לוגית (תקף)**. נציג **הוכחה פורמלית** המראה זאת. נשתמש במערכת הוכחה מסוג **היסק טבעי (Natural Deduction)**. כדי להוכיח פסוק מהצורה $A \to (B \to C)$, מספיק להניח את $A$ ואת $B$ ולהוכיח את $C$. כלומר, נוכיח את הגרירה הבאה: $\exists x P(x), \exists x Q(x) \vdash \exists x (P(x) \to Q(x))$. סדרת ההוכחה: 1. $\exists x P(x)$ (הנחה) 2. $\exists x Q(x)$ (הנחה) 3. $Q(a)$ (הנחה זמנית עבור **כלל היסק** של אלימינציה של $\exists$, כאשר $a$ הוא קבוע/משתנה "טרי" שאינו מופיע בהנחות או במסקנה הרצויה) 4. $P(a) \to Q(a)$ (משורה 3, לפי כלל היסק מתחשיב הפסוקים: $B \vdash A \to B$) 5. $\exists x (P(x) \to Q(x))$ (משורה 4, לפי כלל אינטרודוקציה של $\exists$) 6. $\exists x (P(x) \to Q(x))$ (מהנחה 2 ומהגזירה 3-5, לפי כלל אלימינציה של $\exists$. הכלל תקף כי $a$ אינו מופיע במסקנה (שורה 5), או בהנחות (שורות 1 ו-2).) 7. $\exists x Q(x) \to \exists x (P(x) \to Q(x))$ (מהנחה 2 ומהמסקנה 6, לפי כלל אינטרודוקציה של $\to$ / משפט הדדוקציה) 8. $\exists x P(x) \to (\exists x Q(x) \to \exists x (P(x) \to Q(x)))$ (מהנחה 1 ומהמסקנה 7, לפי כלל אינטרודוקציה של $\to$ / משפט הדדוקציה) ההוכחה מראה שהפסוק הוא **משפט (theorem)** של מערכת ההוכחה, ולכן הוא תקף לוגית. $\blacksquare$