שלמות (לוגיקה מתמטית)

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

בשפה פורמלית T נקראת שלמה ביחס לתכונה α אם כל נוסחה ${\textstyle \beta \in T}$ בעלת α התכונה יכולה להיגזר באמצעות אותה מערכת, כלומר היא אחד ממשפטיה - אחרת המערכת נחשבת לא שלמה. באופן אינטואיטיבי, מערכת נקראת שלמה במובן המסוים הזה, אם היא יכולה לגזור כל נוסחה שהיא נכונה.

שלמות ונאותות

התכונה ההפוכה (והמשלימה) לשלמות נקראת נאותות (Soundness): מערכת היא נאותה ביחס לתכונה (לרוב תוקף סמנטי) אם לכל משפט שניתן להוכיח בה יש את התכונה הזו.

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

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

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

אי-שלמות

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

צורות של שלמות

שלמות אקספרסיבית

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

שלמות פונקציונלית

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

שלמות סמנטית

שלמות סמנטית היא ההפך (משלים) לנאותות (soundness) עבור מערכות פורמליות. מערכת פורמלית היא שלמה ביחס לטאוטולוגיות או "שלמה מבחינה סמנטית" כאשר כל הטאוטולוגיות שלה הן משפטים, ואילו מערכת פורמלית היא נאותה כאשר כל המשפטים הם טאוטולוגיות (כלומר, הם נוסחאות תקפות מבחינה סמנטית: נוסחאות שנכונות תחת כל פרשנות שפת המערכת התואמת את כללי המערכת). כלומר, מערכת פורמלית שלמה מבחינה סמנטית אם

$\models _{\mathcal {S}}\varphi \ \to \ \vdash _{\mathcal {S}}\varphi .$

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

שלמות חזקה

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

$\Gamma \models _{\mathcal {S}}\varphi \ \to \ \Gamma \vdash _{\mathcal {S}}\varphi .$

השלמות-הפרכה - Refutation-completeness

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

$\Gamma \models _{\mathcal {S}}\bot \to \ \Gamma \vdash _{\mathcal {S}}\bot .$

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

דוגמאות למערכות השלמות להפרכה כוללות: רזולוציית SLD על סעיפי הורן - Horn clauses, סופרפוזיציה - Superposition calculus על לוגיקה סתמית משוואה - Clause מסדר ראשון, רזולוציית רובינסון על קבוצות סעיפים. האחרון אינו שלם מאוד: למשל $\{a\}\models a\lor b$ מתקיים אפילו בתת-קבוצה של לוגיקה מסדר ראשון, אבל $a\lor b$ לא ניתן לגזור ממנו $\{a\}$ לפי החלטה (כלל הרזולוציה). למרות זאת, $\{a,\lnot (a\lor b)\}\vdash \bot$ ניתן לגזור.

שלמות תחבירית - Syntactical completeness

מערכת פורמלית S היא שלמה תחבירית או שלמה באופן דדוקטיבי או שלמה מקסימלית אם עבור כל משפט (נוסחה סגורה) φ של שפת המערכת או φ או ¬φ הוא משפט של S. זה נקרא גם השלמות שלילה, והוא חזק יותר משלימות סמנטית. במובן אחר, מערכת פורמלית שלמה מבחינה תחבירית אם ורק אם לא ניתן להוסיף לה משפט בלתי ניתן להוכחה מבלי להכניס חוסר עקביות. לוגיקה פרופוזיציונית פונקציונלית של אמת ולוגיקת פרדיקט מסדר ראשון הן שלמות מבחינה סמנטית, אך אינן שלמות מבחינה תחבירית (לדוגמה, ההצהרה הלוגית הטענתית המורכבת ממשתנה טענה יחיד A אינה משפט, וגם שלילתו). משפט חוסר השלמות של גדל מראה שכל מערכת ניתנת לחישוב בעלת עוצמה מספקת, כגון אריתמטיקה של פאנו, אינה יכולה להיות עקבית וגם שלמה מבחינה תחבירית.

שלמות מבנית-Structural completeness

בלוגיקה על-אינטואיציונית-Superintuitionistic logic ומודאלית-modal logics , היגיון מושלם מבחינה מבנית אם כל כלל קביל ניתן לגזירה.

קישורים חיצוניים

• שלמות, באתר אנציקלופדיה בריטניקה (באנגלית)