הועלה לאתר:  
מספר עמודים: 25
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

לוגיקה - סיכום נקודות

סיכום מאת: ניר אדר

גדירות

בהינתן קבוצת פסוקים plot:[Sigma ], plot:[Sigma ] מגדירה את קבוצת ההשמות המספקות אותה. עבור קבוצת פסוקים plot:[Sigma ], קבוצת המודלים של plot:[Sigma ] מסומנת ב-plot:[Assleft( Sigma  ight)] ומוגדרת plot:[Assleft( Sigma  ight) = left{ {z|z vDash Sigma } ight}].

טענה: אם plot:[{Sigma _1} subseteq {Sigma _2}] אז plot:[Assleft( {{Sigma _2}} ight) subseteq Assleft( {{Sigma _1}} ight)].

שאלה: בהינתן קבוצת השמות plot:[K], האם קיימת קבוצת פסוקיםplot:[Sigma ] שמגדירה את plot:[K], כלומר plot:[Assleft( Sigma  ight) = K]? אם קיימת קבוצת פסוקים כזו נאמר כי plot:[K] גדירה. אם קיימת קבוצת פסוקים סופית שמגדירה את plot:[K] נאמר ש-plot:[K] גדירה באופן סופי.

כמה פסוקים יש? plot:[{aleph _0}]. כמה קבוצת פסוקים? plot:[{2^{{aleph _0}}}]. כמה קבוצות השמות? plot:[{2^{{2^{{aleph _0}}}}}].

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

דוגמאות

plot:[{K_1} = phi ]. האם הקבוצה גדירה? כן, למשל plot:[Sigma  = left{ {{p_1}, eg {p_1}} ight}].

plot:[{K_2}] הינה קבוצת כל ההשמות. כל קבוצת טאוטולוגיות מגדירה את plot:[{K_2}].

הוכחת אי גדירות

סכימת הוכחת אי גדירות של קבוצת השמות plot:[K]:

  1. נניח בשלילה כי plot:[K] גדירה על ידי קבוצת פסוקים plot:[X].
  2. נבחר קבוצת פסוקים מפורשתplot:[Y] שעבורה ידוע מהו plot:[Mleft( Y ight)].
  3. מראים כי plot:[X cup Y] לא ספיקה, על ידי plot:[Mleft( Y ight) cap Mleft( X ight) equiv Mleft( Y ight) cap K = phi ].
  4. מראים כי plot:[X cup Y] ספיקה באמצעות משפט הקומפקטיות:

    מראים שכל תת קבוצה סופיתplot:[D subseteq X cup Y] היא ספיקה. מראים השמה plot:[{z_D}] השייכת ל-plot:[K] כך ש: plot:[{z_D} vDash D]. (מסתמכים בבניית plot:[{z_D}] על האינדקס המקסימלי המופיע גם ב-plot:[D] וגם ב-plot:[Y].
  5. מ-3 ומ-4 אנו מקבלים סתירה: plot:[X] לא קיימת, ולכן plot:[K] לא גדירה.

הגדרה

נאמר שקבוצת השמות plot:[K] תלויה בקבוצת משתנים plot:[D subseteq left{ {{p_i}|i in mathbb{N}} ight}] אם קיימות השמות plot:[{z_1},{z_2}] שמזדהות על כל האטומים מחוץ ל-plot:[D] ומתקיים plot:[{z_1} in K] ו-plot:[{z_2} otin K].

הגדרה

נאמר שקבוצת אטומים plot:[S subseteq left{ {{p_i}|i in mathbb{N}} ight}] מהווה תומך לקבוצת השמות plot:[K] אם לכל שתי השמות plot:[{z_1},{z_2}] שמזדהות על כל האטומים בתוך plot:[S] (כלומר לכל plot:[{z_1}left( {{p_i}} ight) = {z_2}left( {{p_i}} ight),{p_i} in S]) אז plot:[{z_1} in K Leftrightarrow {z_2} in K].

דוגמא: plot:[K = left{ {z|zleft( {{p_i}} ight) = 1} ight}], plot:[{S_1} = left{ {{p_1}} ight},{S_2} = left{ {{p_1},{p_3},{p_4}} ight}].

הגדרה

נאמר שלקבוצת השמות יש תומך סופי אם קיים תומך לקבוצה בגודל סופי.

טענה

לקבוצה plot:[K] יש תומך סופי אמ"מ plot:[K] גדירה באופן סופי.

·       מהתומך הסופי ניתן ליצור מספר פסוקים סופי, שיתאר את התומך. פסוקים אלו יגדירו את plot:[Sigma ].

·       אם plot:[K] גדירה באופן סופי אז קיימת plot:[Sigma ] סופית המגדירה אותה. מפסוקי plot:[Sigma ] יש מספר סופי של אטומים. אטומם אלו מהווים תומך ל-plot:[K].

תגיות המסמך:

לפרק הקודםעקביות
לפרק הבאתחשיב היחסים
מאת: bentz

תיקון

מציעה להחליף את
(a¬)
ב
a¬
שכן (a¬) אינו פסוק
מאת: משה ב

סמנטיקה
שיתוף:
| עוד