טיפוס (תורת המודלים)

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

הגדרה פורמלית

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

אוסף הטיפוסים השלמים מסדר n כמרחב טופולוגי

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

דוגמה

עבור שפה בת מניה, לכל מבנה M ותת קבוצה בת מניה A, מתקיים . הטיפוסים המבודדים ב- הם צפופים אם ורק אם העוצמה  לא מקבלת את הערך המקסימלי שלה, כלומר ; מתברר שתנאי זה שקול לכך ש- . במקרה זה, אם T היא התורה השלמה של M, יש ל-T מודל ראשוני.

טיפוסים ביחס לתורה T

ניתן לדבר גם על n-טיפוסים ביחס לתורה כלשהי T; אלה קבוצות נוסחאות ב-n משתנים שהן עקביות ביחס ל-T. כמקודם, n-טיפוס שלם ביחס לתורה T הוא n-טיפוס חלקי מקסימלי ביחס להכלה. נשים לב שההגדרה אינה ביחס למודל כלשהו M או לקבוצת פרמטרים כלשהי, אך מלבד זאת היא אנלוגית לחלוטין.  
טופולוגית סטון קיימת גם מעל אוסף כל ה-n טיפוסים השלמים ביחס לתורה T,  - מוגדרת על ידי אותן קבוצות פתוחות בסיסיות . בשונה ממרחבי סטון שהוגדרו מקודם (ביחס למבנה כלשהו M), המרחבים הנוצרים באופן זה לא חייבים להיות קומפקטיים. יחד עם זאת, אם התורה T היא שלמה, לכל מודל M של T מתקיים  - ואז המרחב קומפקטי. טיפוס p הוא מבודד ביחס לתורה T אם הקבוצה {p} היא פתוחה ב-.  
לעיתים מרחבי סטון מעידים על תכונות של התורה T - למשל, אוסף הטיפוסים המבודדים צפוף בכל אחד ממרחבי סטון (מכל מימד n), אם ורק אם ל-T יש מודל ראשוני. דוגמה נוספת לכך היא במשפט Ryll-Nardzewski, בו הוכח כי בקרב תורות שלמות בנות מניה (שיש להן מודל אינסופי), -קטגוריות שקולה לכך שכל מרחבי סטון הם סופיים.

השמטת טיפוסים לא מבודדים

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