הצגת המקור של הדף "חילוץ כמתים"

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

== רקע ==

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

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

קיימות מספר דרכים להוכיח שלתורה יש חילוץ כמתים:
* לכל נוסחה, '''מציאה מפורשת של נוסחה שקולה חסרת כמתים'''. שיטה זו מאפשרת להוכיח שתורת הסדר הקווי הצפוף ללא נקודות קצה היא בעלת חילוץ כמתים: לכל נוסחה בתורה זו, ניתן להתאים נוסחה המתארת את טיפוסי הסדר האפשריים של המשתנים החופשיים המופיעים בנוסחה המקורית.
* נניח שבשפה קיים סמל קבוע c (המשמש למציאת נוסחה שקולה חסרת כמתים לפסוקים - לפסוק יכיח מותאמת הנוסחה c=c). עבור M ו-N מודלים של התורה, ו-A תת-קבוצה משותפת לשניהם, חילוץ כמתים שקול לתנאי הבא: לכל נוסחה בפרמטרים מ-A ומשתנה יחיד v, אם קיים איבר <math>m  \in M</math> כך ש-M מספק את הנוסחה המתקבלת מהצבת m במקום המשתנה v, אז קיים איבר <math>n  \in N</math> כך ש-N מספק את הנוסחה המתקבלת מהצבת n במקום המשתנה v. ניתן להרחיב את התנאי הזה הלאה למציאת תנאים מספיקים לחילוץ כמתים:
# תת-מבנה '''סגור בפשטות''' בתוך מבנה המכיל אותו אם המבנים מסכימים על פסוקים חסרי כמתים עם פרמטרים מהמבנה הקטן וכימות ישי על משתנה יחיד v. תורה היא בעלת מודלים ראשוניים אלגברית אם לכל תת-מבנה של מודל כלשהו של התורה יש מודל שהוא '''ראשוני אלגברית ביחס אליו''' - המקיים שכל מודל המכיל את תת-המבנה ממנו יצאנו מכיל בתוכו עותק של המודל הראשוני אלגברית מעליו. '''תורות בהן כל תת-מודל הוא סגור בפשטות, שיש להן מודלים ראשוניים אלגברית''', הן בעלות חילוץ כמתים. בשיטה זו ניתן להוכיח שתורות אלגבריות רבות הן בעלות חילוץ כמתים (ובהן תורת השדות הסגורים אלגברית, תורת ה[[חבורה (מבנה אלגברי)|חבורות]] ה[[חבורה חליקה|חליקות]] ה[[חבורה אבלית|אבליות]] [[פיתול (אלגברה)|חסרות הפיתול]] ותורת ה[[שדה סגור ממשית|שדות הסגורים ממשית]]).
# נניח ש-M, N מודלים של תורה T, שעוצמתה קטנה מעוצמת M. עוד נניח ש-N מממש כל טיפוס מעל קבוצת פרמטרים שגודלה לא עולה על גודל M. אז חילוץ כמתים שקול, במצב זה, לתנאי הבא: כל שיכון חלקי מתת קבוצה של M ל-N ניתן להרחבה לשיכון של M ב-N. בשיטה זו, למשל, ניתן להוכיח חילוץ כמתים בתורת השדות הסגורים דיפרנציאלית ממאפיין 0.
* פיתוח '''אלגוריתם לחילוץ כמתים''' - עבור תורה שבה קיים אלגוריתם כזה, שאלת כריעות התורה נעשית פשוטה הרבה יותר, שכן בשיטה זו מנוטרלים שני המכשולים העיקריים בדרך לכריעות - כמתים ומשתנים (כשמשתנים ניתן לנטרל באמצעות ההבחנה שכימות כולל על כל משתנה לא משפיע על סטטוס היכיחות של הנוסחה). אם כן, שאלת כריעות התורה מצטמצמת לבדיקת הכריעות של תורה שקולה המורכבת רק מפסוקים חסרי כמתים (שהם צירופים בוליאניים של פסוקים אטומיים, ושאלת כריעותם פשוטה הרבה יותר).

== שימושים ==
בדרך כלל יש לתורות בעלות חילוץ כמתים תכונות 'טובות':
* כאמור, ניתן לקבוע בקלות רבה יותר לגבי תורות בעלות חילוץ כמתים האם הן [[כריעות]] או לא. בשיטה זו ניתן להוכיח ש[[אריתמטיקת פרסבורגר]] (התורה השלמה של המספרים השלמים בשפה המכילה את השוויון, החיבור ואת הקבועים 0 ו-1) היא כריעה ו[[שלמות|שלמה]]. ניתן להרחיב ולמצוא חסמי יעילות עבור בעיית הכריעות של תורות בעלות חילוץ כמתים.
* תורה היא '''שלמת מודלים''' אם בקרב המודלים שלה, תתי מבנים ותתי מבנים אלמנטריים מתלכדים. חילוץ כמתים גורר שלמות מודלים. אבחנה זו מפשטת הוכחת משפטים רבים באלגברה, כדוגמת [[הבעיה ה-17 של הילברט]] ו[[משפט האפסים של הילברט]].
* חילוץ כמתים בתורה T יכול לסייע במחקר הקבוצות הגדירות במודלים שלה (שכן מספיק לבחון רק את הקבוצות הגדירות על ידי נוסחאות חסרות כמתים). תורות בעלות חילוץ כמתים בשפה מתאימה יכולות להיות מינימליות במובן החזק (כלומר כל קבוצה גדירה היא סופית או קו-סופית, או באופן שקול, כל קבוצה גדירה ניתן להגדיר בשפת השוויון) או o-מינימליות (כלומר כל קבוצה גדירה היא איחוד סופי של אינטרוולים, קבוצות סופיות וקבוצות קו-סופיות, או באופן שקול - כל קבוצה גדירה ניתן להגדיר כבר באמצעות יחס סדר דו מקומי ויחס השוויון). לדוגמה, תורת [[מרחב וקטורי|המרחבים הווקטוריים]] מעל [[מספר רציונלי|הרציונליים]] היא בעלת חילוץ כמתים, ולכן כל תת-קבוצה גדירה מוגדרת באמצעות נוסחה חסרת כמתים, כלומר משוואה או אי שוויון ליניארי. באופן שקול, כל קבוצה גדירה היא צירוף בוליאני של היפר מישורים, שכל אחד מהם הוא סופי - ולכן היא מינימלית במובן החזק.

== הפניות ==
* {{cite book | last=Marker | first=David | title= Model Theory: An Introduction | publisher=Springer | year=2002 | isbn=0-387-98760-6| series=[[Graduate Texts in Mathematics]] 217}}
==קישורים חיצוניים==
* {{MathWorld}}

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