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