שאלה בתחשיב הפסוקים

[ohad]

http://i.imm.io/S2cp.png

(אנו במערכת http://www.codecogs.com/gif.latex?WFF_%7B%5C%7B%5Crightarrow,%5Clnot%5C%7D%7D , הפונקציה subst הוגדרה בעבר והיא הצבה כלשהי של פסוקים במקום משתנים)

 

ברורה לי הנכונות של הטענה, רק לא ברור איך בדיוק להוכיח זאת...

האם אפשר לעשות אינדוקציה על אורך סדרת ההוכחה של http://www.codecogs.com/gif.latex?%5Calpha ? ואיך בדיוק עושים את זה?

 

תודה!

 

 

תודה מראש ל incog :-)

 

 

[incog]

קצת קשה לעזור בלי לדעת בדיוק מה זו הפונקציה subst...

[ohad]

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

http://i.imm.io/S2vi.pngבתרגיל ההוא הוכחנו שהתמונה שלה היא פסוקים ב WFF (הטווח בהגדרה יותר רחב), ועוד כמה תכונות שלא נראות לי רלוונטיות פה.

[incog]

ההגדרה הזו ממש בלבלה אותי ויש בה טעות (צריך למחוק את החלק השני בבסיס, O הזה הוא לא WFF ).
אז תחת ההנחה שהבנתי נכון, הפתרון הוא כזה:
ראשית כל תוכיח שאם A טאוטולוגיה אז גם subset(A,s)   d  זו טאוטולוגיה (תנסה לחשוב על זה קצת)

כעת אם: Sigma|- A , אז ממשפט הדדוקציה קיימים A_1,.,,A_n  בסיגמא כך ש:
A_1^A_2^...^A_n->A  , זו טאוטולוגיה.
לכן אם תיקח subset של זה זו גם תהיה טאוטולוגיה. וכעת תשתמש בתכונה של הפונקציה ותקבל כי:
subset(A_1)^...^subset(A_n)->subset(A)   d  זו טאוטולוגיה.
ולכן לפי הגדרה subset(sigma)|-subset(A)   d

 

[ohad]

בגדול נראה לי שהבנתי, אני אשב על זה יותר מחר. 2 שאלות בכל זאת:

1. כשכתבת בסוף "לפי ההגדרה" הכוונה היא שוב לפי משפט הדדוקציה רק בכיוון ההפוך לא?

2. כיוון ההוכחה שאני הצעתי לא טוב? יש לאלפא סדרת הוכחה, ואם תעשה לכל איבר בסדר subst תקבל גם סדרת הוכחה"שקולה" ותקפה.

 

תודה!

[incog]

1) כן.
2) לא שמתי לב למה שרשמת, הכיוון שלך הוא בהחלט כיוון נכון (למעשה הוא שקול לחלוטין למה שכתבתי ומצריך בדיוק אותה כמות עבודה).

עדיין בדיוק כמו שציינתי מקודם אתה תצטרך קודם להוכיח טענת עזר שאם A טאוטולוגיה אז subst(A) גם טאוטולוגיה ואז תוכיח באינדוקציה:
טענה: אם A_0,..,.A_n סדרת הוכחה של סיגמא, אזי subst(A_0),..,subst(A_n) d סדרת הוכחה מ- subst(Sigma) d 
אם יש לך סדרה:
A_0,..,A_n,  נסמן את הסדרה החדשה (לאחר הפעלת subst)  ב- B_0,..,B_n. צריך להראות שזו אכן סדרת הוכחה:
עבור A_0 מתקיים בהכרח שזו טואטולוגיה או שייך לסיגמא, במקרה הראשון תשתמש בטענת העזר, במקרה השני זה מיידי.
כעת נוכיח עבור סדרה באורך n:
לפי הנחת האינדוקציה: B_1,..,B_n-1  היא סדרת הוכחה מ- subst(Sigma) d לכן על מנת לסיים אתה צריך להוכיח ש: B_n הוא או טאוטולוגיה או מישהו מ- subset(Sigma) d
או התקבל על ידי ניתוק רישא מ- B_i,B_k עבור i,k<n:
 אם A_n טאוטולוגיה או שייך לסיגמא זה כמו במקרה הבסיס, אחרת: A_n מתקבל על ידי מודוס פוננס, כלומר קיימים בסדרה הזו: A_k=A_i->A_j  ו- A_j  , לפי הנחת  האינדוקציה: subset(A_j)    ו- subst(A_k)=subset(A_i)->subset(A_j) d  ולכן תקבל ש: B_n מתקבל מ- B_k ו- B_j  על ידי ניתוק רישא.
וסיימנו את טענת האינדוקציה.

כעת מהטענה הזו נובע מידית מה שצריך להוכיח.

שוב פעם, עיקר הקושי (הטכני) זה להוכיח את הטענה שאם: A טאוטולוגיה אזי גם subset(A) d טאוטולוגיה, זה ברור לחלוטין אינטואיטיבית, אבל זה לא פשוט להוכיח את זה פורמלית וגם לי לקח קצת זמן לחשוב על זה.

[ohad]

עבור A_0 מתקיים בהכרח שזו טואטולוגיה או שייך לסיגמא, במקרה הראשון תשתמש בטענת העזר, במקרה השני זה מיידי.

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

[incog]

כן, זה אכן מפשט בהרבה.

[ohad]

זה מה שיצא:

http://i.imm.io/S7Hx.png

אתה חושב שצריך לפרט יותר למה הצבה באקסיומה היא אקסיומה (זה נראה לי ממש טריוויאלי)?

 

שוב תודה!!

[incog]

אולי להוסיף עוד שורה (זה נובע מהגדרת הסגור והעובדה שהאקסיומה היא סכמטית), אבל זה לא דורש יותר מידי פירוט.