garywelz/programming_framework
0
1{2 "schemaVersion": "1.0",3 "discourse": {4 "id": "propositional-logic",5 "name": "Propositional Logic",6 "subject": "logic",7 "variant": "classical",8 "description": "Hilbert-style axiomatic development of classical propositional logic. Three axioms (Łukasiewicz P2), modus ponens, definitions of disjunction, conjunction, biconditional, and key theorems (double negation, De Morgan, excluded middle, deduction theorem).",9 "structure": {10 "axioms": 4,11 "definitions": 3,12 "theorems": 1913 }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). Propositional Logic Dependency Graph. Programming Framework.",25 "keywords": [26 "propositional logic",27 "Hilbert",28 "Łukasiewicz",29 "tautology",30 "modus ponens"31 ]32 },33 "sources": [34 {35 "id": "frege",36 "type": "primary",37 "authors": "Frege, G.",38 "title": "Begriffsschrift",39 "year": "1879",40 "notes": "First axiomatic propositional logic"41 },42 {43 "id": "lukasiewicz",44 "type": "primary",45 "authors": "Łukasiewicz, J.",46 "title": "Elements of Mathematical Logic",47 "year": "1929",48 "notes": "P2: 3 axioms"49 },50 {51 "id": "wikipedia",52 "type": "digital",53 "title": "Propositional calculus",54 "url": "https://en.wikipedia.org/wiki/Propositional_calculus",55 "notes": "Axioms and theorems"56 }57 ],58 "nodes": [59 {60 "id": "A1",61 "type": "axiom",62 "label": "φ → (ψ → φ)",63 "shortLabel": "A1",64 "short": "Weakening",65 "colorClass": "axiom"66 },67 {68 "id": "A2",69 "type": "axiom",70 "label": "(φ→(ψ→χ)) → ((φ→ψ)→(φ→χ))",71 "shortLabel": "A2",72 "short": "Distrib. of impl.",73 "colorClass": "axiom"74 },75 {76 "id": "A3",77 "type": "axiom",78 "label": "(¬φ→¬ψ) → (ψ→φ)",79 "shortLabel": "A3",80 "short": "Contraposition",81 "colorClass": "axiom"82 },83 {84 "id": "MP",85 "type": "axiom",86 "label": "Modus Ponens: φ, (φ→ψ) ⊢ ψ",87 "shortLabel": "MP",88 "short": "MP",89 "colorClass": "axiom"90 },91 {92 "id": "T1",93 "type": "theorem",94 "label": "φ → φ",95 "shortLabel": "T1",96 "short": "Self-implication",97 "colorClass": "theorem"98 },99 {100 "id": "T2",101 "type": "theorem",102 "label": "¬¬φ → φ",103 "shortLabel": "T2",104 "short": "Double neg. elim",105 "colorClass": "theorem"106 },107 {108 "id": "T3",109 "type": "theorem",110 "label": "φ → ¬¬φ",111 "shortLabel": "T3",112 "short": "Double neg. intro",113 "colorClass": "theorem"114 },115 {116 "id": "T4",117 "type": "theorem",118 "label": "(φ→ψ) → (¬ψ→¬φ)",119 "shortLabel": "T4",120 "short": "Transposition",121 "colorClass": "theorem"122 },123 {124 "id": "T5",125 "type": "theorem",126 "label": "(φ→ψ)∧(ψ→χ) ⇒ (φ→χ)",127 "shortLabel": "T5",128 "short": "Hyp. syllogism",129 "colorClass": "theorem"130 },131 {132 "id": "DefOr",133 "type": "definition",134 "label": "φ ∨ ψ := ¬φ → ψ",135 "shortLabel": "DefOr",136 "short": "Def. disjunction",137 "colorClass": "definition"138 },139 {140 "id": "DefAnd",141 "type": "definition",142 "label": "φ ∧ ψ := ¬(φ → ¬ψ)",143 "shortLabel": "DefAnd",144 "short": "Def. conjunction",145 "colorClass": "definition"146 },147 {148 "id": "DefIff",149 "type": "definition",150 "label": "φ ↔ ψ := (φ→ψ)∧(ψ→φ)",151 "shortLabel": "DefIff",152 "short": "Def. biconditional",153 "colorClass": "definition"154 },155 {156 "id": "T6",157 "type": "theorem",158 "label": "φ → (φ ∨ ψ)",159 "shortLabel": "T6",160 "short": "Addition (∨I)",161 "colorClass": "theorem"162 },163 {164 "id": "T7",165 "type": "theorem",166 "label": "(φ∧ψ) → φ",167 "shortLabel": "T7",168 "short": "Simplification (∧E)",169 "colorClass": "theorem"170 },171 {172 "id": "T8",173 "type": "theorem",174 "label": "(φ∧ψ) → ψ",175 "shortLabel": "T8",176 "short": "Simplification (∧E)",177 "colorClass": "theorem"178 },179 {180 "id": "T9",181 "type": "theorem",182 "label": "φ → (ψ → (φ∧ψ))",183 "shortLabel": "T9",184 "short": "Conjunction (∧I)",185 "colorClass": "theorem"186 },187 {188 "id": "T10",189 "type": "theorem",190 "label": "(φ→ψ) ↔ (¬φ∨ψ)",191 "shortLabel": "T10",192 "short": "Material impl.",193 "colorClass": "theorem"194 },195 {196 "id": "T11",197 "type": "theorem",198 "label": "¬(φ∧ψ) ↔ (¬φ∨¬ψ)",199 "shortLabel": "T11",200 "short": "De Morgan (1)",201 "colorClass": "theorem"202 },203 {204 "id": "T12",205 "type": "theorem",206 "label": "¬(φ∨ψ) ↔ (¬φ∧¬ψ)",207 "shortLabel": "T12",208 "short": "De Morgan (2)",209 "colorClass": "theorem"210 },211 {212 "id": "T13",213 "type": "theorem",214 "label": "φ ∨ ¬φ",215 "shortLabel": "T13",216 "short": "Excluded middle",217 "colorClass": "theorem"218 },219 {220 "id": "T14",221 "type": "theorem",222 "label": "¬(φ ∧ ¬φ)",223 "shortLabel": "T14",224 "short": "Non-contradiction",225 "colorClass": "theorem"226 },227 {228 "id": "T15",229 "type": "theorem",230 "label": "(φ∧¬φ) → ψ",231 "shortLabel": "T15",232 "short": "Explosion",233 "colorClass": "theorem"234 },235 {236 "id": "T16",237 "type": "theorem",238 "label": "(φ∨ψ) ↔ (ψ∨φ)",239 "shortLabel": "T16",240 "short": "Commutation (∨)",241 "colorClass": "theorem"242 },243 {244 "id": "T17",245 "type": "theorem",246 "label": "(φ∧ψ) ↔ (ψ∧φ)",247 "shortLabel": "T17",248 "short": "Commutation (∧)",249 "colorClass": "theorem"250 },251 {252 "id": "T18",253 "type": "theorem",254 "label": "(φ∧(ψ∨χ)) ↔ ((φ∧ψ)∨(φ∧χ))",255 "shortLabel": "T18",256 "short": "Distribution",257 "colorClass": "theorem"258 },259 {260 "id": "T19",261 "type": "theorem",262 "label": "Deduction theorem",263 "shortLabel": "T19",264 "short": "Deduction thm",265 "colorClass": "theorem"266 }267 ],268 "edges": [269 {270 "from": "A1",271 "to": "T1"272 },273 {274 "from": "A2",275 "to": "T1"276 },277 {278 "from": "MP",279 "to": "T1"280 },281 {282 "from": "A3",283 "to": "T2"284 },285 {286 "from": "T1",287 "to": "T2"288 },289 {290 "from": "MP",291 "to": "T2"292 },293 {294 "from": "A1",295 "to": "T3"296 },297 {298 "from": "A3",299 "to": "T3"300 },301 {302 "from": "MP",303 "to": "T3"304 },305 {306 "from": "A3",307 "to": "T4"308 },309 {310 "from": "T2",311 "to": "T4"312 },313 {314 "from": "T3",315 "to": "T4"316 },317 {318 "from": "MP",319 "to": "T4"320 },321 {322 "from": "A2",323 "to": "T5"324 },325 {326 "from": "T1",327 "to": "T5"328 },329 {330 "from": "MP",331 "to": "T5"332 },333 {334 "from": "A1",335 "to": "DefOr"336 },337 {338 "from": "A2",339 "to": "DefOr"340 },341 {342 "from": "A3",343 "to": "DefOr"344 },345 {346 "from": "MP",347 "to": "DefOr"348 },349 {350 "from": "DefOr",351 "to": "DefAnd"352 },353 {354 "from": "A3",355 "to": "DefAnd"356 },357 {358 "from": "MP",359 "to": "DefAnd"360 },361 {362 "from": "DefAnd",363 "to": "DefIff"364 },365 {366 "from": "T9",367 "to": "DefIff"368 },369 {370 "from": "MP",371 "to": "DefIff"372 },373 {374 "from": "DefOr",375 "to": "T6"376 },377 {378 "from": "A1",379 "to": "T6"380 },381 {382 "from": "MP",383 "to": "T6"384 },385 {386 "from": "DefAnd",387 "to": "T7"388 },389 {390 "from": "A1",391 "to": "T7"392 },393 {394 "from": "A3",395 "to": "T7"396 },397 {398 "from": "MP",399 "to": "T7"400 },401 {402 "from": "DefAnd",403 "to": "T8"404 },405 {406 "from": "A1",407 "to": "T8"408 },409 {410 "from": "A3",411 "to": "T8"412 },413 {414 "from": "MP",415 "to": "T8"416 },417 {418 "from": "A1",419 "to": "T9"420 },421 {422 "from": "A2",423 "to": "T9"424 },425 {426 "from": "MP",427 "to": "T9"428 },429 {430 "from": "DefOr",431 "to": "T10"432 },433 {434 "from": "T4",435 "to": "T10"436 },437 {438 "from": "MP",439 "to": "T10"440 },441 {442 "from": "DefAnd",443 "to": "T11"444 },445 {446 "from": "DefOr",447 "to": "T11"448 },449 {450 "from": "T4",451 "to": "T11"452 },453 {454 "from": "T6",455 "to": "T11"456 },457 {458 "from": "MP",459 "to": "T11"460 },461 {462 "from": "DefAnd",463 "to": "T12"464 },465 {466 "from": "DefOr",467 "to": "T12"468 },469 {470 "from": "T4",471 "to": "T12"472 },473 {474 "from": "MP",475 "to": "T12"476 },477 {478 "from": "DefOr",479 "to": "T13"480 },481 {482 "from": "T2",483 "to": "T13"484 },485 {486 "from": "T3",487 "to": "T13"488 },489 {490 "from": "MP",491 "to": "T13"492 },493 {494 "from": "DefAnd",495 "to": "T14"496 },497 {498 "from": "T4",499 "to": "T14"500 },501 {502 "from": "MP",503 "to": "T14"504 },505 {506 "from": "DefAnd",507 "to": "T15"508 },509 {510 "from": "A1",511 "to": "T15"512 },513 {514 "from": "A2",515 "to": "T15"516 },517 {518 "from": "MP",519 "to": "T15"520 },521 {522 "from": "DefOr",523 "to": "T16"524 },525 {526 "from": "T4",527 "to": "T16"528 },529 {530 "from": "MP",531 "to": "T16"532 },533 {534 "from": "DefAnd",535 "to": "T17"536 },537 {538 "from": "T9",539 "to": "T17"540 },541 {542 "from": "MP",543 "to": "T17"544 },545 {546 "from": "DefAnd",547 "to": "T18"548 },549 {550 "from": "DefOr",551 "to": "T18"552 },553 {554 "from": "T6",555 "to": "T18"556 },557 {558 "from": "T7",559 "to": "T18"560 },561 {562 "from": "T8",563 "to": "T18"564 },565 {566 "from": "T9",567 "to": "T18"568 },569 {570 "from": "MP",571 "to": "T18"572 },573 {574 "from": "A1",575 "to": "T19"576 },577 {578 "from": "A2",579 "to": "T19"580 },581 {582 "from": "MP",583 "to": "T19"584 }585 ],586 "colorScheme": {587 "axiom": {588 "fill": "#e74c3c",589 "stroke": "#c0392b"590 },591 "definition": {592 "fill": "#3498db",593 "stroke": "#2980b9"594 },595 "theorem": {596 "fill": "#1abc9c",597 "stroke": "#16a085"598 }599 }600}