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

ל'''מערכת פאנו''' שלושה מרכיבים - [[קבוצה (מתמטיקה)|קבוצה]] <math>\ \omega</math>, קבוע <math>\ 0\in \omega</math>, ופעולה <math>\ S :\colon \omega \rightarrowto \omega</math>, המקיימים את האקסיומות הבאות (בעברית נקרא לפעולה זו "פעולת העוקב"):

# קיים <math>\ 0\in \omega</math> כך שלכל <math>\ x\in \omega</math> לא מתקיים <math>\ S(x)=0</math> (כלומר, <math>0</math> הוא איבר ראשון במערכת).

# לכל שני איברים <math>\ x,y\in\omega</math>, אם <math>\ S(x)=S(y)</math> אז גם <math>\ x=y</math> (כלומר - הפונקציה <math>S</math> [[חד חד ערכית]]).

המספר 1 מוגדר במערכת הזו כעוקב של אפס, 2 מוגדר כעוקב של 1, וכן הלאה. לאחר שמגדירים את פעולת החיבור, אפשר לראות בפעולת העוקב הוספת אחד, כלומר <math>\ S(x)=x+1</math>. האקסיומה השלישית, המאפשרת להגדיר ולהוכיח טענות באינדוקציה, היא ליבה של המערכת. כיוון שהאקסיומה מונה על כל תת-קבוצה <math>K</math>, היא אינה כתובה ב[[שפה מסדר ראשון]]. בתורת ה[[מודל (לוגיקה מתמטית)|מודלים]] וה[[הוכחה פורמלית|הוכחות הפורמליות]] קל יותר לנתח מערכות מסדר ראשון, ואכן קיימת גרסה המחליפה את האקסיומה השלישית ב[[סכמת אקסיומות]], כדלקמן.

בשפה מסדר ראשון לא ניתן למנות על "כל קבוצה", כפי שעושה האקסיומה השלישית. סכימת האקסיומות, הכוללת מספר בן-מניה של אקסיומות מסדר ראשון (אחת לכל נוסחה), מבטאת את אותה טענה, אבל מסתפקת בקבוצות שהן, במובן של הלוגיקה הפורמלית, [[קבוצה ניתנת להגדרה|ניתנות להגדרה]]. האקסיומה קובעת שאם <math>0</math> מקיים תכונה מסוימת, ולכל <math>x</math>, אם <math>x</math> מקיים אותה אז גם <math>x+1</math> מקיים אותה, אז התכונה מתקיימת לכל <math>x</math>.

ה[[חיבור]], שסימנו <math>+</math>, הוא [[פעולה בינארית]] המוגדרת באופן הבא:

* בסיס: לכל <math>x</math> טבעי מתקיים <math>\ x \times 0 = 0</math>.

* השלב הרקורסיבי: לכל <math>x,y</math> טבעיים מתקיים <math>x \times S(y)=x+(x \times y)</math>.

מהגדרה זו מקבלים שהעוקב של <math>0</math>, <math>\ S(0)</math> הוא [[איבר יחידה]] ביחס לכפל (לכל x טבעי מתקיים: <math>x \times S(0)=x+(x \times 0)=x+0=x</math>), וסימונו המקובל הוא [[1 (מספר)|1]]. מהגדרת החיבור נובע <math>\ s(x) = x+1</math>. לפי הסימון החדש פעולת החיבור מוגדרת לפי <math>\ x+(y+1) = (x+y) +1</math> ופעולת הכפל מוגדרת <math>\ x \times (y+1) = x + (x \times y)</math>.

[[ריכרד דדקינד]] הוכיח שמערכת האקסיומות של פאנו (עם אקסיומת האינדוקציה מסדר שני) היא [[מערכת קטגורית|קטגורית]], כלומר: כל שני [[מודל (לוגיקה מתמטית)|מודלים]] של מערכת זו הם [[איזומורפיזם|איזומורפיים]]. בניסוח פורמלי יותר: אם <math>\ <langle \omega_A,0_A,S_A >\rangle </math> ו- <math>\ <langle \omega_B,0_B,S_B >\rangle </math> הם שני מודלים של מערכת פאנו, אז הפונקציה <math>\ f: \colon \omega_A \to \omega_B </math>, המוגדרת (על-פי אקסיומת האינדוקציה של המערכת הראשונה) על ידי <math>\ f(0_A)=0_B, f(S_A(x))=S_B(f(x))</math>, היא איזומורפיזם בין המבנים.

* נגדיר את המספר <math>0</math> כ[[הקבוצה הריקה|קבוצה הריקה]] <math>\emptyset</math>.

כעת ניתן להגדיר על הטבעיים [[סדר חלקי]] פשוט באמצעות [[תת קבוצה|הכלה]] (כהגדרתה בתורת הקבוצות) באופן הבא: לכל <math>x,y</math> טבעיים נגדיר <math>x \le y</math> [[אם ורק אם]] <math>x \subseteq y</math>. לפי [[עקרון הסדר הטוב]] זהו [[סדר טוב]].