nx_axioms.nx source

1// nx_axioms.nx -- foundational axioms as sealed substrate constants. 2// 3// THE BUILD-FROM-ZERO DISCIPLINE: every higher primitive must trace 4// its derivation back to these axioms via lineage_ids. No primitive 5// ships without showing the chain (axiom -> ... -> primitive). 6// 7// This file is the substrate's MATHEMATICAL FLOOR. Nothing lives 8// below it; every theorem above lives by citation through it. 9// 10// Citations: 11// Peano (1889) "Arithmetices principia" 12// Zermelo (1908) "Untersuchungen über die Grundlagen der 13// Mengenlehre" 14// Fraenkel (1922) replacement axiom 15// Skolem (1923) first-order form of ZF 16// Boole (1854) "An Investigation of the Laws of Thought" 17// Aristotle (~350 BC) Organon (laws of thought) 18// Tarski (1936) formal definition of truth 19// Hilbert (1899) geometry axiomatization 20// 21// genealogy_id: peano_1889 + zfc + boole_1854 + aristotle_organon 22// lineage_id: foundational 23 24// ===== Peano arithmetic axioms (PA) ===================================== 25// 26// PA1 0 is a natural number. -- existence of zero 27// PA2 Every natural number has a successor. -- successor function 28// PA3 0 is not the successor of any natural. -- 0 is least element 29// PA4 Distinct naturals have distinct successors. -- injectivity of S 30// PA5 Induction: P(0) ^ (P(n) -> P(S(n))) -> P -- induction schema 31 32const NX_AX_PEANO_PA1_ZERO_EXISTS: i64 = 101 33const NX_AX_PEANO_PA2_SUCCESSOR: i64 = 102 34const NX_AX_PEANO_PA3_ZERO_NOT_SUCC: i64 = 103 35const NX_AX_PEANO_PA4_SUCC_INJECTIVE: i64 = 104 36const NX_AX_PEANO_PA5_INDUCTION: i64 = 105 37 38// ===== ZFC set theory axioms ============================================ 39// 40// Z1 Extensionality sets equal iff same members 41// Z2 Empty set there exists a set with no members 42// Z3 Pairing for any x,y there exists {x,y} 43// Z4 Union for any X there exists union X 44// Z5 Power set for any X there exists P(X) 45// Z6 Infinity there exists an inductive set 46// Z7 Separation (schema) {x in A : phi(x)} exists 47// Z8 Replacement (schema) image of a function exists as set 48// Z9 Foundation every nonempty set has E-minimal element 49// Z10 Choice every family of nonempty sets has a choice fn 50 51const NX_AX_ZFC_EXTENSIONALITY: i64 = 201 52const NX_AX_ZFC_EMPTY_SET: i64 = 202 53const NX_AX_ZFC_PAIRING: i64 = 203 54const NX_AX_ZFC_UNION: i64 = 204 55const NX_AX_ZFC_POWER_SET: i64 = 205 56const NX_AX_ZFC_INFINITY: i64 = 206 57const NX_AX_ZFC_SEPARATION: i64 = 207 58const NX_AX_ZFC_REPLACEMENT: i64 = 208 59const NX_AX_ZFC_FOUNDATION: i64 = 209 60const NX_AX_ZFC_CHOICE: i64 = 210 61 62// ===== Boolean algebra / propositional logic =========================== 63 64const NX_AX_LOGIC_IDENTITY: i64 = 301 // A -> A 65const NX_AX_LOGIC_NONCONTRADICTION: i64 = 302 // ~(A ^ ~A) 66const NX_AX_LOGIC_EXCLUDED_MIDDLE: i64 = 303 // A v ~A 67const NX_AX_LOGIC_DISTRIBUTIVITY: i64 = 304 // A^(BvC) = (A^B)v(A^C) 68const NX_AX_LOGIC_DEMORGAN: i64 = 305 // ~(A^B) = ~A v ~B 69const NX_AX_LOGIC_MODUS_PONENS_RULE: i64 = 306 // A, A->B |- B (rule) 70const NX_AX_LOGIC_UNIVERSAL_INSTANT: i64 = 307 // forall x P(x) |- P(t) 71const NX_AX_LOGIC_EXISTENTIAL_GEN: i64 = 308 // P(t) |- exists x P(x) 72 73// ===== order / equivalence relation axioms ============================= 74 75const NX_AX_REL_REFLEXIVITY: i64 = 401 // a R a 76const NX_AX_REL_SYMMETRY: i64 = 402 // a R b -> b R a 77const NX_AX_REL_TRANSITIVITY: i64 = 403 // a R b ^ b R c -> a R c 78const NX_AX_REL_ANTISYMMETRY: i64 = 404 // a R b ^ b R a -> a = b 79const NX_AX_REL_TOTALITY: i64 = 405 // a R b v b R a 80const NX_AX_REL_TRICHOTOMY: i64 = 406 // exactly one of <, =, > 81 82// ===== algebraic structure axioms ====================================== 83 84const NX_AX_ALG_ASSOCIATIVITY: i64 = 501 // (a*b)*c = a*(b*c) 85const NX_AX_ALG_COMMUTATIVITY: i64 = 502 // a*b = b*a 86const NX_AX_ALG_IDENTITY_ELEMENT: i64 = 503 // exists e: a*e = a 87const NX_AX_ALG_INVERSE_ELEMENT: i64 = 504 // exists a': a*a' = e 88const NX_AX_ALG_DISTRIBUTIVITY: i64 = 505 // a*(b+c) = a*b + a*c 89const NX_AX_ALG_CLOSURE: i64 = 506 // a,b in S -> a*b in S 90 91// ===== order completeness ============================================== 92 93const NX_AX_ORD_LEAST_UPPER_BOUND: i64 = 601 // every bounded set has sup 94const NX_AX_ORD_ARCHIMEDEAN: i64 = 602 // for any x, exists n: n>x 95const NX_AX_ORD_DEDEKIND_COMPLETENESS: i64 = 603 // Dedekind cut existence 96 97// ===== probability axioms (Kolmogorov 1933) ============================ 98// 99// K1 P(E) >= 0 for every event E 100// K2 P(Omega) = 1 (sample space has measure 1) 101// K3 P(union of disjoint events) = sum of P's (sigma-additivity) 102 103const NX_AX_PROB_NONNEGATIVITY: i64 = 701 104const NX_AX_PROB_NORMALIZATION: i64 = 702 105const NX_AX_PROB_COUNTABLE_ADDITIVITY: i64 = 703 106 107// ===== measure theory (extends K1-K3) ================================== 108 109const NX_AX_MEAS_NULL_EMPTY: i64 = 801 // mu(empty) = 0 110const NX_AX_MEAS_MONOTONICITY: i64 = 802 // A subset B -> mu(A) <= mu(B) 111const NX_AX_MEAS_SUBADDITIVITY: i64 = 803 // mu(A u B) <= mu(A)+mu(B) 112 113// ===== Hilbert's geometry axioms (subset) ============================== 114 115const NX_AX_GEO_TWO_POINTS_DETERMINE_LINE: i64 = 901 116const NX_AX_GEO_LINE_EXTENDS: i64 = 902 117const NX_AX_GEO_CIRCLE_FROM_CENTER_RADIUS: i64 = 903 118const NX_AX_GEO_RIGHT_ANGLES_EQUAL: i64 = 904 119const NX_AX_GEO_PARALLEL_POSTULATE: i64 = 905 120 121// ===== category-theoretic foundations ================================== 122 123const NX_AX_CAT_IDENTITY_MORPHISM: i64 = 1001 124const NX_AX_CAT_COMPOSITION: i64 = 1002 125const NX_AX_CAT_COMPOSITION_ASSOC: i64 = 1003 126 127// ===== descriptors ===================================================== 128// 129// Returns the human-readable name for an axiom code; useful when 130// emitting derivation chains to the provenance ledger. 131// 132// Substrate-level sealed-enum decoding (not magic-string lookup). 133// Each axiom has a stable i64 code, name lookup via if-cascade. 134 135func nx_axiom_name(code: i64) -> *u8 { 136 if code == NX_AX_PEANO_PA1_ZERO_EXISTS { return "Peano PA1 zero exists" } 137 if code == NX_AX_PEANO_PA2_SUCCESSOR { return "Peano PA2 successor function" } 138 if code == NX_AX_PEANO_PA3_ZERO_NOT_SUCC { return "Peano PA3 0 is not a successor" } 139 if code == NX_AX_PEANO_PA4_SUCC_INJECTIVE { return "Peano PA4 successor injective" } 140 if code == NX_AX_PEANO_PA5_INDUCTION { return "Peano PA5 induction" } 141 if code == NX_AX_ZFC_EXTENSIONALITY { return "ZFC extensionality" } 142 if code == NX_AX_ZFC_EMPTY_SET { return "ZFC empty set" } 143 if code == NX_AX_ZFC_PAIRING { return "ZFC pairing" } 144 if code == NX_AX_ZFC_UNION { return "ZFC union" } 145 if code == NX_AX_ZFC_POWER_SET { return "ZFC power set" } 146 if code == NX_AX_ZFC_INFINITY { return "ZFC infinity" } 147 if code == NX_AX_ZFC_SEPARATION { return "ZFC separation schema" } 148 if code == NX_AX_ZFC_REPLACEMENT { return "ZFC replacement schema" } 149 if code == NX_AX_ZFC_FOUNDATION { return "ZFC foundation / regularity" } 150 if code == NX_AX_ZFC_CHOICE { return "ZFC axiom of choice" } 151 if code == NX_AX_LOGIC_IDENTITY { return "Logic identity A -> A" } 152 if code == NX_AX_LOGIC_NONCONTRADICTION { return "Logic noncontradiction" } 153 if code == NX_AX_LOGIC_EXCLUDED_MIDDLE { return "Logic excluded middle" } 154 if code == NX_AX_LOGIC_MODUS_PONENS_RULE { return "Logic modus ponens" } 155 if code == NX_AX_REL_REFLEXIVITY { return "Relation reflexivity" } 156 if code == NX_AX_REL_SYMMETRY { return "Relation symmetry" } 157 if code == NX_AX_REL_TRANSITIVITY { return "Relation transitivity" } 158 if code == NX_AX_REL_ANTISYMMETRY { return "Relation antisymmetry" } 159 if code == NX_AX_ALG_ASSOCIATIVITY { return "Algebra associativity" } 160 if code == NX_AX_ALG_COMMUTATIVITY { return "Algebra commutativity" } 161 if code == NX_AX_ALG_IDENTITY_ELEMENT { return "Algebra identity element" } 162 if code == NX_AX_ALG_INVERSE_ELEMENT { return "Algebra inverse element" } 163 if code == NX_AX_ALG_DISTRIBUTIVITY { return "Algebra distributivity" } 164 if code == NX_AX_ALG_CLOSURE { return "Algebra closure" } 165 if code == NX_AX_ORD_LEAST_UPPER_BOUND { return "Order least upper bound" } 166 if code == NX_AX_ORD_ARCHIMEDEAN { return "Order Archimedean property" } 167 if code == NX_AX_PROB_NONNEGATIVITY { return "Kolmogorov K1 P >= 0" } 168 if code == NX_AX_PROB_NORMALIZATION { return "Kolmogorov K2 P(Omega) = 1" } 169 if code == NX_AX_PROB_COUNTABLE_ADDITIVITY { return "Kolmogorov K3 sigma-additivity" } 170 if code == NX_AX_GEO_PARALLEL_POSTULATE { return "Hilbert parallel postulate" } 171 if code == NX_AX_CAT_IDENTITY_MORPHISM { return "Category identity morphism" } 172 if code == NX_AX_CAT_COMPOSITION { return "Category composition" } 173 return "unknown axiom" 174} 175 176// Returns 1 if code is a recognized axiom; 0 otherwise. Substrate 177// uses this when verifying derivation chains -- every leaf must be 178// a recognized axiom. 179 180func nx_axiom_is_valid(code: i64) -> i64 { 181 if code >= 101 { if code <= 110 { return 1 } } // Peano 182 if code >= 201 { if code <= 210 { return 1 } } // ZFC 183 if code >= 301 { if code <= 310 { return 1 } } // Logic 184 if code >= 401 { if code <= 410 { return 1 } } // Relations 185 if code >= 501 { if code <= 510 { return 1 } } // Algebra 186 if code >= 601 { if code <= 610 { return 1 } } // Order 187 if code >= 701 { if code <= 710 { return 1 } } // Probability 188 if code >= 801 { if code <= 810 { return 1 } } // Measure 189 if code >= 901 { if code <= 910 { return 1 } } // Geometry 190 if code >= 1001 { if code <= 1010 { return 1 } } // Category 191 return 0 192}