Peano Arithmetic — Order & Induction

graph TD A5["A5\nInduction"] DefAdd["DefAdd\nDefinition of +"] T5["T5\nAssociativity of +"] T6["T6\nLeft identity"] T7["T7\nSuccessor and add"] T8["T8\nCommutativity of +"] T9["T9\nCancellation for +"] DefMul["DefMul\nDefinition of ·"] T12["T12\nZero from left"] T13["T13\nSuccessor and mul"] T14["T14\nCommutativity of ·"] T15["T15\nAssociativity of ·"] T16["T16\nDistributivity"] T18["T18\nOrder definition"] T19["T19\nTrichotomy"] T20["T20\nOrder + add"] T21["T21\nOrder + mul"] T22["T22\nMultiplicative identity"] T23["T23\nRight identity"] T24["T24\nWell-ordering"] T25["T25\nStrong induction"] A5 --> DefAdd DefAdd --> T5 A5 --> T5 DefAdd --> T6 A5 --> T6 DefAdd --> T7 T6 --> T7 A5 --> T7 DefAdd --> T8 T5 --> T8 T6 --> T8 T7 --> T8 A5 --> T8 DefAdd --> T9 T8 --> T9 A5 --> T9 DefAdd --> DefMul A5 --> DefMul DefMul --> T12 T6 --> T12 A5 --> T12 DefMul --> T13 T8 --> T13 A5 --> T13 DefMul --> T14 T12 --> T14 T13 --> T14 A5 --> T14 DefMul --> T15 T5 --> T15 T8 --> T15 A5 --> T15 DefMul --> T16 T5 --> T16 T8 --> T16 T15 --> T16 A5 --> T16 DefAdd --> T18 T8 --> T18 T9 --> T18 T18 --> T19 T9 --> T19 T18 --> T20 T8 --> T20 T18 --> T21 T16 --> T21 T14 --> T21 DefMul --> T22 T6 --> T22 A5 --> T22 T14 --> T23 T22 --> T23 T18 --> T24 T19 --> T24 A5 --> T24 T18 --> T25 T24 --> T25 A5 --> T25 classDef axiom fill:#ff6b6b,color:#fff,stroke:#c0392b classDef definition fill:#b197fc,color:#fff,stroke:#9775fa classDef theorem fill:#51cf66,color:#fff,stroke:#40c057 class A5 axiom class DefAdd,DefMul definition class T5,T6,T7,T8,T9,T12,T13,T14,T15,T16,T18,T19,T20,T21,T22,T23,T24,T25 theorem