מערכת פאנו | הגדרה פורמלית
English: Peano axioms

הגדרה פורמלית

Nuvola apps edu mathematics blue-p.svg

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

למערכת פאנו שלושה מרכיבים - קבוצה , קבוע , ופעולה , המקיימים את האקסיומות הבאות (בעברית נקרא לפעולה זו "פעולת העוקב"):

  1. קיים כך שלכל לא מתקיים (כלומר, 0 הוא איבר ראשון במערכת).
  2. לכל שני איברים , אם אז גם (כלומר - הפונקציה S חד חד ערכית).
  3. תת-הקבוצה היחידה המקיימת את התכונות
    • , ו-
    • לכל איבר , אם אז גם ,
היא עצמה. (זוהי אקסיומת האינדוקציה).

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

3'. לכל נוסחה בשפה, קיימת האקסיומה

כאשר הוא קיצור עבור .

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

המערכת הכוללת את שתי האקסיומות 1 ו-2 לעיל ואת סכימת האקסיומות 3' קרויה אריתמטיקת פאנו, ומסומנת בדרך-כלל באותיות PA.