עקביות

הגדרה

קבוצת פסוקים (קבוצת הנחות) plot:[X] תקרא עקבית אם plot:[X
ot  vdash F].

משפט

לכל קבוצת פסוקים plot:[X], מתקיים כי plot:[X] עקבית אמ"מ כל תת קבוצה סופית של plot:[X] היא עקבית.

משפט

קבוצת פסוקים plot:[X] היא עקבית אמ"מ לא קיים פסוק plot:[alpha ] כך ש: plot:[X vdash alpha ] וגם plot:[X vdash 
eg alpha ].

משפט

קבוצת פסוקים plot:[X] היא עקבית אמ"מ קיים פסוק plot:[alpha ] כך ש-plot:[X
ot  vdash alpha ].

הוכחה:

plot:[ Leftarrow ] X עקבית plot:[ Leftarrow ] plot:[X
ot  vdash F]plot:[ Leftarrow ] קיים plot:[alpha  = F] כך ש-plot:[X
ot  vdash alpha ].

plot:[ Rightarrow ] נניח ש-X איננה עקבית. נוכיח: לכל plot:[alpha ], מתקיים כי plot:[X vdash alpha ]. plot:[X] אינה עקבית plot:[X vdash F Leftarrow ]. יהי plot:[alpha ] פסוק כלשהו. נראה כי plot:[X vdash alpha ]:

n.             plot:[F]

קיימת סדרת הוכחה כי plot:[X vdash F]

n+1.        plot:[F
   	o left( {left( {alpha  	o F} 
ight) 	o F} 
ight)]

אקסיומה 1

n+2.        plot:[left(
   {alpha  	o F} 
ight) 	o F]

MP(n, n+1)

n+3.        plot:[left(
   {left( {alpha  	o F} 
ight) 	o F} 
ight) 	o alpha ]

אקסיומה 3

n+4.        plot:[alpha
   ]

MP(n + 2, n + 3)

plot:[ Leftarrow ] לכל plot:[alpha ], מתקיים plot:[X vdash alpha ].

מתי X לא עקבית

  1. X לא עקבית אם קיים פסוק plot:[alpha ] כך ש: plot:[X vdash alpha ] וגםplot:[X vdash 
eg alpha ].
  2. X לא עקבית אם לכלplot:[eta ], מתקייםplot:[X vdash eta ].

טענה

plot:[F 
otin Dedleft( X 
ight) Leftrightarrow X
ot  vdash F].

משפט הנאותות הצר

לכל פסוק plot:[alpha ], אם plot:[ vdash alpha ] אזי plot:[ vDash alpha ]. (כלומר, כל פסוק יכיח הוא טאוטולוגיה).

  • משפט זה נותן לנו קשר בין סינטקס לסמנטיקה.

משפט הנאותות הרחב

לכל קבוצת פסוקים plot:[X] ולכל פסוק plot:[alpha ]: אם plot:[X vdash alpha ] אזי plot:[X vDash alpha ].

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

האם קיימת קבוצה עקבית? שאלה שקולה: האם הקבוצה הריקה היא עקבית (כי הקבוצה הריקה מוכלת בכל קבוצה). נראה כי plot:[phi ] עקבית, כלומר plot:[F 
otin Dedleft( phi  
ight)].

נשתמש במשפט הנאותות הצר. plot:[F] אינו יכיח, כי הוא לא טאוטולוגיה. מכאן plot:[phi ] עקבית.

שימושים למשפט הנאותות: משפט הנאותות הוא הכלי שבאמצעותו מוכיחים אי יכיחות ואי עקביות. על מנת להוכיח כי plot:[X
ot  vdash alpha ] נראה plot:[X
ot  vDash alpha ].

משפט שקול למשפט הנאותות: אם plot:[X] ספיקה, אז plot:[X] עקבית.

הוכחה: נניח בשלילה כי plot:[X] לא עקבית, אזי plot:[X vdash F]. לפי משפט הנאותות plot:[X Leftarrow X vDash F] לא ספיקה (כל השמה שמספקת את plot:[X] מספקת את plot:[F], אך לא קיימת כזו). סתירה לנתון.

דוגמא

תהי הקבוצה plot:[Sigma  = left{ {{p_i} 	o
 {p_{i + 1}}|i in mathbb{N}} 
ight}]. נוכיח שקבוצה זו הינה עקבית.

צ"ל: plot:[Sigma 
ot  vdash F]. לפי משפט הנאותות מספיק להראות כי plot:[Sigma 
ot  vDash F]. כלומר: צריך להראות השמה plot:[z] המספקת את plot:[Sigma ] וגם מקיימת plot:[ar zleft( F 
ight) = 0]. נבחר את ההשמה plot:[{z_F}] (השמה הנותנת 0 לכל האטומים). ניתן לראות בקלות שלכל plot:[alpha  in Sigma ] מתקיים plot:[ar zleft( alpha  
ight) = 1]. plot:[{z_F} Leftarrow ] מספקת את plot:[Sigma ] אבל plot:[{ar z_F}left( F 
ight) = 0].

ומכאן: קיימת השמה המספקת את plot:[Sigma ] אך לא את plot:[F] plot:[Sigma  
e F Leftarrow ].



הגדרה

ניסוח 1: נאמר שקבוצת פסוקים X היא עקבית מקסימלית אם X עקבית ולכל פסוק plot:[alpha ] כך ש-plot:[X
ot  vdash alpha ] מתקיים כי plot:[X cup left{ alpha  
ight}] לא עקבית.

ניסוח 2: X עקבית מקסימלית אם X עקבית ולכל פסוק plot:[X vdash alpha ] או plot:[X vdash alpha  	o F].

לא עקבית

עקבית

עקבית מקסימלית

plot:[egin{gathered}
     X vdash
   alpha  hfill
   \
     X vdash
   alpha  	o F hfill
   \ 
   end{gathered}
   ]

plot:[egin{gathered}
     X vdash
   alpha  hfill
   \
     X
ot 
   vdash alpha  	o F hfill
   \ 
   end{gathered}
   ]

plot:[egin{gathered}
     X
ot 
   vdash alpha  hfill
   \
     X vdash
   alpha  	o F hfill
   \ 
   end{gathered}
   ]

plot:[egin{gathered}
     X
ot 
   vdash alpha  hfill
   \
     X
ot 
   vdash alpha  	o F hfill
   \ 
   end{gathered}
   ]

משפט

תהי X קבוצה עקבית, אזי קיימת קבוצה עקבית מקסימלית Y, כך ש-plot:[X subseteq Y].

הרעיון: נרצה לעבור על כל הפסוקים ולדאוג של-X תהיה דעה על כל פסוק.

טענה: תהי X קבוצה עקבית. X עקבית מקסימלית אמ"מ לכל זוג פסוקים plot:[eta ,gamma ] מתקיים plot:[X vdash 
eg eta  Leftrightarrow X vdash eta  	o gamma ] אוplot:[X vdash gamma ].

טענה: אם X היא קבוצה עקבית מקסימלית, אז X ספיקה.

משפט

לכל קבוצת פסוקים X, X עקבית אמ"מ X ספיקה.

הוכחה: (כיוון אחד בלבד): נניח כי X עקבית. אזי קיימת קבוצה עקבית מקסימלית Y כך ש-plot:[X subseteq Y] plot:[ Leftarrow ]Y ספיקה. כלומר קיימת השמה plot:[{Z_Y}] המספקת את plot:[Y]. plot:[{Z_Y} vDash Y]. מאחר ומתקיים כי plot:[X subseteq Y] הרי ש-plot:[{Z_Y} vDash X]. ראינו שכל קבוצה עקבית היא ספיקה.

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

לכל קבוצת פסוקים X ולכל פסוק plot:[alpha ], אם plot:[X vDash alpha ] אזי plot:[X vdash alpha ].

מסקנה ממשפט השלמות והנאותות – משפט הקומפקטיות

תהא X קבוצה. X ספיקה אמ"מ כל תת קבוצה סופית שלה היא ספיקה.

שימוש: במשפט זה נשתמש פעמים רבות כדי להפוך בעיות אינסופיות לבעיות סופיות.

קשר בין סינטקס לסמנטיקה:

הגדרה

השמה המספקת קבוצה plot:[Sigma ] תיקרא מודל של plot:[Sigma ].

נסמן: plot:[Mleft( Sigma  
ight) =
 {M_Sigma } = left{ {{	ext{all models of }}Sigma } 
ight} = left{ {z|Z
 vDash Sigma } 
ight}].

משפט

אם לקבוצה plot:[Sigma ] יש מודל, אז היא עקבית.

משפט

קבוצת פסוקים X היא עקבית מקסימלית אמ"מ קיימת בדיוק השמה אחת המספקת את X.

ניסוח שקול: X עקבית מקסימלית אמ"מ plot:[left| {Mleft( X 
ight)} 
ight| = 1].

דוגמאות

קבוצות מקסימליות ולא מקסימליות:

הקבוצה:

עקבי מקסימלי?

plot:[Sigma  =
   left{ {{p_i}|i in mathbb{N}} 
ight}]

מקסימלי. plot:[Mleft( Sigma  
ight) = left{ {{z_T}}
   
ight}]

plot:[Sigma  =
   left{ {
eg {p_i}|i in mathbb{N}} 
ight}]

מקסימלי. plot:[Mleft( Sigma  
ight) = left{ {{z_F}}
   
ight}]

plot:[left{ {{p_{2i}}
   	o {p_{2i + 1}}|i in mathbb{N}} 
ight}]

לא מקסימלי. כל "השמת מדרגה" תספק את הקבוצה.

plot:[left{
   {{p_i} vee {p_{i + 1}}|i in mathbb{N}} 
ight}]

לא מקסימלי

plot:[left{ {
eg
   left( {{p_i} vee {p_{i + 1}}} 
ight)|i in mathbb{N}} 
ight}]

מקסימלי

plot:[left{ {
eg
   {p_i} vee 
eg {p_{i + 1}}|i in mathbb{N}} 
ight}]

לא מקסימלי



צביעה של גרפים

בהינתן גרף G עם plot:[left( {V,E} 
ight)] צביעה חוקית בשני צבעים היא צביעה בה כל צומת נצבע באחד הצבעים, ולשני צמתים שכנים צמתים שונים. גרף הוא 2-צביע אם קיימת לו צביעה חוקית בשני צבעים.

בהינתן גרף plot:[Gleft( {V,E} 
ight)] נתרגם את השאלה לשאלה בפסוקים:

  • לכל צומת נתאים אטום.
  • לכל קשת plot:[e = {v_i}{v_j}] נתאים פסוק: plot:[{alpha _{ij}} = {p_i} oplus {p_j}] כאשר plot:[{alpha _{ij}} equiv left( {{p_i} wedge 
eg {p_j}}
      
ight) vee left( {
eg {p_i} wedge {p_j}} 
ight)].
  • נגדיר: plot:[{X_G} = left{ {{alpha
      _{ij}}|left( {i,j} 
ight) in E} 
ight}].

טענה 1: G הוא גרף 2-צביע אמ"מ plot:[{X_G}] ספיקה.

טענה 2: גרף G הוא 2-צביע אמ"מ כל תת גרף סופי שלו הוא 2-צביע.

הוכחה:

plot:[ Leftarrow ] נתון: הגרף הוא 2-צביע plot:[ Leftarrow ] הצביעה הינה צביעה חוקית עבור כל תת גרף.

plot:[ Rightarrow ] נתון: כל תת גרף סופי הוא 2-צביע. נוכיח כי G הוא 2-צביע. מספיק שנוכיח כי plot:[{X_G}] ספיקה. על פי הקומפקטיות מספיק שנראה שכל תת קבוצה סופית של plot:[{X_G}] ספיקה. תהי plot:[D subseteq {X_G}] סופית.

נסמן ב-plot:[{V_D}] את קבוצת הצמתים המופיעים ב-plot:[D]. נסמן ב-plot:[{G_D}] את תת הגרף המתאים ל-plot:[{V_D}]. plot:[{G_D}] הוא תת גרף סופי (מכיוון ש-plot:[D] סופית). plot:[{G_D}] הוא 2-צביע ולכן plot:[{X_{G,D}}] ספיקה. plot:[D subseteq {X_{G,D}}] כי plot:[D] מתארת חלק מהקשתות בין הצמתים ב-plot:[{V_D}] ולכן גם plot:[D] ספיקה.

תבנית (הוכחות כגון צביעת גרף)

  1. תרגום הבעיה לפסוקים. נחפש plot:[{X_G}] כך ש-plot:[{X_G}] ספיקה אמ"מ G מקיימת את התכונה.
  2. משתמשים בזהירות במשפט הקומפקטיות.


תגיות המסמך:

מאת: bentz

תיקון

מציעה להחליף את
(a¬)
ב

שכן (a¬) אינו פסוק
מאת: משה ב

סמנטיקה

שיתוף:
| עוד