בתורת המודלים, טיפוס הוא אוסף נוסחאות המתארות "התנהגות" של איברים במבנה מתמטי. בהינתן מבנה מסוים, טיפוס לא רק מאפשר לתאר התנהגות של איברים מתוכו, אלא גם של "איברים פוטנציאליים", המגולמים במשתנים ${\displaystyle x_{1},\ldots ,x_{n}}$. "התנהגות" המשתנים מנוסחת בפועל באמצעות קבוצת נוסחאות מסדר ראשון בשפת המבנה.

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

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

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

קיימים שני דגשים מרכזיים:

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

קבוצת נוסחאות p המקיימת את שתי התכונות האלה נקראת טיפוס. הטיפוס p שמכיל את כל הנוסחאות v>n מעיד על תכונה של משתנה אחד, v; טיפוס כזה נקרא 1-טיפוס. באופן דומה, טיפוס המעיד על תכונה של n משתנים נקרא n-טיפוס.

נניח ${\displaystyle M}$ מבנה. נתבונן בשפה ${\displaystyle L}$ המכילה, נוסף על שפת המודל ${\displaystyle M}$, סמל קבוע חדש עבור כל אחד מאיברי תת קבוצה כלשהי ${\displaystyle A}$ של ${\displaystyle M}$ (ייתכן ש-${\displaystyle A}$ ריקה).

n-טיפוס חלקי הוא קבוצה ${\displaystyle p}$ של נוסחאות בשפה ${\displaystyle L}$, במשתנים ${\displaystyle x_{1},\ldots ,x_{n}}$, שהיא עקבית עם התורה השלמה של ${\displaystyle M}$ (ביחס לשפה ${\displaystyle L}$).

n-טיפוס שלם הוא n-טיפוס חלקי שהוא מקסימלי ביחס להכלה (ובאופן שקול, מכיל לכל נוסחה ב-n המשתנים אותה או את שלילתה).

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

את אוסף כל ה-n טיפוסים (השלמים) מעל קבוצת פרמטרים ${\displaystyle A}$ במבנה ${\displaystyle M}$ נהוג לסמן ${\displaystyle S_{n}^{A}(M)}$.

טיפוס מסדר n הוא ממומש ב-${\displaystyle M}$ אם יש איבר ב-${\displaystyle M^{n}}$ המספק את כל הנוסחאות בו; אחרת, הטיפוס מושמט ב-${\displaystyle M}$.

למשל, הטיפוס ${\displaystyle p=\left\{v>1,v>2,v>3,...,v>n,...\right\}}$ בשפת המספרים הטבעיים מתאר משתנה ${\displaystyle v}$ שגדול מכל המספרים הטבעיים. הטיפוס מושמט במודל הסטנדרטי של הטבעיים, ${\displaystyle \mathbb {N} }$. יחד עם זאת, ${\displaystyle p}$ ממומש בכל מודל לא סטנדרטי של האריתמטיקה.

משפט הקומפקטיות מאפשר להוכיח שהתופעה המתוארת בדוגמה מתרחשת תמיד - כל טיפוס מעל מבנה ${\displaystyle M}$ ניתן למימוש בהרחבה אלמנטרית כלשהי של ${\displaystyle M}$.

טיפוס שלם הממומש על ידי איבר ${\displaystyle {\vec {a}}\in M^{n}}$ במבנה ${\displaystyle M}$ מסומן גם ${\displaystyle tp^{M}({\vec {a}})}$ (ובאופן טריוויאלי, קיים טיפוס יחיד כזה).

טיפוס p ביחס למבנה ${\displaystyle M}$ לא חייב להיות ממומש בו, אך תמיד קיימת הרחבה אלמנטרית ${\displaystyle M\prec N}$ בה ${\displaystyle p}$ ממומש על ידי איבר ${\displaystyle {\vec {a}}\in N^{n}}$, ואז ${\displaystyle p=tp^{N}({\vec {a}})}$.

נתבונן במספרים הרציונליים בשפת הקבוצות הסדורות. נמצא את כל הטיפוסים מסדר 1 במשתנה v, כאשר מאפשרים שימוש בכל מספר רציונלי כפרמטר. ניתן להצטמצם לקבוצות נוסחאות מהצורה ${\displaystyle v>q}$ ו-${\displaystyle v=q}$ (מאחר שתורת הסדר הקווי הצפוף ללא איבר ראשון ואחרון היא בעלת חילוץ כמתים). נקבל שכל 1-טיפוס p במשתנה ${\displaystyle v}$ מקיים אחד משלושה:

1. p ממומש על ידי איבר רציונלי q (כלומר הטיפוס הוא אוסף הנוסחאות שנובעות מהנוסחה ${\displaystyle v=q}$ - במקרה זה הנוסחה ${\displaystyle v=q}$ מבודדת את הטיפוס).
2. p מתאר איבר שמהווה חתך דדקינד מוכלל של המספרים הרציונליים (כלומר המשתנה v גדול מכל אברי קבוצה כלשהי של מספרים רציונליים, וקטן מכל איברי משלימתה - פורמלית, קיים שוני מחתכי דדקינד המתבטא בכך שלקבוצה ה"תחתונה יותר" יכול להיות מקסימום).
3. p מתאר איבר הגדול מכל המספרים הרציונליים, או קטן מכולם.

מכאן, ${\displaystyle |S_{1}^{Q}(Q)|=2^{\aleph _{0}}}$.

טיפוס מסעיף 2, המתאר חתך דדקינד, מגלם במשתנה ${\displaystyle v}$ את המספר הממשי המתאים לחתך. מבנה המספרים הממשיים הוא הרחבה אלמנטרית של הרציונליים בה הטיפוס ממומש.

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

טיפוסים ששייכים למחלקת הטיפוסים שבסעיף 1 ממומשים כבר במבנה ממנו יצאנו - המספרים הרציונליים. אלה טיפוסים שניתן לתאר באמצעות נוסחה אחת מסדר ראשון - ${\displaystyle v=q}$. טיפוסים כאלה נקראים טיפוסים מבודדים. אכן, כל טיפוס מבודד ממומש במבנה ביחס אליו הוא הוגדר. לפיכך, אם ברצוננו להשמיט טיפוס, נרצה שהטיפוס לא יהיה מבודד.

קיימת טופולוגיה טבעית מעל ${\displaystyle S_{n}^{A}(M)}$.

אם נתבונן במרחב סטון של האלגברה הבוליאנית הנוצרת מהקבוצות הגדירות ב-${\displaystyle M^{n}}$, ניתן לזהות את איברי המרחב הזה עם קבוצות עקביות מקסימליות של נוסחאות מעל n משתנים כלשהם; כאמור, כל קבוצה כזו היא בדיוק טיפוס שלם מסדר n. כך, אנו מקבלים באופן טבעי טופולוגיה על ${\displaystyle S_{n}^{A}(M)}$.

עבור נוסחה מסדר ראשון ${\displaystyle \phi }$, נגדיר את הקבוצה ${\displaystyle [\phi ]=\left\{p\in S_{n}^{A}(M):\phi \in p\right\}}$. אז האוסף ${\displaystyle \left\{[\phi (v_{1},...,v_{n})]:\phi (v_{1},...,v_{n})\in form(L)\right\}}$ הוא בסיס של קבוצות פתוחות לטופולוגיה זו (ולמעשה, כל קבוצה כזו היא גם סגורה).

טיפוס p ייקרא מבודד אם הקבוצה {p} במרחב סטון היא פתוחה. באופן שקול, אלה טיפוסים הנוצרים על ידי אוסף כל הנוסחאות שנובעות לוגית מנוסחה כלשהי ${\displaystyle \phi }$, הנקראת הנוסחה המבודדת את הטיפוס.

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

עבור שפה בת מניה, לכל מבנה M ותת קבוצה בת מניה A, מתקיים ${\displaystyle |S_{n}^{A}(M)|\leq 2^{\aleph _{0}}}$. הטיפוסים המבודדים ב-${\displaystyle S_{n}^{A}(M)}$ הם צפופים אם ורק אם העוצמה ${\displaystyle |S_{n}^{A}(M)|}$ לא מקבלת את הערך המקסימלי שלה, כלומר ${\displaystyle |S_{n}^{A}(M)|<2^{\aleph _{0}}}$; מתברר שתנאי זה שקול לכך ש-${\displaystyle |S_{n}^{A}(M)|\leq \aleph _{0}}$ . במקרה זה, אם T היא התורה השלמה של M, יש ל-T מודל ראשוני.

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

טופולוגית סטון קיימת גם מעל אוסף כל ה-n טיפוסים השלמים ביחס לתורה T, ${\displaystyle S_{n}(T)}$ - מוגדרת על ידי אותן קבוצות פתוחות בסיסיות ${\displaystyle \left\{[\phi (v_{1},...,v_{n})]:\phi (v_{1},...,v_{n})\in form(L)\right\}}$. בשונה ממרחבי סטון שהוגדרו מקודם (ביחס למבנה כלשהו M), המרחבים הנוצרים באופן זה לא חייבים להיות קומפקטיים. יחד עם זאת, אם התורה T היא שלמה, לכל מודל M של T מתקיים ${\displaystyle S_{n}(T)=S_{n}^{M}(\emptyset )}$ - ואז המרחב קומפקטי. טיפוס p הוא מבודד ביחס לתורה T אם הקבוצה {p} היא פתוחה ב-${\displaystyle S_{n}(T)}$.

לעיתים מרחבי סטון מעידים על תכונות של התורה T - למשל, אוסף הטיפוסים המבודדים צפוף בכל אחד ממרחבי סטון (מכל מימד n), אם ורק אם ל-T יש מודל ראשוני. דוגמה נוספת לכך היא במשפט Ryll-Nardzewski, בו הוכח כי בקרב תורות שלמות בנות מניה (שיש להן מודל אינסופי), ${\displaystyle \!\,\aleph _{0}}$-קטגוריות שקולה לכך שכל מרחבי סטון הם סופיים.

כל טיפוס מבודד ביחס למבנה M ממומש בו; לגבי טיפוסים שמוגדרים ביחס לתורה T - השמטה או מימוש של טיפוסים כאלה היא ביחס למודל ספציפי של T. טיפוסים מבודדים ביחס לתורה T מושמטים במודל M שלה אם ורק אם אין במודל עדים לנוסחה המבודדת אותם (כלומר M לא מספק את הנוסחה ${\displaystyle \exists x\phi (x)}$ ); כפועל יוצא מכך, אם התורה T היא שלמה, כל טיפוס מבודד ממומש בכל אחד מהמודלים שלה.

מכאן, על מנת שטיפוס כלשהו יושמט, מסתמן שמספיק שלא יהיה מבודד. משפט השמטת הטיפוס מבטא את התפיסה הזו:

משפט השמטת הטיפוס: עבור תורה בת מניה T, כל טיפוס לא מבודד מושמט באיזשהו מודל בן מניה M של T.

לכאורה, ובעיקר מסיבות הקשורות לטרמינולוגיה, השמטת טיפוס נראית כדבר שלילי. בפועל, יש לכך תועלות רבות. למשל, ניתן להיעזר בהשמטת הטיפוס ${\displaystyle p(v)=\{v\neq 0,v\neq S(0),v\neq S(S(0)),...\}}$ במודל כלשהו של תורה T (בשפה המכילה את ${\displaystyle \{0,S\}}$), על מנת להוכיח שמערכת ההיסק הסטנדרטית עבור ה-w-לוגיקה היא שלמה (באנלוגיה למשפט השלמות של גדל).