חילוץ כמתים

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

רקע

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

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

קיימות מספר דרכים להוכיח שלתורה יש חילוץ כמתים:

• לכל נוסחה, מציאה מפורשת של נוסחה שקולה חסרת כמתים. שיטה זו מאפשרת להוכיח שתורת הסדר הקווי הצפוף ללא נקודות קצה היא בעלת חילוץ כמתים: לכל נוסחה בתורה זו, ניתן להתאים נוסחה המתארת את טיפוסי הסדר האפשריים של המשתנים החופשיים המופיעים בנוסחה המקורית.
• נניח שבשפה קיים סמל קבוע c (המשמש למציאת נוסחה שקולה חסרת כמתים לפסוקים - לפסוק יכיח מותאמת הנוסחה c=c). עבור M ו-N מודלים של התורה, ו-A תת-קבוצה משותפת לשניהם, חילוץ כמתים שקול לתנאי הבא: לכל נוסחה בפרמטרים מ-A ומשתנה יחיד v, אם קיים איבר $m\in M$ כך ש-M מספק את הנוסחה המתקבלת מהצבת m במקום המשתנה v, אז קיים איבר $n\in N$ כך ש-N מספק את הנוסחה המתקבלת מהצבת n במקום המשתנה v. ניתן להרחיב את התנאי הזה הלאה למציאת תנאים מספיקים לחילוץ כמתים:

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

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

שימושים

בדרך כלל יש לתורות בעלות חילוץ כמתים תכונות 'טובות':

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

הפניות

• Marker, David (2002). Model Theory: An Introduction. Graduate Texts in Mathematics 217. Springer. ISBN 0-387-98760-6.