משפט לוונהיים-סקולם

היסטוריה

כמוסבר בהמשך, משפט לוונהיים-סקולם הוא תוצר של שני משפטים, משפט הכיווץ ומשפט הניפוח. ב-1915 הוכיח המתמטיקאי הגרמני לאופולד לוונהיים גרסה מוקדמת של משפט הכיווץ, שלכל תורה עם מודל אינסופי יש מודל בן מנייה. אולם בהוכחה של לוונהיים הייתה טעות. ב-1920 הציג המתמטיקאי הנורווגי תורלף סקולם הוכחה חלופית ונכונה.
המשפט המלא הוכח ב-1936 על ידי המתמטיקאי הרוסי אנטולי מלצב, לאחר שהוכיח את הגרסה המלאה של משפט הקומפקטיות הדרושה בהוכחת משפט הניפוח. במאמרו הוא ציין שלטענת סקולם המשפט המלא הוכח עוד קודם לכן על ידי אלפרד טרסקי במהלך סמינר ב-1928. אולם טרסקי לא זכר את הוכחתו ולא ברור כיצד יכל להוכיח את המשפט ללא משפט הקומפקטיות.

תנאי המשפט

לא ניתן להחליש את תנאי המשפט. אם לתורה יש מודל סופי הדבר אינו גורר קיום מודל אינסופי. זאת משום שבכל שפה מסדר ראשון יש יחס שוויון, ולכן התורה יכולה לכלול פסוק שאומר שבכל קבוצה של n+1 איברים יש שניים שווים (ומכאן שכל מודל יש לכל היותר n איברים). גם קיומו של מודל אינסופי לא גורר קיום מודל סופי. למשל כל קבוצה אינסופית היא מודל לתורה שלכל n כוללת את הפסוק הקובע שיש לפחות n איברים שונים. מצד שני, לתורה זו אין אף מודל סופי.
אם שפת התורה אינה בת-מנייה, אז מתקיימת גרסה מוכללת של משפט לוונהיים-סקולם הקובעת שקיים מודל מכל עוצמה שאינה קטנה מעוצמת השפה. ההוכחה של המשפט המוכלל אנלוגית למקרה הבן מנייה.

הוכחת משפט הניפוח

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

מסקנות

משפט לוונהיים-סקולם מאפשר להסיק מסקנות רבות על כוח הביטוי של שפה מסדר ראשון. מהמשפט נובע למשל שלא ניתן לתאר את קבוצת המספרים הטבעיים בשפה מסדר ראשון, בלי לתאר באותה מידה גרסאות מנופחות הכוללות "יותר מידי" מספרים. מכיוון שמערכת פאנו הכתובה בשפה מסדר שני מתארת את המספרים הטבעיים עד כדי איזומורפיזם, נובע מכך שלא ניתן לצמצם את אקסיומות מערכת פאנו לשפה מסדר ראשון. אריתמטיקת פאנו, שהיא המערכת המתקבלת מהחלפת אקסיומת האינדוקציה (הכתובה בסדר שני), בסכמה של אקסיומות הקובעות אינדוקציה לכל נוסחה מסדר ראשון, היא חלשה באופן מהותי ממערכת פאנו.
ממשפט לוונהיים-סקולם וממשפט הקומפקטיות ניתן להסיק שאם לתורה  יש מודלים סופיים בלתי חסומים (לכל M טבעי יש מודל שעוצמתו M לפחות), אז יש לה מודל מכל עוצמה אינסופית. ממשפט הקומפקטיות נובע שהתורה המתקבלת מ- על ידי הוספת אינסוף פסוקים שקובעים שיש לפחות n איברים שונים לכל n טבעי היא עקבית. לכן יש לה ל- מודל אינסופי, ולכן מודל מכל עוצמה אינסופית.
מסקנה נוספת ממשפט לוונהיים-סקולם היא שאם תורה  תורה -קטגורית (יש לה מודל יחיד עד כדי איזומורפיזם מעוצמה ), ואין לה מודלים סופיים, אז  תורה שלמה. זאת משום שאם  הם מודלים כלשהם של , אז לפי הנתון הם אינם סופיים, ולכן לפי משפט הכיווץ יש להם תת-מבנים אלמנטריים  מעוצמה . מכיוון ש- תורה -קטגורית נובע מכך ש- איזומורפיים. לכן אותם משפטים נכונים הן ב- והן ב-, וכל המשפטים הללו בהכרח נובעים מ-.
בראשית המאה ה-20 ניסתה הקהילה המתמטית למצוא תורה מסדר ראשון שתתאר את המתמטיקה המודרנית כולה (ראו תוכנית הילברט). משפט לוונהיים-סקולם קבע שאף תורה שכזו לא תהיה קטגורית, ויהיו לה מודלים רבים. מאוחר יותר הוכח משפטי האי-שלמות של גדל שאף החריף את הבעיה יותר - לא תיתכן תורה שכזו שתהיה גם עקבית, גם אפקטיבית וגם שלמה (כלומר לא רק שיהיו לה מודלים רבים, אלא שלא בכולם יתקיימו אותם המשפטים).
משפט לינדסטרום קובע ששפה מסדר ראשון היא התחשיב הלוגי החזק ביותר שבמסגרתו מתקיימים הן משפט הקומפקטיות והן משפט הכיווץ של לוונהיים-סקולם.

פרדוקס סקולם

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