מערכת פאנו – הבדלי גרסאות

תוכן שנמחק תוכן שנוסף
שורה 5:
==הגדרה פורמלית==
{{סימון מתמטי}}
ל'''מערכת פאנו''' שלושה מרכיבים - [[קבוצה (מתמטיקה)|קבוצה]] <math>\ \omega</math>, קבוע <math>\ 0\in \omega</math>, ופעולה <math>\ S : \omega \rightarrow \omega</math>, המקיימים את האקסיומות הבאות (בעברית נקרא לפעולה זו "פעולת העוקב"):
# אם <math>\ x\in\omega</math>, אז גם <math>\ S(x)\in\omega</math>.
או בעברית: אם x נמצא בקבוצה אז גם העוקב שלו בקבוצה.
# לא קיים <math>\ x=0\in \omega</math> כך ששלכל <math>\ x\in \omega</math> לא מתקיים <math>\ S(x)=0</math> (כלומר, 0 הוא איבר ראשון במערכת).
או בעברית: קיים איבר בקבוצה (ששמו 0), כך שאותו איבר אינו עוקב של אף אחד.
# לכל שני איברים <math>\ x,y\in\omega</math>, אם <math>\ S(x)=S(y)</math> אז גם <math>\ x=y</math> (כלומר - הפונקציה S [[חד חד ערכית]]).
או בעברית: אם ל x ול y יש את אותו העוקב אזי x ו y הם אותו איבר (X=Y).
# [[תת-קבוצה|תת-הקבוצה]] היחידה <math>\ K\subseteq \omega</math> המקיימת את התכונות
#* <math>0 \in K</math>, ו-
#* לכל איבר<math>\ x\in \omega</math>, אם <math>x \in K</math> אז גם <math>S(x) \in K</math>,
: היא <math>\ \omega</math> עצמה. (זוהי [[אינדוקציה מתמטית|אקסיומת האינדוקציה]]).
או בעברית: קבוצת כל העוקבים יחד עם האיבר הראשון (ששמו כאמור הוא 0) היא הקבוצה הנדונה.
 
המספר 1 מוגדר במערכת הזו כעוקב של אפס, 2 מוגדר כעוקב של 1, וכן הלאה. לאחר שמגדירים את פעולת החיבור, אפשר לראות בפעולת העוקב הוספת אחד, כלומר <math>\ S(x)=x+1</math>. האקסיומה השלישית, המאפשרת להגדיר ולהוכיח טענות באינדוקציה, היא ליבה של המערכת. כיוון שהאקסיומה מונה על כל תת-קבוצה K, היא אינה כתובה ב[[שפה מסדר ראשון]]. בתורת ה[[מודל (לוגיקה מתמטית)|מודלים]] וה[[הוכחה פורמלית|הוכחות הפורמליות]] קל יותר לנתח מערכות מסדר ראשון, ואכן קיימת גרסה המחליפה את האקסיומה השלישית ב[[סכמת אקסיומות]], כדלקמן.