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