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

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

בדרך כלל כוללים ברשימת האקסיומות גם את כל הטאוטולוגיות, שבהן מותר להציב כל פסוק.

## דוגמאות
**דוגמה**. נבנה שפה מסדר ראשון עם שני יחסים, האחד אונארי (כלומר, בעל מקום אחד) שנסמן ב-P, והשני בינארי, שאותו נסמן ב-A. הפסוק \exists y\,(P(y)\and A(x,y)) אינו יכול לשמש כאקסיומה, משום שיש לו משתנה חופשי (x). הפסוק
:\forall x\,(\neg P(x)\to\exists y\,(P(y)\and A(x,y)))
יכול לשמש אקסיומה, משום שאין לו משתנים חופשיים. גם
:\forall x\,\forall y\,\forall z:\quad(A(x,z)\and A(y,z))\implies P(z)
היא אקסיומה אפשרית.

כמודל לתורה זו, אפשר לחשוב על קבוצת האנשים והצלחות במסעדה, כאשר היחס P מתקיים רק עבור הצלחות, והיחס A(x,y) פירושו כי x,y מצויים באותו שולחן, כלומר בפרט A(x,y) הוא יחס שקילות. במקרה זה, האקסיומה הראשונה אומרת שכל סועד יושב בשולחן עליו יש צלחת, והאקסיומה השנייה אומרת שכל סועד יושב בשולחן משלו (אם x,y סועדים היושבים יחד, אפשר לבחור z=x ולהסיק כי x הוא צלחת).

כדוגמה נוספת, תורת החבורות עוסקת במבנים אלגבריים הנקראים חבורות. מבנים אלה הם מודלים לתורה, שהשפה שלה כוללת פונקציה בינארית אחת * קבוע אחד e, ואת הסימן של יחס השוויון, =. האקסיומות המגדירות חבורה הן:
*אסוציאטיביות: \forall x\,\forall y\,\forall z:\quad(x*y)*z=x*(y*z)
*קיום איבר יחידה: \forall x:\quad x*e=e*x=x
*קיום איבר הופכי: \forall x\,\exists y:\quad x*y=y*x=e
דוגמה מפורסמת לתורה לוגית היא אריתמטיקת פאנו, שהיא תורה המתוכננת לדיון במספרים טבעיים. בשפה שלה יש רק קבוע אחד (0), פונקציה אונארית אחת (פונקציית העוקב), יחס השוויון, וכמה סכימות פשוטות לגזירה של אקסיומות. במאמץ מה אפשר להגדיר בשפה הזו חיבור וכפל, ואז ניתן לנסח בה חלק משמעותי של הטענות באריתמטיקה. תורה כזו, או חזקה ממנה, נקראת **תורה אריתמטית**.

דוגמה חשובה אחרת, אולי החשובה ביותר, היא זו של תורת הקבוצות האקסיומטית: בשפה יש רק יחס בינארי אחד (\in) ששמו 'שייכות', ומספר לא גדול של סכימות לגזירת אקסיומות. מערכת האקסיומות היסודית היא מערכת צרמלו-פרנקל, ואותה מסמנים ב-ZF. כאשר מוסיפים לה את אקסיומת הבחירה שהיא:
*לכל x ולכל פונקציה f מ-x, קיימת פונקציה מ-x שעבורה g(a)\in f(a) לכל a\in x
מתקבלת המערכת ZFC (האות C מגיעה מהמלה האנגלית choice). כדי לקבל כאן פסוק חוקי, צריך לפרוש את המושג "פונקציה מ-x" לביטוי המכיל רק את היחס "שייך"; זהו תרגיל קל יחסית.

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

תורה שבה לא ניתן להוכיח אף פסוק מן הצורה \phi\and\neg\phi נקראת תורה עקבית. בתורה שאיננה עקבית אפשר להוכיח **כל** פסוק, ולכן קשה למצוא בכאלה עניין רב. תורה שבה, לכל פסוק נטול משתנים חופשיים, אפשר להוכיח את הפסוק או את שלילתו, נקראת תורה שלמה. תורה שיש לה מודל יחיד (עד כדי איזומורפיזם) מעוצמה \kappa היא \kappa-קטגורית. תורה שאין לה מודלים סופיים והיא \kappa-קטגורית (לאיזושהי עוצמה אינסופית הגדולה או שווה לעוצמת השפה) היא שלמה. תורה היא אריתמטית אם יש לה מודל שמכיל מודל שאיזומורפי לאריתמטיקה החלשה (קבוצת הטבעיים יחד עם 4 פעולות חשבון, פונקציה אונרית "עוקב של" והיחסים =,. לאריתמטיקה החלשה 7 אקסיומות שהן אקסיומות פיאנו למעט אקסיומת האינדוקציה שהיא מסדר שני).

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

בהינתן מבנה מתמטי  בשפה מסדר ראשון L, **התורה השלמה** של M בשפה זו היא אוסף כל הנוסחאות המסתפקות על ידי המודל M; תורה זו מסומנת \text{Th}(M). זו תמיד תורה שלמה, וכל מודל שלה שקול אלמנטרית ל-M; אם M אינסופי, ייתכנו מודלים של \text{Th}(M) שאינם איזומורפיים ל-M. למשל, קיימים מודלים של התורה השלמה של המספרים הטבעיים (בשפת אריתמטיקת פאנו) שאינם איזומורפיים להם – המודלים הלא-סטנדרטיים של האריתמטיקה.

## ראו גם
*שפה מסדר ראשון
*מודל (לוגיקה מתמטית)
*הוכחה (לוגיקה מתמטית)

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