5.1.4.2. כללי הסקכאשר יש בידינו את האקסיומות, נוכל באמצעות כללי ההיסק לבנות טענות נוספות. כלל הסק עבור הרכבה סדרתית דוגמא לשימוש: רוצים להוכיח את הטענה הבאה: שימוש באקסיומת ההצבה: מסתכל על הביטוי
מצידו הימני: ניקח את הביטוי מצד שמאל, ונפעיל שוב את
אקסיומת ההצבה עם ההצבה כעת נשתמש בהרכבה SEQ לשרשור התוצאות: נשתמש שוב באקסיומת ההצבה כאשר מימין אנו שמים את הצד השמאלי של (3). לסיום נבצע שוב SEQ והוכחנו את הטענה שהתבקשנו להוכיח. כלל הסק עבור if הכלל נאות: כל חישוב של כלל הסק עבור while
כלל הסק דוגמא לאי-שלמות ללא CONS: נביט בטענה הבאה: הטענה אומרת "אם יודעים כי הטענה נכונה בגלל שאנו מדברים על נכונות
חלקית, והלולאה לעולם אינה עוצרת. אנו רוצים להוכיח את הטענה הנכונה, והדרך היחידה
ללא טענה זו אינה נכונה ומכיוון שמע' ההוכחה נאותה לא נוכל להוכיח אותה. קיבלנו שלילה של השלמות, כי לא ניתן להוכיח את הטענה ממנה התחלנו, שהיא טענה נכונה. נראה כעת איך מוכיחים את הטענה כאשר CONS כן חלק ממערכת ההוכחה. כאמור, אנו רוצים להוכיח נבחר את הטענה הנכונה הבאה: נפעיל REP: נשתמש פעמיים באקסיומת ARITH: נפעיל CONS על 2,3,4 ונקבל את הטענה אותה אנו מעוניינים להוכיח. צריך לשים לב כי לא הראנו כי הוספת CONS גרמה למערכת להיות שלמה. הראנו כי הבעיה שהיתה קיימת לפני הוספת CONS (לא יכולנו להוכיח טענה נכונה) נפתרה.
אין תגובות!
|
תוכן העניינים:
קישורים רלוונטיים:שיתוף: |