משפט הקומפקטיות
משפט הקומפקטיות הוא משפט מרכזי בלוגיקה המתמטית, המאפשר לטפל במערכות אינסופיות של אקסיומות על ידי הבנת חלקים סופיים שלהן.
כמשפטים רבים אחרים מלוגיקה, קיימות למשפט זה שתי גרסאות: בתחשיב הפסוקים, ובלוגיקה מסדר ראשון.
בתחשיב הפסוקים המשפט קובע כי לאוסף פסוקים יש מודל אם ורק אם לכל תת-קבוצה סופית שלו יש מודל (הכוונה במודל של פסוק היא להשמה של ערך אמת לפסוקים האטומיים, המספקת את הפסוק). שמו של המשפט בא מקיומה של הוכחה טופולוגית עבורו, המתבססת על קומפקטיות של מרחב טופולוגי מסוים ומשפט טיכונוף.
את גרסת המשפט ללוגיקה מסדר ראשון הוכיח אנטולי מלצב ב-1936. בגרסה זו המשפט קובע שאם לכל תת קבוצה סופית של קבוצת פסוקים נתונה בשפה מסדר ראשון יש מודל, אז יש מודל לקבוצה כולה.
את המשפט ניתן להוכיח בעזרת אקסיומת הבחירה (וליתר דיוק, גרסה מוחלשת של אקסיומת הבחירה, כדוגמת למת העל-מסננים, מספיקה), ולכן הוא עשוי שלא להיות תקף כאשר מפתחים את תורת הקבוצות ללא אקסיומה זו.
הוכחות למשפט
הן בתחשיב הפסוקים והן בתחשיב היחסים, קיימות הוכחות רבות למשפט הקומפקטיות.
ההוכחה הנפוצה ביותר היא זו המסתמכת על משפט השלמות של גדל. נציג את עיקרי ההוכחה הזו בלוגיקה מסדר ראשון (קיימת גרסה דומה לתחשיב הפסוקים):
משפט הקומפקטיות הוא סמנטי במהותו (עוסק במודלים), ולא תחבירי (עוסק בהוכחות). הרעיון בהוכחה זו הוא להראות שמספיק להוכיח גרסה תחבירית של משפט הקומפקטיות: "בהינתן קבוצת פסוקים, אם כל תת-קבוצה סופית שלה היא עקבית, אז הקבוצה כולה עקבית". ההוכחה של הטענה הזו קלה מאוד ומסתמכת על כך שכל הוכחה היא סופית.
הקושי הוא, אם כן, לעבור לגרסה התחבירית הזו; הכלי שמאפשר לקשר בין סמנטיקה לתחביר הוא משפט השלמות של גדל, לפיו "עקביות" ו-"קיום מודל" הם היינו-הך. מרגע שתפסנו את האבחנה הזו, ההוכחה טריוויאלית.
נעיר שקיימת הוכחה של משפט השלמות של גדל מתוך משפט הקומפקטיות: משפט הקומפקטיות ומשפט השלמות של גדל שקולים במסגרת אקסיומות צרמלו-פרנקל לגרסה חלשה יותר של אקסיומת הבחירה, והיא למת העל-מסננים (לפיה כל מסנן על קבוצה כלשהי ניתן להרחבה לעל-מסנן).
כפי שציינו, קיימת הוכחה טופולוגית למשפט הקומפקטיות, ומכאן שמו. עיקרי ההוכחה: בתחשיב הפסוקים הסטנדרטי, קבוצות ההשמות המקיימות פסוקים נתונים הן קבוצות סגורות במרחב הטופולוגי הקומפקטי של כל ההשמות, ולכן אם החיתוך של כל מספר סופי מהן אינו ריק, אז גם החיתוך של כולן אינו ריק.
בלוגיקה מסדר ראשון, קיימת הוכחה נוספת ואלגנטית מתחום תורת המודלים, הנעזרת בעל-מכפלות ובמשפט Łoś.
ניתן להוכיח בקלות יחסית את גרסת המשפט לתחשיב הפסוקים מגרסתו בלוגיקה מסדר ראשון.
שימושים למשפט
בראש ובראשונה, ובדומה למשפטי לוונהיים-סקולם, משפט הקומפקטיות מעיד על חולשה כלשהי של הלוגיקה מסדר ראשון. באמצעותו ניתן למצוא תכונות שלא ניתנות להבעה באמצעות קבוצות של פסוקים מסדר ראשון. נדגים זאת: יישום טיפוסי של משפט הקומפקטיות הוא לבניית שדה סדור לא ארכימדי השקול אלמנטרית לשדה הממשיים. מכאן, תכונת הארכימדיות היא תכונה שלא ניתן להביע באמצעות לוגיקה מסדר ראשון.
יישום נוסף, המיוחס לסקולם, של משפט הקומפקטיות, הוא לבניית מודל בן מניה לא סטנדרטי של האריתמטיקה. מודל כזה הוא מבנה בן מניה השקול אלמנטרית למספרים הטבעיים בשפת אריתמטיקת פאנו (גרסה מסדר ראשון של מערכת פאנו), אך אינו איזומורפי להם. הדרך לבנות מודל כזה היא לצרף לתורה השלמה של הטבעיים את אוסף הנוסחאות: לכל מספר טבעי הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} .
נקבל אוסף מורחב של נוסחאות. כל תת-קבוצה סופית של אוסף זה היא עקבית (המספרים הטבעיים מהווים מודל שלה), ולכן יש מודל לאוסף כולו. (יתרה מכך, ממשפט לוונהיים סקולם היורד ניתן למצוא מודל כזה שהוא בן מניה). אם כן, מודל זה לא איזומורפי לטבעיים אך שקול אלמנטרית להם - זהו מודל לא סטנדרטי לאריתמטיקה.
מסקנה מעניינת היא שאקסיומת האינדוקציה אינה ניתנת לניסוח בלוגיקה מסדר ראשון, שכן ניתן להשתמש בה (ובשתי אקסיומות נוספות מסדר ראשון) כדי לאפיין את הטבעיים עד כדי איזומורפיזם. אקסיומה זו כן ניתנת לניסוח בלוגיקה מסדר שני, ולכן קיבלנו שמשפט הקומפקטיות כושל בלוגיקה זו (ומכאן גם משפט השלמות לא תקף בה).
ניתן להשתמש במשפטי הקומפקטיות על מנת להוכיח מגרסתו הסופית של משפט ארבעת הצבעים את גרסתו האינסופית, וכנ"ל לגבי משפט החתונה של הול. יישומים טיפוסיים אלו מדגימים את האופן שבו מושג הקומפקטיות מקשר בין הסופי לאינסופי. כך, למשל, ניתן להסיק ממשפט הקומפקטיות שאם לקבוצת נוסחאות יש מודלים סופיים גדולים כרצוננו, יש לה מודל אינסופי.
משפט הקומפקטיות הוא אחד משתי תכונות מפתח המשמשות במשפט לינדסטרום לאפיון הלוגיקה מסדר ראשון. התכונה השנייה היא משפט לוונהיים-סקולם היורד.
קישורים חיצוניים
30142955משפט הקומפקטיות