9 שיטות סינטקטיות בתחשיב הפרדיקטים

[[לוגיקה]]

עצי אמת בתחשיב הפרדיקטים

• ניזכר, יש לנו "כללים" לטיפול בכל קשר אמת: אחד לצורה הרגילה ואחד לצורה השלולה
• כדי ליצור עץ אמת בשפת תחשיב הפרדיקטים, נצטרך כלל גם לכל כמת, וכלל לכל כמת בצורתו השלולה

1. כלל ההדגמה הישית - Existential instantiation (אבריבציה E.I.)

• משמש כדי להיפטר מ-כמת ישי ∃
• הכלל קובע: אפשר להיפטר מהכמת ע"י מחיקת הסימן שלו, והחלפת כל משתנה שהיה קשור ע"י כמת זה בקבוע שלא הופיע לפני כן על הענף
• ההחלפה מתבצעת על אותו הענף (בלי לפתוח הסתעפות)

• למשל: μΦμ∃ (μ משתנה קשור) הופך ל: Φv (העפנו את הכמת, השארנו את הפרדיקט, החלפנו את המשתנה הקשור בקבוע חדש)

• אם קשורים שני משתנים, נגיד (x(Fx∧Gx∃, נשנה את שניהם לאותו קבוע, כך:

• Fa∧Ga
• ואם למשל כבר יש על הענף קבוע a, נעשה Fb∧Gb

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

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

  • (נזכור שקונסיסטנטי = לפחות ענף אחד פתוח)

• ולמה חשוב שזה יהיה משתנה שלא הופיע עדיין על הענף?

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

• לשים לב שניתן לחזור על אותו משתנה אם הוא הופיע על ענף אחר (ענף זה מה שבודקים כדי לחפש כפילויות ולקבוע סגור/פתוח), למשל על c בדוגמה הבאה: ![[Pasted image 20250125141938.png|300]]

2. כלל ההדגמה הכוללת - Universal Instantiation (אבריבציה U.I.)

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

• אם אין קבועים בענף, נשתמש בקבוע שרירותי כלשהו ∀μΦμ --> Φv

• לא נכתוב V ליד הפירוק (כדי לסמן שהשלמנו אותו), אלא נעשה קו ' - ' ולאחריו נכתוב על איזה קבועים כבר הדגמנו את הפסוק

• ∀x(Ax→Bx) -- a, b
• אם נוסף לנו c בהמשך:

• ∀x(Ax→Bx) -- a, b, c

• חשוב לעקוב, בעיקר לפני שאנחנו קובעים כי ענף הוא פתוח (יש לוודא שאין עוד פעולות)

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

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

סדר פעולות

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

3. כלל שלילת הכמת הכולל

¬∀μΦμ הופך ל- ∃μ¬Φμ

• אנחנו בעצם ממירים את המשמעות של כמת כולל שלול לצורה של כמת ישי עם שלילת הפרדיקט: "לא כל u הוא פרדיקט Φ" הופך ל-"יש u שאינו פרדיקט Φ".
• מתאר לעצמי שממשיכים ע"י פירוק הכמת הישי, לפי הכלל שלמדנו

4. כלל שלילת הכמת הישי

¬∃μΦμ הופך ל- ∀μ¬Φμ

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

[[תרגילים - פרק 9 🏋️#תרגיל א#|תרגיל א]]

חילוץ מודל מענף פתוח

• ענף פתוח/קבוצה קונסיסטנטית מלמד אותנו שישנו פשר לפיו כל הקבוצה אמתית.
• לפשר הזה קוראים מודל

• כיצד מחלצים את המודל?

• הגדרה:

  פשר π הוא מודל של קבוצת הפסוקים T אם ורק אם כל פסוק מהקבוצה T אמיתי בפשר π

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

• זה מלמד אותנו איזה פריטים יש בדומיין, ולאילו אקסטנציות (לתחום של אילו פרדיקטים) כל אחד מהם משתייך או לא משתייך ![[Pasted image 20250125163056.png]] ![[Pasted image 20250125163102.png]]

• לפי סדר פעולות:

• בוחנים את כל האטומיים והאטומיים השלולים על הענף הפתוח
• הדומיין של המודל כולל את כל הקבועים המופיעים בפסוקים האלה
• פסוק אטומי מלמד אותנו שהקבוע המופיע בו הוא איבר באקסטנציה של הפרדיקט המתאים. למשל Pa מלמד אותנו ש-a נכלל באקסטנציה של P

• פסוק אטומי שלול מלמד אותנו את ההפך - ¬Pa מלמד אותנו ש-a אינו איבר באקסטנציה של P

• כשאנחנו מוכיחים תקפות או אי-תקפות, אם הגענו לעץ פתוח עבור ההנחות + שלילת המסקנה, המודל שנחלץ מהענף הוא פשר שמוכיח את אי-תקפות הטיעון

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

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

[[תרגילים - פרק 9 🏋️#תרגיל ב#|תרגיל ב]]

עצים אינסופיים

• בבניה של עץ אמת עבור קבוצת פסוקים בתחשיב הפסוקים, תמיד נגיע לעץ שלם - כלומר כזה שלא ניתן יותר להפעיל עליו כללים
• בתחשיב הפרדיקטים, אנחנו יכולים להיכלא בעץ רקורסיבי, שתמיד יהיו כללים נוספים להפעיל עליו
• זה בגלל השילוב של כללי ההדגמה: הדגמה ישית תמיד דורשת שנמציא קבוע, והדגמה כוללת תמיד דורשת שנדגים עבור כל קבוע;
• במקרים מסוימים שבהם יש לנו כמת ישי בתוך הטווח של כמת כולל, אנחנו ניקלע ללופ:
• תחילה נצטרך להדגים את הכולל עבור a
• אח"כ נצטרך להדגים את הישי עבור a ו-b
• אח"כ נצטרך להדגים את הכולל עבור b
• אח"כ נצטרך להדגים את הישי עבור b ו-c
• אח"כ נצטרך להדגים את הכולל עבור c
• את הישי עבור c ו-d וכן הלאה

![[Pasted image 20250125192056.png]]

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

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

• לסיכום, שיטת העצים בתחשיב הפרדיקטים מאפשרת להוכיח שקבוצת פסוקים לא-קונסיסטנטית היא אכן כזו, ע"י הצגת עץ סגור; אבל היא לא מאפשרת לקבוע עבור כל קבוצה נתונה אם היא קונסיסטנטית או לא.

[[תרגילים - פרק 9 🏋️#תרגיל ג#|תרגיל ג]]

דדוקציה טבעית בתחשיב הפרדיקטים

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

כלל ההכללה הישית - Existential Generalization (אבריבציה E.G.)

• ניתן להוסיף כמת ישי לכל פרדיקט עם קבוע אישי או עם משתנה.
• אם נתון Fa, אפשר לגזור ממנו "יש x עבור Fx"
• ∃xFx כלומר:

• צורה כללית: Φμ ∴∃xΦx

• מדובר בכלל היסק - לעומת כללי החילוף, לא ניתן להפעיל אותו על חלק בנוסחה, ולא ניתן להפעיל אותו "לכיוון השני" (לא נוכל לגזור מ-"יש x עבור Fx" ספציפית את Fa למשל)

• אפשר גם להשתמש בכלל כשיש משתנים וקבועים יחד תחת הפרדיקט, כך שהמשתנים נשארים בצורה החדשה: Fay ∴∃yFay

הוא צעד תקין.

• אפשר גם לקחת פסוק עם כמת שיש בו עוד משתנה או קבוע, ככה: ∃yGay ∴∃x∃yGxy

• כשאומרים שאי אפשר להפעיל על חלק מנוסחה, הכוונה היא שיש להפעיל כך: Fx→Gx Ez(Fz→Gz) ולא על הרישה או הסיפה בלבד לעולם.

• (אפשר היה להשאיר את המשתנה x כמו בדוגמה עם Fay, ואפשר גם להחליף את כל המופעים - באותו אופן Fay יכל להפוך ל-Faz למשל).
• חשוב לשים לב שכל המשתנים שנציב יהיו קשורים ע"י הכמת שהוספנו!

כלל ההדגמה הכוללת - Universal Instantiation (אבריבציה U.I.)

• קובע שאם יש לנו ביטוי בטווח של הכמת הכולל, ניתן לגזור אותו ללא הכמת עבור כל קבוע או משתנה.
• זאת בתנאי שכל המופעים של המשתנה שהיו קשורים ע"י הכמת הכולל, יהיו חופשיים בצורה החדשה.
• ההיגיון הוא פשוט - אם הפרדיקט F נכון עבור כל x בתחום הדיון, אז ברור שאפשר לכתוב כל קבוע או משתנה תחת הפרדיקט F - גם Fx וגם Fa
• גם זה כלל היסק - ולא כלל חילוף

∀xΦx ∴Φμ כאשר x משתנה ו-μ הוא כל קבוע או משתנה

• חשוב להחליף את כל המופעים הקשורים ע"י הכמת, כך: ∀x(Fx→Hx) ∴Fa→Ha

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

  • ∀x∃y(Ax∨¬Ay) נניח שנתון
  • יש לנו שני כמתים שהטווח שלהם הוא עד סוף הנוסחה - אז כשנפעיל את הכלל, נצטרך לוודא שהמשתנה x הוא מופע חופשי בתוצאה.
  • ∃y(Az∨¬Ay)
  • (לא נחליף אותו ב-y כי הוא לא יכול להיקשר ע"י הכמת הישי! לכן z)
  • יכל גם להישאר x...
  • על אותו משקל - משתנים שלא מחליפים עם הכלל נשארים קשורים או חופשיים, כמו שהיו לפני הפעלת הכלל!

• לזכור שאפשר "להמציא" איזה משתנה שרוצים... אם יש

• ∀x(Ax→Bx)
• ולנו יכול לעזור נניח
• Ac→Bc
• אפשר פשוט להחליט שאנחנו מפעילים את הכלל כדי להציב c...

[[תרגילים - פרק 9 🏋️#תרגיל ד#|תרגיל ד]]

כלל שלילת הכמת - Quantifier Negation (אבריבציה Q.N.)

• אותו כלל שאנחנו מכירים מ[[9 - שיטות סינטקטיות בתחשיב הפרדיקטים#3. כלל שלילת הכמת הכולל#|שלילת הכמת הישי ושלילת הכמת הכולל]] - מדובר פשוט בשקילות לוגית, מהסוג של "אין x עבור = כל x אינו"; ומהסוג של "אף x אינו = יש x שאינו" (הכוונה היא שמחליפים כמת ישי שלול בכמת כולל שהטווח שלו שלול, והפוך עם כמת כולל שלול)

כלל ההכללה הכוללת - Universal Generalization (אבריבציה U.G.)

• חידוד חשוב: יכול להיות שהופעלו עוד כללים אחרי U.I... ∀x(Gx→Fx) למשל היה לנו הפעלנו U.I בשביל Gx→Fx ואז הצבנו עם C.P. את Gx בשביל להוציא Fx ∀x(Fx) אז אפשר לעשות
• השאלה האמתית היא אם המשתנה היה קשור ע"י כמת כולל בצורתו המקורית.
• והמשמעות היא שרק הנחות (אם רגילות ואם מותנות - CP) הן מקור למשתנה שאי אפשר להכליל ב-U.G.

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

Φμ ∴∀xΦx

• ההסתייגות (לא תמיד ניתן להפעיל):
• יש שתי אפשרויות שבהן יהיה לנו מופע חופשי של משתנה:

• הוא תוצאה של הפעלת הכלל U.I., ומהווה מראש הדגמה של הכללה, אז במקרה כזה ברור שניתן ללכת הלוך-וחזור מ- ∀xGx ל- Ga ואז לעשות את הדרך בחזרה: Ga ל- ∀xGx

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

• הכוונה בכך שגם בתוצאה של הפעלת הכלל לא יכול להיות משתנה חופשי, הוא שגם המשתנה המקורי (נניח x כחלק מ-Gx) צריך להיות חופשי, וגם התוצאה של ההכללה: ∀yGy אם הכללנו את Gx לצורה של: זה בסדר כי y לא חופשי. ∀yGz יהיה לא תקין

![[Pasted image 20250127103130.png]]

לא ברור מהחוברת... נראה לי שההפעלה של הכלל בסעיף 4 לא תקינה כי מדובר במסקנה של ה-C.P... כלומר במסקנה שכן "שייכת" לטיעון הכולל

• בקיצור לזכור, צריך שבהנחה שהכלל מופעל עליה יהיה מופע חופשי שהוא תוצאה של הדגמה, ושבתוצאה של הפעלת הכלל לא יהיה מופע חופשי של המשתנה החדש כלל
• עוד חשוב לזכור: אם הפעלנו C.P. - כל מופע חופשי של משתנה תחת ההנחות המותנות אינו נחשב! כמו כאן:
• כלומר שרק ההנחה המותנית המקורית שלנו, ולא הפיתוחים שלה, נחשבים לצורך בדיקת מופעים חופשיים עבור הכלל U.G.
• ![[Pasted image 20250127103750.png]]

כלל ההדגמה הישית - Existential Instantiation (אבריבציה E.I.)

• הכלל המאתגר ביותר, בגלל שמטענה כמו "קיים x ש..." אי אפשר לגזור שום טענה אישית (מהסוג של "פרט a הוא...").
• המשמעות היא שאי אפשר להדגים טענה ישית, וזו בעיה כי אנחנו צריכים כלי לפירוק של טענות ישיות בדדוקציה הטבעית.
• הפיתרון הוא לכתוב הדגמה של הנוסחה הישית כהנחה של הוכחה מותנית
• ∃vΦv אם יש לנו את זה ו-v הוא משתנה
• Φμ אפשר לעבור לכזה כאשר μ הוא אחד משני דברים:
• משתנה ללא מופע חופשי בשורה שקודמת להדגמה

• קבוע חדש לגמרי (ללא מופע קודם)

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

• בניגוד להוכחה מותנית רגילה, את השורה האחרונה של הקופסה נעתיק לבסוף בלי ליצור התניה שמתחילה בהנחה המותנית הראשונה - ננמק באמצעות השורה שההדגמה הישית הופעלה עליה, טווח הפסוקים של ההוכחה המותנית + E.I.

  k. ∃μΦμ
  m. Φv
  ...
  n. α
  n+1. α k, m-n E.I.
  

הכלל קובע כי אסור להדגים על־ידי שימוש במשתנה שיש לו מופע חופשי בשורה כלשהי הקודמת לשורה שהדגמנו בה. למשל, אם בשורה כלשהי יש מופע חופשי למשתנה x, כמו בנוסחה Ax→Bx , אז הנוסחה הישית 7xFx לא יכולה להיות מודגמת על־ידי שימוש במשתנה x — אי אפשר לכתוב Fx כמקרה הדגמה — אך ניתן להשתמש במשתנה אחר שאין לו כל מופע חופשי באיזושהי שורה לפני ההדגמה. וכך גם עם קבועים. אם הקבוע a מופיע בשורה הקודמת להדגמה, לא ניתן להדגים עם

• איך זה שאפשר להשתמש ב-CP באופן הזה?

  • זה בגלל שהצורה הכללית ∀μ(Φμ→α) זהה לצורה הכללית ∃μ(Φμ→α) ("כל פרט הוא ערך עבור הפרדיקט" שקול לוגית ל- "יש ערך עבור הפרדיקט...") (אבל זה לא אמור לעבוד הפוך... אבל שקילות היא לא הדדית?)

• בפועל אנחנו כן מסיימים את ה-C.P. המיוחד של E.I. בפסוק התניה, אבל ההתניה תמיד תהיה

• Φμ→α
• וזה תמיד יגיע מצורה מקורית של
• ∃μΦμ
• לכן תמיד אפשר להכליל באמצעות U.G. ולקבל
• ∀μ(Φμ→α)
• שהוא כאמור שקול לוגית ל-
• ∃μΦμ→α
• ומאחר שהתחלנו מהצורה המקורית
• ∃μΦμ
• אנחנו יכולים להשתמש ב-M.P. כדי לגזור את התוצאה הפשוטה של ההוכחה המותנית - `α

סיכום ותיקון של הסייגים לכללים

סיכום ההסתייגויות: E.I. הדגמה ישית המשתנה שאנחנו בוחרים להדגים באמצעותו (משבצים בתוצאה של הכלל) הוא ללא מופע חופשי בשורה קודמת בכלל. בקופסאות סגורות לא נחשב. ואם הוא קבוע אז הוא חדש לגמרי. ביציאה מ-E.I: אסור שיהיה לנו משתנה חופשי שהוא המשתנה שהדגמנו באמצעותו (לשים לב - זה שבחרנו לתוצאת הכלל, לא זה שהפעלנו עליו!)

U.I. הדגמה כללית המשתנה שנבחר יהיה חופשי בכל מקום שהוא קשור בצורה המקורית, ולא יקשר במקרה ע"י כמת שעדיין לא פורק U.G. הכללה כוללת המשתנה שנפעיל עליו את הכלל: ללא מופע חופשי בשום הנחה קודמת ורלוונטית (אם זו מותנית (CP או EI) שיצאנו מהקופסה שלה - היא לא נחשבת.) לשים לב - הנחה ולא סתם שורה. המשתנה שנבחר (להחליף בו): כל משתנה... כל עוד אין לו מופע קשור בתוצאה של הפעלת הכלל (מצבים מיוחדים... בד"כ הוא ייקשר כמובן ע"י הכמת שנוסיף.)

תקף להנחה מותנית כל עוד אנחנו בטווח שלה - אם יצאנו מהקופסה, הקופסה לא קיימת

E.G. הכללה ישית - אין תנאים, כל עוד יש פרדיקט עם ערך