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

בתורת המודלים, **טיפוס** הוא אוסף נוסחאות המתארות "התנהגות" של איברים במבנה מתמטי. בהינתן מבנה מסוים, טיפוס לא רק מאפשר לתאר התנהגות של איברים מתוכו, אלא גם של "איברים פוטנציאליים", המגולמים במשתנים x_1,\ldots,x_n. "התנהגות" המשתנים מנוסחת בפועל באמצעות קבוצת נוסחאות מסדר ראשון בשפת המבנה. 

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

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

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

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

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

**n-טיפוס חלקי **הוא קבוצה p של נוסחאות בשפה L, במשתנים x_1,\ldots,x_n, שהיא עקבית עם התורה השלמה של M (ביחס לשפה L).

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

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

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

טיפוס מסדר n הוא **ממומש ב-<math>M</math> **אם יש איבר ב-M^n המספק את כל הנוסחאות בו; אחרת, הטיפוס **מושמט ב-<math>M</math>**. 

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

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

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

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

### דוגמה
נתבונן במספרים הרציונליים בשפת הקבוצות הסדורות. נמצא את כל הטיפוסים מסדר 1 במשתנה v, כאשר מאפשרים שימוש בכל מספר רציונלי כפרמטר. ניתן להצטמצם לקבוצות נוסחאות מהצורה v>q ו-v=q (מאחר שתורת הסדר הקווי הצפוף ללא איבר ראשון ואחרון היא בעלת חילוץ כמתים). נקבל שכל 1-טיפוס p במשתנה v מקיים אחד משלושה:
#p ממומש על ידי איבר רציונלי q (כלומר הטיפוס הוא אוסף הנוסחאות שנובעות מהנוסחה v=q - במקרה זה הנוסחה v=q **מבודדת את הטיפוס**).
# p מתאר איבר שמהווה חתך דדקינד מוכלל של המספרים הרציונליים (כלומר המשתנה v גדול מכל אברי קבוצה כלשהי של מספרים רציונליים, וקטן מכל איברי משלימתה - פורמלית, קיים שוני מחתכי דדקינד המתבטא בכך שלקבוצה ה"תחתונה יותר" יכול להיות מקסימום).
#p מתאר איבר הגדול מכל המספרים הרציונליים, או קטן מכולם.

מכאן, |S_1^Q(Q)| = 2^{\aleph_0}.

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

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

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

## אוסף הטיפוסים השלמים מסדר n כ[[מרחב טופולוגי]]
קיימת טופולוגיה טבעית מעל S_n^A(M). 

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

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

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

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

### דוגמה
עבור שפה בת מניה, לכל מבנה M ותת קבוצה בת מניה A, מתקיים |S_n^A(M)| \le 2^{\aleph_0}. הטיפוסים המבודדים ב-S_n^A(M) הם צפופים אם ורק אם העוצמה |S_n^A(M)| לא מקבלת את הערך המקסימלי שלה, כלומר |S_n^A(M)| ; מתברר שתנאי זה שקול לכך ש-|S_n^A(M)|\le\aleph_0 . במקרה זה, אם T היא התורה השלמה של M, יש ל-T מודל ראשוני.

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

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

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

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

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

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

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

קטגוריה:לוגיקה מתמטית