garywelz/programming_framework
0
1#!/usr/bin/env node2/**3 * Build Propositional Logic discourse JSON and Mermaid.4 * Hilbert-style (Łukasiewicz P2): 3 axioms + MP, definitions of ∨∧↔, key theorems.5 * Based on Frege, Łukasiewicz, Church; Wikipedia Propositional calculus.6 */7 8const fs = require('fs');9const path = require('path');10 11const NODES = [12 { id: "A1", type: "axiom", label: "φ → (ψ → φ)", short: "Weakening", colorClass: "axiom" },13 { id: "A2", type: "axiom", label: "(φ→(ψ→χ)) → ((φ→ψ)→(φ→χ))", short: "Distrib. of impl.", colorClass: "axiom" },14 { id: "A3", type: "axiom", label: "(¬φ→¬ψ) → (ψ→φ)", short: "Contraposition", colorClass: "axiom" },15 { id: "MP", type: "axiom", label: "Modus Ponens: φ, (φ→ψ) ⊢ ψ", short: "MP", colorClass: "axiom" },16 { id: "T1", type: "theorem", label: "φ → φ", short: "Self-implication", colorClass: "theorem" },17 { id: "T2", type: "theorem", label: "¬¬φ → φ", short: "Double neg. elim", colorClass: "theorem" },18 { id: "T3", type: "theorem", label: "φ → ¬¬φ", short: "Double neg. intro", colorClass: "theorem" },19 { id: "T4", type: "theorem", label: "(φ→ψ) → (¬ψ→¬φ)", short: "Transposition", colorClass: "theorem" },20 { id: "T5", type: "theorem", label: "(φ→ψ)∧(ψ→χ) ⇒ (φ→χ)", short: "Hyp. syllogism", colorClass: "theorem" },21 { id: "DefOr", type: "definition", label: "φ ∨ ψ := ¬φ → ψ", short: "Def. disjunction", colorClass: "definition" },22 { id: "DefAnd", type: "definition", label: "φ ∧ ψ := ¬(φ → ¬ψ)", short: "Def. conjunction", colorClass: "definition" },23 { id: "DefIff", type: "definition", label: "φ ↔ ψ := (φ→ψ)∧(ψ→φ)", short: "Def. biconditional", colorClass: "definition" },24 { id: "T6", type: "theorem", label: "φ → (φ ∨ ψ)", short: "Addition (∨I)", colorClass: "theorem" },25 { id: "T7", type: "theorem", label: "(φ∧ψ) → φ", short: "Simplification (∧E)", colorClass: "theorem" },26 { id: "T8", type: "theorem", label: "(φ∧ψ) → ψ", short: "Simplification (∧E)", colorClass: "theorem" },27 { id: "T9", type: "theorem", label: "φ → (ψ → (φ∧ψ))", short: "Conjunction (∧I)", colorClass: "theorem" },28 { id: "T10", type: "theorem", label: "(φ→ψ) ↔ (¬φ∨ψ)", short: "Material impl.", colorClass: "theorem" },29 { id: "T11", type: "theorem", label: "¬(φ∧ψ) ↔ (¬φ∨¬ψ)", short: "De Morgan (1)", colorClass: "theorem" },30 { id: "T12", type: "theorem", label: "¬(φ∨ψ) ↔ (¬φ∧¬ψ)", short: "De Morgan (2)", colorClass: "theorem" },31 { id: "T13", type: "theorem", label: "φ ∨ ¬φ", short: "Excluded middle", colorClass: "theorem" },32 { id: "T14", type: "theorem", label: "¬(φ ∧ ¬φ)", short: "Non-contradiction", colorClass: "theorem" },33 { id: "T15", type: "theorem", label: "(φ∧¬φ) → ψ", short: "Explosion", colorClass: "theorem" },34 { id: "T16", type: "theorem", label: "(φ∨ψ) ↔ (ψ∨φ)", short: "Commutation (∨)", colorClass: "theorem" },35 { id: "T17", type: "theorem", label: "(φ∧ψ) ↔ (ψ∧φ)", short: "Commutation (∧)", colorClass: "theorem" },36 { id: "T18", type: "theorem", label: "(φ∧(ψ∨χ)) ↔ ((φ∧ψ)∨(φ∧χ))", short: "Distribution", colorClass: "theorem" },37 { id: "T19", type: "theorem", label: "Deduction theorem", short: "Deduction thm", colorClass: "theorem" }38];39 40// Dependencies (from → to). Based on Hilbert/Łukasiewicz P2 development.41const DEPS = {42 T1: ["A1", "A2", "MP"],43 T2: ["A3", "T1", "MP"],44 T3: ["A1", "A3", "MP"],45 T4: ["A3", "T2", "T3", "MP"],46 T5: ["A2", "T1", "MP"],47 DefOr: ["A1", "A2", "A3", "MP"],48 DefAnd: ["DefOr", "A3", "MP"],49 DefIff: ["DefAnd", "T9", "MP"],50 T6: ["DefOr", "A1", "MP"],51 T7: ["DefAnd", "A1", "A3", "MP"],52 T8: ["DefAnd", "A1", "A3", "MP"],53 T9: ["A1", "A2", "MP"],54 T10: ["DefOr", "T4", "MP"],55 T11: ["DefAnd", "DefOr", "T4", "T6", "MP"],56 T12: ["DefAnd", "DefOr", "T4", "MP"],57 T13: ["DefOr", "T2", "T3", "MP"],58 T14: ["DefAnd", "T4", "MP"],59 T15: ["DefAnd", "A1", "A2", "MP"],60 T16: ["DefOr", "T4", "MP"],61 T17: ["DefAnd", "T9", "MP"],62 T18: ["DefAnd", "DefOr", "T6", "T7", "T8", "T9", "MP"],63 T19: ["A1", "A2", "MP"]64};65 66const discourse = {67 schemaVersion: "1.0",68 discourse: {69 id: "propositional-logic",70 name: "Propositional Logic",71 subject: "logic",72 variant: "classical",73 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).",74 structure: { axioms: 4, definitions: 3, theorems: 19 }75 },76 metadata: {77 created: "2026-03-15",78 lastUpdated: "2026-03-15",79 version: "1.0.0",80 license: "CC BY 4.0",81 authors: ["Welz, G."],82 methodology: "Programming Framework",83 citation: "Welz, G. (2026). Propositional Logic Dependency Graph. Programming Framework.",84 keywords: ["propositional logic", "Hilbert", "Łukasiewicz", "tautology", "modus ponens"]85 },86 sources: [87 { id: "frege", type: "primary", authors: "Frege, G.", title: "Begriffsschrift", year: "1879", notes: "First axiomatic propositional logic" },88 { id: "lukasiewicz", type: "primary", authors: "Łukasiewicz, J.", title: "Elements of Mathematical Logic", year: "1929", notes: "P2: 3 axioms" },89 { id: "wikipedia", type: "digital", title: "Propositional calculus", url: "https://en.wikipedia.org/wiki/Propositional_calculus", notes: "Axioms and theorems" }90 ],91 nodes: [],92 edges: [],93 colorScheme: {94 axiom: { fill: "#e74c3c", stroke: "#c0392b" },95 definition: { fill: "#3498db", stroke: "#2980b9" },96 theorem: { fill: "#1abc9c", stroke: "#16a085" }97 }98};99 100// Add nodes101for (const n of NODES) {102 discourse.nodes.push({103 id: n.id,104 type: n.type,105 label: n.label,106 shortLabel: n.id,107 short: n.short,108 colorClass: n.colorClass109 });110 for (const dep of DEPS[n.id] || []) {111 discourse.edges.push({ from: dep, to: n.id });112 }113}114 115// Write JSON116const dataDir = path.join(__dirname, "..", "data");117const outPath = path.join(dataDir, "propositional-logic.json");118fs.mkdirSync(dataDir, { recursive: true });119fs.writeFileSync(outPath, JSON.stringify(discourse, null, 2), "utf8");120console.log("Wrote", outPath);121 122// Sanitize label for Mermaid (Unicode arrows/symbols can cause "Syntax error in text")123function sanitizeMermaidLabel(s) {124 return String(s)125 .replace(/→/g, "impl")126 .replace(/⊢/g, "|-")127 .replace(/∨/g, "or")128 .replace(/∧/g, "and")129 .replace(/↔/g, "iff")130 .replace(/\n/g, " ");131}132 133// Generate Mermaid - use parentheses for node shape (more robust than brackets)134function toMermaid(filter) {135 const nodes = filter ? discourse.nodes.filter(filter) : discourse.nodes;136 const nodeIds = new Set(nodes.map(n => n.id));137 const edges = discourse.edges.filter(e => nodeIds.has(e.from) && nodeIds.has(e.to));138 const lines = ["graph TD"];139 for (const n of nodes) {140 const desc = n.short || n.label;141 const raw = (n.shortLabel || n.id) + " " + (desc.length > 30 ? desc.slice(0, 27) + "..." : desc);142 const lbl = sanitizeMermaidLabel(raw).replace(/"/g, '\\"');143 lines.push(` ${n.id}("${lbl}")`);144 }145 for (const e of edges) {146 lines.push(` ${e.from} --> ${e.to}`);147 }148 lines.push(" classDef axiom fill:#e74c3c,color:#fff,stroke:#c0392b");149 lines.push(" classDef definition fill:#3498db,color:#fff,stroke:#2980b9");150 lines.push(" classDef theorem fill:#1abc9c,color:#fff,stroke:#16a085");151 const axiomIds = nodes.filter(n => n.type === "axiom").map(n => n.id).join(",");152 const defIds = nodes.filter(n => n.type === "definition").map(n => n.id).join(",");153 const thmIds = nodes.filter(n => n.type === "theorem").map(n => n.id).join(",");154 if (axiomIds) lines.push(` class ${axiomIds} axiom`);155 if (defIds) lines.push(` class ${defIds} definition`);156 if (thmIds) lines.push(` class ${thmIds} theorem`);157 return lines.join("\n");158}159 160function closure(ids) {161 const needed = new Set(ids);162 let changed = true;163 while (changed) {164 changed = false;165 for (const e of discourse.edges) {166 if (needed.has(e.to) && !needed.has(e.from)) { needed.add(e.from); changed = true; }167 }168 }169 return n => needed.has(n.id);170}171 172function toMermaidWithCounts(filter) {173 const nodes = filter ? discourse.nodes.filter(filter) : discourse.nodes;174 const nodeIds = new Set(nodes.map(n => n.id));175 const edges = discourse.edges.filter(e => nodeIds.has(e.from) && nodeIds.has(e.to));176 return { mermaid: toMermaid(filter), nodes: nodes.length, edges: edges.length };177}178 179// 3 sections180const sections = [181 { name: "axioms-implication", ids: ["A1","A2","A3","MP","T1","T2","T3","T4","T5"], title: "Axioms & Implication", desc: "Three Hilbert axioms, modus ponens, self-implication, double negation, transposition, hypothetical syllogism" },182 { name: "definitions-connectives", ids: ["DefOr","DefAnd","DefIff","T6","T7","T8","T9","T10","T11","T12"], title: "Definitions & Connectives", desc: "Definitions of disjunction, conjunction, biconditional; simplification, addition, material implication, De Morgan" },183 { name: "tautologies-metalogic", ids: ["T13","T14","T15","T16","T17","T18","T19"], title: "Tautologies & Metalogic", desc: "Excluded middle, non-contradiction, explosion, commutation, distribution, deduction theorem" }184];185 186const subgraphData = [];187for (const s of sections) {188 const filter = closure(s.ids);189 const { mermaid: sub, nodes: n, edges: e } = toMermaidWithCounts(filter);190 subgraphData.push({ ...s, mermaid: sub, nodes: n, edges: e });191 fs.writeFileSync(path.join(dataDir, `propositional-logic-${s.name}.mmd`), sub, "utf8");192 console.log("Wrote", path.join(dataDir, `propositional-logic-${s.name}.mmd`));193}194 195// Full graph196fs.writeFileSync(path.join(dataDir, "propositional-logic.mmd"), toMermaid(), "utf8");197 198// Generate HTML199const MATH_DB = process.env.MATH_DB || "/home/gdubs/copernicus-web-public/huggingface-space/mathematics-processes-database";200const DISC_DIR = path.join(MATH_DB, "processes", "discrete_mathematics");201 202function htmlTemplate(title, subtitle, mermaid, nodes, edges) {203 const mermaidEscaped = mermaid.replace(/</g, "<").replace(/>/g, ">");204 return `<!DOCTYPE html>205<html lang="en">206<head>207 <meta charset="UTF-8">208 <meta name="viewport" content="width=device-width, initial-scale=1.0">209 <title>${title} - Mathematics Process</title>210 <script src="https://cdn.jsdelivr.net/npm/mermaid@10.6.1/dist/mermaid.min.js"></script>211 <style>212 * { margin: 0; padding: 0; box-sizing: border-box; }213 body { font-family: 'Segoe UI', Tahoma, Geneva, Verdana, sans-serif; background: linear-gradient(135deg, #8e44ad 0%, #3498db 100%); min-height: 100vh; padding: 20px; }214 .container { max-width: 1600px; margin: 0 auto; background: white; border-radius: 15px; box-shadow: 0 20px 40px rgba(0,0,0,0.1); overflow: hidden; }215 .header { background: linear-gradient(135deg, #8e44ad 0%, #9b59b6 100%); color: white; padding: 30px; }216 .header h1 { margin: 0 0 10px 0; font-size: 2em; font-weight: 300; }217 .header-meta { display: flex; flex-wrap: wrap; gap: 15px; margin-top: 15px; font-size: 0.9em; opacity: 0.9; }218 .meta-item { background: rgba(255,255,255,0.2); padding: 5px 12px; border-radius: 20px; }219 .nav-links { padding: 15px 30px; background: #f8f9fa; border-bottom: 1px solid #ecf0f1; }220 .nav-links a { color: #8e44ad; text-decoration: none; margin-right: 20px; font-weight: 500; }221 .nav-links a:hover { text-decoration: underline; }222 .content { padding: 30px; }223 .description { margin-bottom: 30px; }224 .flowchart-container { margin: 30px 0; }225 .flowchart-container h2 { color: #2c3e50; margin-bottom: 15px; }226 .mermaid { background: white; padding: 20px; border-radius: 10px; border: 1px solid #ecf0f1; overflow-x: hidden; overflow-y: auto; min-height: 500px; max-width: 100%; }227 .color-legend { background: #f8f9fa; padding: 20px; border-radius: 10px; margin: 30px 0; }228 .color-legend h3 { color: #2c3e50; margin-bottom: 15px; }229 .color-grid { display: grid; grid-template-columns: repeat(auto-fit, minmax(200px, 1fr)); gap: 15px; }230 .color-item { display: flex; align-items: center; gap: 10px; padding: 10px; background: white; border-radius: 5px; }231 .color-box { width: 30px; height: 30px; border-radius: 4px; border: 1px solid #ddd; }232 .info-section { display: grid; grid-template-columns: repeat(auto-fit, minmax(300px, 1fr)); gap: 20px; margin-top: 30px; }233 .info-card { background: #f8f9fa; padding: 20px; border-radius: 10px; }234 .info-card h3 { color: #2c3e50; margin-bottom: 15px; }235 .info-card ul { list-style: none; padding: 0; }236 .info-card li { padding: 8px 0; border-bottom: 1px solid #ecf0f1; }237 .info-card li:last-child { border-bottom: none; }238 </style>239</head>240<body>241 <div class="container">242 <div class="header">243 <h1>${title}</h1>244 <div class="header-meta">245 <span class="meta-item">Mathematics</span>246 <span class="meta-item">Discrete Mathematics / Logic</span>247 <span class="meta-item">Source: Frege, Łukasiewicz</span>248 </div>249 </div>250 <div class="nav-links">251 <a id="back-link" href="#">← Back to Mathematics Database</a>252 <a id="index-link" href="#">Propositional Logic Index</a>253 <a href="https://en.wikipedia.org/wiki/Propositional_calculus" target="_blank">Propositional Calculus (Wikipedia)</a>254 <a href="https://huggingface.co/spaces/garywelz/programming_framework" target="_blank">Programming Framework</a>255 </div>256 <script>257 (function() {258 const hostname = window.location.hostname;259 const base = hostname.includes('storage.googleapis.com')260 ? 'https://storage.googleapis.com/regal-scholar-453620-r7-podcast-storage/mathematics-processes-database'261 : '../..';262 document.getElementById('back-link').href = base + '/mathematics-database-table.html';263 document.getElementById('index-link').href = base + '/processes/discrete_mathematics/discrete_mathematics-propositional-logic.html';264 })();265 </script>266 <div class="content">267 <div class="description">268 <h2>Description</h2>269 <p>${subtitle}</p>270 <p style="margin-top:10px;"><em>Source: Frege, G. <a href="https://en.wikipedia.org/wiki/Begriffsschrift" target="_blank">Begriffsschrift</a> (1879); Łukasiewicz, J. Elements of Mathematical Logic (1929)</em></p>271 </div>272 <div class="flowchart-container">273 <h2>Dependency Flowchart</h2>274 <p class="flowchart-note" style="font-size:0.9rem;color:#7f8c8d;margin-bottom:12px;"><strong>Note:</strong> Arrows mean "depends on" (tail → head).</p>275 <div class="mermaid">${mermaidEscaped}</div>276 </div>277 <div class="color-legend">278 <h3>Color Scheme</h3>279 <div class="color-grid">280 <div class="color-item"><div class="color-box" style="background:#e74c3c"></div><div><strong>Red</strong><br><small>Axioms</small></div></div>281 <div class="color-item"><div class="color-box" style="background:#3498db"></div><div><strong>Blue</strong><br><small>Definitions</small></div></div>282 <div class="color-item"><div class="color-box" style="background:#1abc9c"></div><div><strong>Teal</strong><br><small>Theorems</small></div></div>283 </div>284 </div>285 <div class="info-section">286 <div class="info-card">287 <h3>Statistics</h3>288 <ul>289 <li><strong>Nodes:</strong> ${nodes}</li>290 <li><strong>Edges:</strong> ${edges}</li>291 </ul>292 </div>293 <div class="info-card">294 <h3>Keywords</h3>295 <ul>296 <li>propositional logic</li><li>Hilbert</li><li>Łukasiewicz</li><li>tautology</li><li>modus ponens</li><li>De Morgan</li>297 </ul>298 </div>299 </div>300 </div>301 </div>302 <script>303 mermaid.initialize({ startOnLoad: true, theme: 'default', flowchart: { useMaxWidth: true, htmlLabels: true, curve: 'step', nodeSpacing: 25, rankSpacing: 90, padding: 20 }, themeVariables: { fontSize: '14px', fontFamily: 'Segoe UI, Arial, sans-serif' } });304 </script>305</body>306</html>`;307}308 309if (fs.existsSync(path.join(MATH_DB, "processes"))) {310 for (const d of subgraphData) {311 const html = htmlTemplate(312 `Propositional Logic — ${d.title}`,313 d.desc + ". Shows how theorems depend on axioms, definitions, and prior theorems.",314 d.mermaid,315 d.nodes,316 d.edges317 );318 const fileName = "discrete_mathematics-propositional-logic-" + d.name;319 fs.writeFileSync(path.join(DISC_DIR, fileName + ".html"), html, "utf8");320 console.log("Wrote", path.join(DISC_DIR, fileName + ".html"));321 }322 // Index page323 const indexHtml = `<!DOCTYPE html>324<html lang="en">325<head>326 <meta charset="UTF-8">327 <meta name="viewport" content="width=device-width, initial-scale=1.0">328 <title>Propositional Logic - Mathematics Process</title>329 <style>330 * { margin: 0; padding: 0; box-sizing: border-box; }331 body { font-family: 'Segoe UI', Tahoma, Geneva, Verdana, sans-serif; background: linear-gradient(135deg, #8e44ad 0%, #3498db 100%); min-height: 100vh; padding: 20px; }332 .container { max-width: 900px; margin: 0 auto; background: white; border-radius: 15px; box-shadow: 0 20px 40px rgba(0,0,0,0.1); overflow: hidden; padding: 30px; }333 h1 { color: #2c3e50; margin-bottom: 15px; }334 p { color: #555; margin-bottom: 25px; line-height: 1.6; }335 .nav-links { margin-bottom: 20px; }336 .nav-links a { color: #8e44ad; text-decoration: none; margin-right: 20px; font-weight: 500; }337 .nav-links a:hover { text-decoration: underline; }338 .sections { display: grid; gap: 15px; }339 .sections a { display: block; padding: 20px; background: #f8f9fa; border-radius: 10px; color: #2c3e50; text-decoration: none; font-weight: 500; border-left: 4px solid #8e44ad; }340 .sections a:hover { background: #ecf0f1; }341 </style>342</head>343<body>344 <div class="container">345 <div class="nav-links">346 <a id="back-link" href="#">← Back to Mathematics Database</a>347 <a href="https://en.wikipedia.org/wiki/Propositional_calculus" target="_blank">Propositional Calculus (Wikipedia)</a>348 </div>349 <script>350 (function() {351 const backLink = document.getElementById('back-link');352 backLink.href = window.location.hostname.includes('storage.googleapis.com')353 ? 'https://storage.googleapis.com/regal-scholar-453620-r7-podcast-storage/mathematics-processes-database/mathematics-database-table.html'354 : '../../mathematics-database-table.html';355 })();356 </script>357 <h1>Propositional Logic</h1>358 <p>Hilbert-style axiomatic development of classical propositional logic. Three axioms (Łukasiewicz P2), modus ponens, definitions of disjunction, conjunction, biconditional, and key theorems. Split into three views.</p>359 <div class="sections">360 <a href="discrete_mathematics-propositional-logic-axioms-implication.html">Chart 1 — Axioms & Implication</a>361 <a href="discrete_mathematics-propositional-logic-definitions-connectives.html">Chart 2 — Definitions & Connectives</a>362 <a href="discrete_mathematics-propositional-logic-tautologies-metalogic.html">Chart 3 — Tautologies & Metalogic</a>363 </div>364 </div>365</body>366</html>`;367 fs.writeFileSync(path.join(DISC_DIR, "discrete_mathematics-propositional-logic.html"), indexHtml, "utf8");368 console.log("Wrote", path.join(DISC_DIR, "discrete_mathematics-propositional-logic.html"));369} else {370 console.log("MATH_DB not found - skipping HTML generation.");371}372 373console.log("Done. Nodes:", discourse.nodes.length, "Edges:", discourse.edges.length);374