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