garywelz/programming_framework
0
1{2 "schemaVersion": "1.0",3 "discourse": {4 "id": "peano-arithmetic",5 "name": "Peano Arithmetic",6 "subject": "arithmetic",7 "variant": "classical",8 "description": "Axiomatic development of natural number arithmetic. Five axioms, definitions of addition and multiplication, and key theorems (associativity, commutativity, distributivity, order). Based on Landau, Foundations of Analysis.",9 "structure": {10 "axioms": 5,11 "definitions": 2,12 "theorems": 2513 }14 },15 "metadata": {16 "created": "2026-03-15",17 "lastUpdated": "2026-03-15",18 "version": "1.0.0",19 "license": "CC BY 4.0",20 "authors": [21 "Welz, G."22 ],23 "methodology": "Programming Framework",24 "citation": "Welz, G. (2026). Peano Arithmetic Dependency Graph. Programming Framework.",25 "keywords": [26 "Peano",27 "arithmetic",28 "natural numbers",29 "induction",30 "foundations"31 ]32 },33 "sources": [34 {35 "id": "landau",36 "type": "primary",37 "authors": "Landau, E.",38 "title": "Foundations of Analysis",39 "year": "1930",40 "publisher": "Chelsea",41 "edition": "1951",42 "notes": "Canonical development"43 },44 {45 "id": "wikipedia",46 "type": "digital",47 "title": "Peano axioms",48 "url": "https://en.wikipedia.org/wiki/Peano_axioms",49 "notes": "Overview and definitions"50 }51 ],52 "nodes": [53 {54 "id": "A1",55 "type": "axiom",56 "label": "0 is a natural number",57 "shortLabel": "A1",58 "short": "0 ∈ N",59 "colorClass": "axiom"60 },61 {62 "id": "A2",63 "type": "axiom",64 "label": "No predecessor of 0: S(x) ≠ 0",65 "shortLabel": "A2",66 "short": "0 not a successor",67 "colorClass": "axiom"68 },69 {70 "id": "A3",71 "type": "axiom",72 "label": "Successor injective: S(x)=S(y) ⇒ x=y",73 "shortLabel": "A3",74 "short": "S injective",75 "colorClass": "axiom"76 },77 {78 "id": "A4",79 "type": "axiom",80 "label": "Closure: S(x) ∈ N for all x ∈ N",81 "shortLabel": "A4",82 "short": "N closed under S",83 "colorClass": "axiom"84 },85 {86 "id": "A5",87 "type": "axiom",88 "label": "Induction: if 0∈K and (x∈K⇒S(x)∈K) then K=N",89 "shortLabel": "A5",90 "short": "Induction",91 "colorClass": "axiom"92 },93 {94 "id": "T1",95 "type": "theorem",96 "label": "x≠y ⇒ S(x)≠S(y)",97 "shortLabel": "T1",98 "short": "Contrapositive of A3",99 "colorClass": "theorem"100 },101 {102 "id": "T2",103 "type": "theorem",104 "label": "S(x)≠x for all x",105 "shortLabel": "T2",106 "short": "Successor ≠ identity",107 "colorClass": "theorem"108 },109 {110 "id": "T3",111 "type": "theorem",112 "label": "If x≠0 then x=S(u) for some u",113 "shortLabel": "T3",114 "short": "Every nonzero is successor",115 "colorClass": "theorem"116 },117 {118 "id": "DefAdd",119 "type": "definition",120 "label": "Addition: x+0=x, x+S(y)=S(x+y)",121 "shortLabel": "DefAdd",122 "short": "Definition of +",123 "colorClass": "definition"124 },125 {126 "id": "T4",127 "type": "theorem",128 "label": "Addition is well-defined for all x,y",129 "shortLabel": "T4",130 "short": "Add well-defined",131 "colorClass": "theorem"132 },133 {134 "id": "T5",135 "type": "theorem",136 "label": "(x+y)+z = x+(y+z)",137 "shortLabel": "T5",138 "short": "Associativity of +",139 "colorClass": "theorem"140 },141 {142 "id": "T6",143 "type": "theorem",144 "label": "0+x = x",145 "shortLabel": "T6",146 "short": "Left identity",147 "colorClass": "theorem"148 },149 {150 "id": "T7",151 "type": "theorem",152 "label": "S(x)+y = S(x+y)",153 "shortLabel": "T7",154 "short": "Successor and add",155 "colorClass": "theorem"156 },157 {158 "id": "T8",159 "type": "theorem",160 "label": "x+y = y+x",161 "shortLabel": "T8",162 "short": "Commutativity of +",163 "colorClass": "theorem"164 },165 {166 "id": "T9",167 "type": "theorem",168 "label": "x+y=x+z ⇒ y=z",169 "shortLabel": "T9",170 "short": "Cancellation for +",171 "colorClass": "theorem"172 },173 {174 "id": "DefMul",175 "type": "definition",176 "label": "Multiplication: x·0=0, x·S(y)=x·y+x",177 "shortLabel": "DefMul",178 "short": "Definition of ·",179 "colorClass": "definition"180 },181 {182 "id": "T10",183 "type": "theorem",184 "label": "Multiplication is well-defined for all x,y",185 "shortLabel": "T10",186 "short": "Mul well-defined",187 "colorClass": "theorem"188 },189 {190 "id": "T11",191 "type": "theorem",192 "label": "x·0 = 0",193 "shortLabel": "T11",194 "short": "Zero times",195 "colorClass": "theorem"196 },197 {198 "id": "T12",199 "type": "theorem",200 "label": "0·x = 0",201 "shortLabel": "T12",202 "short": "Zero from left",203 "colorClass": "theorem"204 },205 {206 "id": "T13",207 "type": "theorem",208 "label": "S(x)·y = x·y + y",209 "shortLabel": "T13",210 "short": "Successor and mul",211 "colorClass": "theorem"212 },213 {214 "id": "T14",215 "type": "theorem",216 "label": "x·y = y·x",217 "shortLabel": "T14",218 "short": "Commutativity of ·",219 "colorClass": "theorem"220 },221 {222 "id": "T15",223 "type": "theorem",224 "label": "(x·y)·z = x·(y·z)",225 "shortLabel": "T15",226 "short": "Associativity of ·",227 "colorClass": "theorem"228 },229 {230 "id": "T16",231 "type": "theorem",232 "label": "x·(y+z) = x·y + x·z",233 "shortLabel": "T16",234 "short": "Distributivity",235 "colorClass": "theorem"236 },237 {238 "id": "T17",239 "type": "theorem",240 "label": "(x+y)·z = x·z + y·z",241 "shortLabel": "T17",242 "short": "Distributivity (right)",243 "colorClass": "theorem"244 },245 {246 "id": "T18",247 "type": "theorem",248 "label": "x≤y iff ∃z x+z=y",249 "shortLabel": "T18",250 "short": "Order definition",251 "colorClass": "theorem"252 },253 {254 "id": "T19",255 "type": "theorem",256 "label": "Trichotomy: exactly one of x<y, x=y, y<x",257 "shortLabel": "T19",258 "short": "Trichotomy",259 "colorClass": "theorem"260 },261 {262 "id": "T20",263 "type": "theorem",264 "label": "x≤y ⇒ x+z≤y+z",265 "shortLabel": "T20",266 "short": "Order + add",267 "colorClass": "theorem"268 },269 {270 "id": "T21",271 "type": "theorem",272 "label": "x≤y and z>0 ⇒ x·z≤y·z",273 "shortLabel": "T21",274 "short": "Order + mul",275 "colorClass": "theorem"276 },277 {278 "id": "T22",279 "type": "theorem",280 "label": "1·x = x (where 1=S(0))",281 "shortLabel": "T22",282 "short": "Multiplicative identity",283 "colorClass": "theorem"284 },285 {286 "id": "T23",287 "type": "theorem",288 "label": "x·1 = x",289 "shortLabel": "T23",290 "short": "Right identity",291 "colorClass": "theorem"292 },293 {294 "id": "T24",295 "type": "theorem",296 "label": "Well-ordering: every nonempty subset has least element",297 "shortLabel": "T24",298 "short": "Well-ordering",299 "colorClass": "theorem"300 },301 {302 "id": "T25",303 "type": "theorem",304 "label": "Strong induction principle",305 "shortLabel": "T25",306 "short": "Strong induction",307 "colorClass": "theorem"308 }309 ],310 "edges": [311 {312 "from": "A3",313 "to": "T1"314 },315 {316 "from": "A1",317 "to": "T2"318 },319 {320 "from": "A2",321 "to": "T2"322 },323 {324 "from": "A3",325 "to": "T2"326 },327 {328 "from": "T1",329 "to": "T2"330 },331 {332 "from": "A5",333 "to": "T2"334 },335 {336 "from": "A5",337 "to": "T3"338 },339 {340 "from": "A5",341 "to": "DefAdd"342 },343 {344 "from": "DefAdd",345 "to": "T4"346 },347 {348 "from": "A5",349 "to": "T4"350 },351 {352 "from": "DefAdd",353 "to": "T5"354 },355 {356 "from": "A5",357 "to": "T5"358 },359 {360 "from": "DefAdd",361 "to": "T6"362 },363 {364 "from": "A5",365 "to": "T6"366 },367 {368 "from": "DefAdd",369 "to": "T7"370 },371 {372 "from": "T6",373 "to": "T7"374 },375 {376 "from": "A5",377 "to": "T7"378 },379 {380 "from": "DefAdd",381 "to": "T8"382 },383 {384 "from": "T5",385 "to": "T8"386 },387 {388 "from": "T6",389 "to": "T8"390 },391 {392 "from": "T7",393 "to": "T8"394 },395 {396 "from": "A5",397 "to": "T8"398 },399 {400 "from": "DefAdd",401 "to": "T9"402 },403 {404 "from": "T8",405 "to": "T9"406 },407 {408 "from": "A5",409 "to": "T9"410 },411 {412 "from": "DefAdd",413 "to": "DefMul"414 },415 {416 "from": "A5",417 "to": "DefMul"418 },419 {420 "from": "DefMul",421 "to": "T10"422 },423 {424 "from": "A5",425 "to": "T10"426 },427 {428 "from": "DefMul",429 "to": "T11"430 },431 {432 "from": "DefMul",433 "to": "T12"434 },435 {436 "from": "T6",437 "to": "T12"438 },439 {440 "from": "A5",441 "to": "T12"442 },443 {444 "from": "DefMul",445 "to": "T13"446 },447 {448 "from": "T8",449 "to": "T13"450 },451 {452 "from": "A5",453 "to": "T13"454 },455 {456 "from": "DefMul",457 "to": "T14"458 },459 {460 "from": "T12",461 "to": "T14"462 },463 {464 "from": "T13",465 "to": "T14"466 },467 {468 "from": "A5",469 "to": "T14"470 },471 {472 "from": "DefMul",473 "to": "T15"474 },475 {476 "from": "T5",477 "to": "T15"478 },479 {480 "from": "T8",481 "to": "T15"482 },483 {484 "from": "A5",485 "to": "T15"486 },487 {488 "from": "DefMul",489 "to": "T16"490 },491 {492 "from": "T5",493 "to": "T16"494 },495 {496 "from": "T8",497 "to": "T16"498 },499 {500 "from": "T15",501 "to": "T16"502 },503 {504 "from": "A5",505 "to": "T16"506 },507 {508 "from": "T16",509 "to": "T17"510 },511 {512 "from": "T8",513 "to": "T17"514 },515 {516 "from": "DefAdd",517 "to": "T18"518 },519 {520 "from": "T8",521 "to": "T18"522 },523 {524 "from": "T9",525 "to": "T18"526 },527 {528 "from": "T18",529 "to": "T19"530 },531 {532 "from": "T9",533 "to": "T19"534 },535 {536 "from": "T18",537 "to": "T20"538 },539 {540 "from": "T8",541 "to": "T20"542 },543 {544 "from": "T18",545 "to": "T21"546 },547 {548 "from": "T16",549 "to": "T21"550 },551 {552 "from": "T14",553 "to": "T21"554 },555 {556 "from": "DefMul",557 "to": "T22"558 },559 {560 "from": "T6",561 "to": "T22"562 },563 {564 "from": "A5",565 "to": "T22"566 },567 {568 "from": "T14",569 "to": "T23"570 },571 {572 "from": "T22",573 "to": "T23"574 },575 {576 "from": "T18",577 "to": "T24"578 },579 {580 "from": "T19",581 "to": "T24"582 },583 {584 "from": "A5",585 "to": "T24"586 },587 {588 "from": "T18",589 "to": "T25"590 },591 {592 "from": "T24",593 "to": "T25"594 },595 {596 "from": "A5",597 "to": "T25"598 }599 ],600 "colorScheme": {601 "axiom": {602 "fill": "#e74c3c",603 "stroke": "#c0392b"604 },605 "definition": {606 "fill": "#3498db",607 "stroke": "#2980b9"608 },609 "theorem": {610 "fill": "#1abc9c",611 "stroke": "#16a085"612 }613 }614}