משפט השלמות של גדל, ההוכחה (חלק ב')

אנו ממשיכים בהוכחת משפט השלמות של גדל. כזכור, בפוסט הקודם הוכחנו שאם $latex \Phi$ היא תורה עקבית מקסימלית מעל מילון $latex \tau$ שבנוסף לכך קיימת עבורה קבוצת עדים $latex C$, אז קיים ל-$latex \Phi$ מודל. זה מספיק כדי לסיים את ההוכחה, בתנאי שנוכיח שכל תורה עקבית $latex \Phi$מעל מילון $latex \tau$ ניתן להרחיב לתורה עקבית …

משפט השלמות של גדל, ההוכחה (חלק א')

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

מערכת הוכחה ללוגיקה מסדר ראשון

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

הבעיה העשירית של הילברט – לכל דבר טוב (חסום) יש סוף

בשעה טובה הגענו אל המכשול האחרון שעומד בינינו ובין סיום ההוכחה שהבעיה העשירית של הילברט אינה כריעה – כמת אוניברסלי חסום. אם נצליח להראות שבהינתן ביטוי דיופנטי $latex P$ אפשר להוכיח שגם הביטוי $latex \forall x<n\left(P\right)$ הוא דיופנטי, נסיים. כאן אמורה להיכנס לתמונה העובדה שהוכחנו (בדם יזע ודמעות) שהפונקציה האקספוננציאלית היא דיופנטית. בואו נתחיל בלראות …