משפט לוונהיים-סקולם
בערך זה |
בלוגיקה מתמטית, משפט לוונהיים-סקולם הוא משפט יסודי בתורת המודלים שקובע שאם לתורה בשפה בת מנייה מסדר ראשון יש מודל אינסופי, אז יש לה מודל מכל עוצמה אינסופית. המשפט מראה שלתורה בת מנייה מסדר ראשון אין שליטה על העוצמה של המודלים האינסופיים שלה (בניגוד ללוגיקה מסדר שני), ושכל תורה שכזו שיש לה מודל אינסופי אינה קטגורית (משמע יש לה יותר ממודל אחד עד כדי איזומורפיזם).
גרסה חזקה יותר של המשפט קובעת שלכל תורה בשפה מסדר ראשון (שאינה בת מנייה בהכרח) שיש לה מודל אינסופי, יש לה מודל מכל עוצמה אינסופית הגדולה מעוצמת קבוצת הקבועים שלה.
היסטוריה
[עריכת קוד מקור | עריכה]כמוסבר בהמשך, משפט לוונהיים-סקולם הוא תוצר של שני משפטים, משפט הכיווץ ומשפט הניפוח. ב-1915 הוכיח המתמטיקאי הגרמני לאופולד לוונהיים גרסה מוקדמת של משפט הכיווץ, שלכל תורה עם מודל אינסופי יש מודל בן מנייה. אולם בהוכחה של לוונהיים הייתה טעות. ב-1920 הציג המתמטיקאי הנורווגי תורלף סקולם הוכחה חלופית ונכונה.
המשפט המלא הוכח ב-1936 על ידי המתמטיקאי הרוסי אנטולי מלצב, לאחר שהוכיח את הגרסה המלאה של משפט הקומפקטיות הדרושה בהוכחת משפט הניפוח. במאמרו הוא ציין שלטענת סקולם המשפט המלא הוכח עוד קודם לכן על ידי אלפרד טרסקי במהלך סמינר ב-1928. אולם טרסקי לא זכר את הוכחתו ולא ברור כיצד יכול היה להוכיח את המשפט ללא משפט הקומפקטיות.
רקע
[עריכת קוד מקור | עריכה]מודל של תורה בשפה מסדר ראשון הוא מבנה (המורכב מקבוצה ומפונקציה המפרשת את קבועי השפה כקבועים ויחסים בקבוצה) שמקיים את כל הפסוקים בשפה. הקבוצה שעומדת בבסיס מבנה נקראת העולם של , ונסמנו . העוצמה של היא העוצמה של .
מבנה הוא תת-מבנה של אם , ופונקציית המבנה של היא צמצום של פונקציית המבנה של ל-. קבוצה נקראת קבוצה סגורה ב- אם סגורה תחת כל הפעולות (פונקציות) בשפה (ובפרט מכילה את כל האיברים ב- המתפרשים כקבועים של , שהם הפעולות ה-0 מקומיות). אם הוא תת-קבוצה סגורה של , אז התת-מבנה שנקבע על ידי הוא התת-מבנה היחיד שעולמו הוא ושפונקציית המבנה שלו היא צמצום פונקציית המבנה של ל-.
תת-מבנה של מבנה נקרא תת-מבנה אלמנטרי אם לכל השמה אפשרית כל הנוסחאות בשפה שנכונות ב-, נכונות גם ב- (אינטואיטיבית, כל טענה שנכונה במבנה נכונה גם בכל תת-מבנה אלמנטרי שלו, ולהפך). מן ההגדרה נובע שאם מודל של , גם התת-מבנה האלמנטרי הוא מודל של .
מבחן טרסקי-ווט קובע שתנאי הכרחי ומספיק לכך שתת-מבנה של הוא תת-מבנה אלמנטרי, הוא:
- לכל נוסחה בשפה , אשר הם המשתנים החופשיים בה, ולכל , אם קיים כך ש- נכון ב-, אז קיים כך ש- נכון ב-.
קבוצת פסוקים היא עקבית אם קיים לה מודל (ראו משפט השלמות של גדל). משפט הקומפקטיות קובע ש- עקבית אם ורק אם כל תת-קבוצה סופית שלה עקבית.
תנאי המשפט
[עריכת קוד מקור | עריכה]לא ניתן להחליש את תנאי המשפט. אם לתורה יש מודל סופי הדבר אינו גורר קיום מודל אינסופי. זאת משום שבכל שפה מסדר ראשון יש יחס שוויון, ולכן התורה יכולה לכלול פסוק שאומר שבכל קבוצה של n+1 איברים יש שניים שווים (ומכאן שכל מודל יש לכל היותר n איברים). גם קיומו של מודל אינסופי לא גורר קיום מודל סופי. למשל כל קבוצה אינסופית היא מודל לתורה שלכל n כוללת את הפסוק הקובע שיש לפחות n איברים שונים. מצד שני, לתורה זו אין אף מודל סופי.
אם שפת התורה אינה בת-מנייה, אז מתקיימת גרסה מוכללת של משפט לוונהיים-סקולם הקובעת שקיים מודל מכל עוצמה שאינה קטנה מעוצמת השפה. ההוכחה של המשפט המוכלל אנלוגית למקרה הבן מנייה.
הוכחה
[עריכת קוד מקור | עריכה]הוכחת המשפט נחלקת למעשה לשניים:
- משפט הכיווץ - לכל תורה בת-מנייה מסדר ראשון עם מודל אינסופי מעוצמה , ולכל עוצמה אינסופית , קיים לתורה זו מודל מעוצמה .
- משפט הניפוח - לכל תורה בת-מנייה מסדר ראשון עם מודל אינסופי מעוצמה , ולכל עוצמה , קיים לתורה זו מודל מעוצמה לפחות.
כמסקנה משני החלקים נובע משפט לוונהיים-סקולם במלואו:
- אם לתורה בת-מנייה מסדר ראשון יש מודל אינסופי מעוצמה , אז לכל עוצמה אינסופית נבחר עוצמה . לפי משפט הניפוח קיים מודל מעוצמה לפחות, ולכן לפי משפט הכיווץ קיים מודל מעוצמה .
הוכחת משפט הכיווץ
[עריכת קוד מקור | עריכה]יהי מבנה בשפה (המקיימת את תנאי המשפט) מעוצמה אינסופית . תהי עוצמה אינסופית. נראה שיש ל- תת-מבנה אלמנטרי מעוצמה .
לכל נוסחה נתאים פונקציה הנקראת פונקציית סקולם. פונקציית סקולם מוגדרת כך: לכל מגדירים , כאשר הוא איבר כך שמתקיים , אם ישנו איבר כזה, או סתם איבר שרירותי אם אין איבר כזה (בחירת האיברים מצריכה את אקסיומת הבחירה). נסמן ב- את קבוצת פונקציות סקולם של כל הנוסחאות בשפה . יש נוסחאות בשפה (כי קבוצת המילים מעל שפה בת מנייה היא בת מנייה) ולכן .
נגדיר כעת ברקורסיה סדרת קבוצות. תהיה תת-קבוצה כלשהי של שעוצמתה . נגדיר:
כלומר היא הקבוצה המתקבלת מ- על ידי הוספת כל התמונות של איברי תחת כל פונקציות סקולם.
נוכיח באינדוקציה כי לכל טבעי, .
- על פי הגדרתו, מקיים .
- נניח שמתקיים . אז יש k-יות סדורות של איברי (משפט טרסקי), ויש פונקציות סקולם, ולכן יש תמונות של איברי תחת פונקציות סקולם. מכאן ש-.
נגדיר . מהגדרת מתקיים וכן .
נבחין כי סגורה תחת פונקציות סקולם. לכל ולכל קיים כך ש-, ולכן .
נראה כי קבוצה סגורה ב-. לכל פעולה n-מקומית בשפה נגדיר נוסחה שהיא הנוסחה . מהסגירות של ביחס לפונקציות סקולם נקבל ש- סגורה ביחס ל- - לכל מתקיים: .
קבוצה סגורה ולכן קיים תת-מבנה של שנקבע על ידה. נוכיח כי זהו תת-מבנה אלמנטרי.
לכל נוסחה ולכל , אם קיים כך שמתקיים , אז לפי הגדרת פונקציית סקולם קיים כך שמתקיים . לכן לפי מבחן טרסקי-ווט תת-מבנה אלמנטרי של .
מכאן שאם מודל של תורה המקיימת את תנאי המשפט, אז היא מודל מעוצמה של .
הוכחת משפט הניפוח
[עריכת קוד מקור | עריכה]תהי תורה בשפה המקיימת את תנאי המשפט, ויהי מודל שלה מעוצמה אינסופית . תהי עוצמה כלשהי. נבנה מודל של שעוצמתו לפחות.
תהי קבוצה שעוצמתה . נגדיר שפה המתקבלת מ- על ידי הוספה של קבוע כנגד כל . נגדיר קבוצת פסוקים בשפה כך: . נגדיר את כקבוצה המתקבלת מהאיחוד .
נשתמש במשפט הקומפקטיות כדי להראות ש- עקבית בשפה . תהי תת-קבוצה סופית של . קיימת קבוצה מהצורה , כך ש- היא תת-קבוצה סופית של , ומתקיים . ב- יש רק מספר סופי של פסוקים מהצורה . נסמן את קבוצת כל ה- שמופיעים בפסוק שכזה ב-.
נגדיר מבנה בשפה שפונקציית המבנה שלו מתלכדת עם זו של לכל הקובעים ב-, ובנוסף מוגדרת באופן שרירותי לכל קבוע ב-, מלבד לקבועים שב-, שאותם היא מפרשת כאיברים שונים זה מזה ב- (ייתכן משום ש- סופית, ואילו אינסופית).
מודל של (כי הוא מודל של , וכל הפסוקים ב- שקובעים שאיברי שונים זה מזה, אכן מתקיימים), לכן היא גם מודל של , ועל כן עקבית. נקבל ממשפט הקומפקטיות ש- עקבית בשפה . נסמן ב- מודל של בשפה . כל הפסוקים ב- נכונים ב-, ובפרט כל פסוקי שקובעים שיש איברים השונים זה מזה נכונים. לכן .
מודל של בשפה (כתת קבוצה של ), ולכן הוא גם מודל של בשפה (תוך צמצום פונקציית המבנה שלו ל-). קיבלנו של- יש מודל מעוצמה לפחות.
מסקנות
[עריכת קוד מקור | עריכה]משפט לוונהיים-סקולם מאפשר להסיק מסקנות רבות על כוח הביטוי של שפה מסדר ראשון. מהמשפט נובע למשל שלא ניתן לתאר את קבוצת המספרים הטבעיים בשפה מסדר ראשון, בלי לתאר באותה מידה גרסאות מנופחות הכוללות "יותר מידי" מספרים. מכיוון שמערכת פאנו הכתובה בלוגיקה מסדר שני מתארת את המספרים הטבעיים עד כדי איזומורפיזם, נובע מכך שלא ניתן לצמצם את אקסיומות מערכת פאנו לשפה מסדר ראשון. אריתמטיקת פאנו, שהיא המערכת המתקבלת מהחלפת אקסיומת האינדוקציה (הכתובה בסדר שני), בסכמה של אקסיומות הקובעות אינדוקציה לכל נוסחה מסדר ראשון, היא חלשה באופן מהותי ממערכת פאנו.
ממשפט לוונהיים-סקולם וממשפט הקומפקטיות ניתן להסיק שאם לתורה יש מודלים סופיים בלתי חסומים (לכל M טבעי יש מודל שעוצמתו M לפחות), אז יש לה מודל מכל עוצמה אינסופית. ממשפט הקומפקטיות נובע שהתורה המתקבלת מ- על ידי הוספת אינסוף פסוקים שקובעים שיש לפחות n איברים שונים לכל n טבעי היא עקבית. לכן יש לה ל- מודל אינסופי, ולכן מודל מכל עוצמה אינסופית.
מסקנה נוספת ממשפט לוונהיים-סקולם היא שאם תורה -קטגורית (יש לה מודל יחיד עד כדי איזומורפיזם מעוצמה ), ואין לה מודלים סופיים, אז תורה שלמה. זאת משום שאם הם מודלים כלשהם של , אז לפי הנתון הם אינם סופיים, ולכן לפי משפט הכיווץ יש להם תת-מבנים אלמנטריים מעוצמה . מכיוון ש- תורה -קטגורית נובע מכך ש- איזומורפיים. לכן אותם משפטים נכונים הן ב- והן ב-, וכל המשפטים הללו בהכרח נובעים מ-.
בראשית המאה ה-20 ניסתה הקהילה המתמטית למצוא תורה מסדר ראשון שתתאר את המתמטיקה המודרנית כולה (ראו תוכנית הילברט). משפט לוונהיים-סקולם קבע שאף תורה שכזו לא תהיה קטגורית, ויהיו לה מודלים רבים. מאוחר יותר הוכח משפטי האי-שלמות של גדל שאף החריף את הבעיה יותר - לא תיתכן תורה שכזו שתהיה גם עקבית, גם אפקטיבית וגם שלמה (כלומר לא רק שיהיו לה מודלים רבים, אלא שלא בכולם יתקיימו אותם המשפטים).
משפט לינדסטרום קובע ששפה מסדר ראשון היא התחשיב הלוגי החזק ביותר שבמסגרתו מתקיימים הן משפט הקומפקטיות והן משפט הכיווץ של לוונהיים-סקולם.
פרדוקס סקולם
[עריכת קוד מקור | עריכה]החלת משפט לוונהיים-סקולם על תורת הקבוצות האקסיומטית גוררת מסקנה הנדמית סתירתית. לפי המשפט קיים מודל בן מנייה של תורת הקבוצות. לכן כל הקבוצות במודל הן בנות מנייה (שכן כל איבר של קבוצה הוא בעצמו קבוצה במסגרת אקסיומות צרמלו-פרנקל). זאת בסתירה לכאורה למשפט קנטור שממנו עולה שקיימות קבוצות שאינן בנות מנייה.
תוצאה זו התגלתה על ידי סקולם ב-1922 ונקראת על שמו "פרדוקס סקולם". סקולם גם הסביר מדוע הפרדוקס אינו סתירה באמת. הפתרון נעוץ בכך שהמונח "קבוצה" במודל של סקולם נבדל מהמשמעות החיצונית שלו. השוואת עוצמות של קבוצות מסתמכת על קיומן של פונקציות חד-חד-ערכיות ועל ביניהן. אולם פונקציות שכאלה הן בעצמן קבוצות, שאינן בהכרח כלולות כקבוצות במסגרת המודל הקטן ובן המנייה של סקולם לתורת הקבוצות. נכון שקיימת פונקציה חיצונית למודל שמתאימה בין קבוצת המספרים הטבעיים לקבוצת המספרים הממשיים במודל של סקולם, אבל הפונקציה הזו אינה קיימת בתוך המודל של סקולם, ולכן הוכחת האלכסון של קנטור עדין עובדת במודל זה.
קישורים חיצוניים
[עריכת קוד מקור | עריכה]- משפט לוונהיים-סקולם, באתר MathWorld (באנגלית)