תורה (לוגיקה מתמטית) – הבדלי גרסאות

==דוגמאות==

 

* <math>\ \forall x (\neg P(x) \implies \exists y : (P(y) \and A(x,y)))</math>

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

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

 

* <math>\ \forall x \forall y \forall z ((x*y)*z=x*(y*z))</math>;

* <math>\ \forall x (x*1=x \and 1*x=x)</math>;

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

 

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

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