לדלג לתוכן

הדפסות 9 דדוקציה ועצים עם כמתים

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

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

יש הרבה הוכחות שדורשות לסדר נכון את השלבים (כדי לא להפעיל סייגים של כללי הכמתים) - לרשום בצד מה "יש לי" ולתכנן להיות מאוד מודע לשרשראות של M.P. ו-M.T. גם פה... ובנוסף להיות מודע ל-QN ולהמרות של משתנים...

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

לעקוב אחרי ההתניות! לא לשכוח סגירות של קופסאות

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

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 אינו פרדיקט Φ"
  • בשני הכללים, אנחנו משתמשים בשקילות לוגית כדי להגיע לצורה של הכמת שאינה שלולה חד

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

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

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 אינו פרדיקט Φ"
  • בשני הכללים, אנחנו משתמשים בשקילות לוגית כדי להגיע לצורה של הכמת שאינה שלולה

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

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

  • הגדרה:

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

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

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

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

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

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

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

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

דדוקציה

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

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

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

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

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

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

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