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

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

נניח שפה מסדר ראשון עם יחס אונארי P ויחס בינארי A. הנוסחה ∃y (P(y) ∧ A(x,y)) אינה אקסיומה כי יש לה משתנה חופשי x.
לעומת זאת, נוסחה כ־∀x (¬P(x) → ∃y (P(y) ∧ A(x,y))) אינה מכילה משתנים חופשיים ויכולה להיות אקסיומה.
גם ∀x ∀y ∀z ((A(x,z) ∧ A(y,z)) → P(z)) היא אקסיומה אפשרית.
כמודל אפשר לדמיין אנשים וצלחות במסעדה. P הוא יחס ל"צלחות", ו‑A(x,y) אומר ש‑x ו‑y נמצאים על אותו שולחן.
אז האקסיומה הראשונה אומרת: לכל סועד יש על שולחנו צלחת. האקסיומה השנייה מבטאת יחס לוגי בין ישיבה וצורות אחרות במודל.

דוגמאות נוספות: תורת החבורות מתארת חבורות, מבנים אלגבריים שהם מודלים של תורה שמכילה פונקציה בינארית *, קבוע e ושוויון.
אריתמטיקת פאנו היא תורה לעיסוק במספרים הטבעיים. בשפתה יש 0, פונקציית העוקב (successor) ושוויון.
ניתן להגדיר בשפה זו חיבור וכפל ולהביע חלק גדול מהטענות של האריתמטיקה; תורה כזו נקראת תורה אריתמטית.
תורת הקבוצות משתמשת רק ביחס השייכות ∈. המערכת הסטנדרטית נקראת ZF; אם מוסיפים את אקסיומת הבחירה מקבלים ZFC.
כדי לבטא למשל "פונקציה מ‑x" בשפה של השייכות, מפרשים אותה באמצעות ∈ בלבד; זהו תרגיל טכני ידוע.

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

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

לסיום, נתון מבנה M בשפה L, התורה המלאה של M, Th(M), היא אוסף כל הנוסחאות שהמודל M מספק. זוהי תמיד תורה שלמה.
כל מודל של Th(M) הוא שקול אלמנטרית ל‑M; אם M אינסופי יכולים להתקיים מודלים של Th(M) שאינם איזומורפיים ל‑M. דוגמה ידועה היא המודלים הלא‑סטנדרטיים של האריתמטיקה.

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

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

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