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

מתוך ויקיפדיה, האנציקלופדיה החופשית

יש לך הודעות חדשות (השווה לגרסה הקודמת).

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

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

[עריכה] דוגמאות

דוגמה. נבנה שפה מסדר ראשון עם שני יחסים, האחד אונארי (כלומר, בעל מקום אחד) שנסמן ב- P, והשני בינרי, שאותו נסמן ב- A. הפסוק $\ \exists y : (P(y) \and A(x,y))$ אינו יכול לשמש כאקסיומה, משום שיש לו משתנה חופשי (x). הפסוק

$\ \forall x (\neg P(x) \implies \exists y : (P(y) \and A(x,y)))$

יכול לשמש אקסיומה, משום שאין לו משתנים חופשיים. גם

$\ \forall x \forall y\forall z(A(x,z)\and A(y,z)\implies P(z))$

היא אקסיומה אפשרית.

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

כדוגמה נוספת, תורת החבורות עוסקת במבנים אלגבריים הקרויים חבורות. מבנים אלה הם מודלים לתורה, שהשפה שלה כוללת פונקציה בינרית אחת * וקבוע אחד, שסימנו 1, ואת הסימן של יחס השוויון, '='. האקסיומות המגדירות חבורה הן:

$\ \forall x \forall y \forall z ((x*y)*z=x*(y*z))$ ;
$\ \forall x (x*1=x \and 1*x=x)$ ;
$\ \forall x \exists y (x*y=1 \and y*x=1)$ .

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

דוגמה חשובה אחרת, אולי החשובה ביותר, היא זו של תורת הקבוצות האקסיומטית: בשפה יש רק יחס בינרי אחד ( $\ \in$ ) ששמו 'שייכות', ומספר לא גדול של סכימות לגזירת אקסיומות. מערכת האקסיומות היסודית היא מערכת צרמלו-פרנקל, ואותה מסמנים ב- ZF. כאשר מוסיפים לה את אקסיומת הבחירה

לכל x ולכל פונקציה f מ- x, קיימת פונקציה מ- x שעבורה $\ g(a)\in f(a)$ לכל $\ a\in x$ ,

מתקבלת המערכת ZFC (האות C מגיעה מהמלה האנגלית choice). כדי לקבל כאן פסוק חוקי, צריך לפרוש את המושג "פונקציה מ- x" לביטוי המכיל רק את היחס "שייך"; זהו תרגיל קל יחסית.

[עריכה] תכונות של תורה

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

תורה שבה לא ניתן להוכיח אף פסוק מן הצורה $\ \phi \and \neg \phi$ נקראת תורה עקבית. בתורה שאיננה עקבית אפשר להוכיח כל פסוק, ולכן קשה למצוא בכאלה עניין רב. תורה שבה, לכל פסוק נטול משתנים חופשיים, אפשר להוכיח את הפסוק או את שלילתו, נקראת תורה שלמה.