הצגת המקור של הדף "טיפוס (תורת המודלים)"

ב[[תורת המודלים]], '''טיפוס''' הוא אוסף נוסחאות המתארות "התנהגות" של איברים ב[[מבנה (לוגיקה מתמטית)|מבנה]] מתמטי. בהינתן מבנה מסוים, טיפוס לא רק מאפשר לתאר התנהגות של איברים מתוכו, אלא גם של "איברים פוטנציאליים", המגולמים ב[[משתנה|משתנים]] <math>x_1,\ldots,x_n</math>. "התנהגות" המשתנים מנוסחת בפועל באמצעות קבוצת [[נוסחה (לוגיקה)|נוסחאות מסדר ראשון]] בשפת המבנה. 

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

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

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

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

== הגדרה פורמלית ==
נניח <math>M</math> מבנה. נתבונן ב[[שפה מסדר ראשון|שפה]] <math>L</math> המכילה, נוסף על שפת [[מודל (לוגיקה מתמטית)|המודל]] <math>M</math>, [[שפה מסדר ראשון|סמל קבוע]] חדש עבור כל אחד מאיברי [[תת-קבוצה|תת קבוצה]] כלשהי <math>A</math> של <math>M</math> (ייתכן ש-<math>A</math> [[הקבוצה הריקה|ריקה]]). 

'''n-טיפוס חלקי '''הוא קבוצה <math>p</math> של [[נוסחה (לוגיקה)|נוסחאות]] בשפה <math>L</math>, במשתנים <math>x_1,\ldots,x_n</math>, שהיא [[עקביות (לוגיקה)|עקבית]] עם [[תורה (לוגיקה מתמטית)|התורה השלמה]] של <math>M</math> (ביחס לשפה <math>L</math>).

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

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

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

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

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

[[משפט הקומפקטיות]] מאפשר להוכיח שהתופעה המתוארת בדוגמה מתרחשת תמיד - כל טיפוס מעל מבנה <math>M</math> ניתן למימוש ב[[תת מבנה אלמנטרי|הרחבה אלמנטרית]] כלשהי של <math>M</math>. 

'''טיפוס שלם''' הממומש על ידי איבר <math>\vec{a}\in M^n</math> במבנה <math>M</math> מסומן גם <math>tp^M(\vec{a})</math> (ובאופן [[טריוויאלי (מתמטיקה)|טריוויאלי]], קיים טיפוס יחיד כזה).

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

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

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

טיפוס מסעיף 2, המתאר [[חתך דדקינד]], מגלם במשתנה <math>v</math> את ה[[מספרים ממשיים|מספר הממשי]] המתאים לחתך. מבנה המספרים הממשיים הוא הרחבה אלמנטרית של הרציונליים בה הטיפוס ממומש. 

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

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

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

אם נתבונן ב[[:en:Stone_space|מרחב סטון]] של ה[[אלגברה הבוליאנית]] הנוצרת מהקבוצות הגדירות ב-<math>M^n</math>, ניתן לזהות את איברי המרחב הזה עם קבוצות עקביות מקסימליות של נוסחאות מעל n משתנים כלשהם; כאמור, כל קבוצה כזו היא בדיוק טיפוס שלם מסדר n. 
כך, אנו מקבלים באופן טבעי טופולוגיה על <math>S_n^A(M)</math>. 

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

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

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

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

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

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

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

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

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

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

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

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