nx_kernel_v2.nx

nx_kernel_v2.nx -- SEMANTIC proof kernel. Real verification, not structural box-checking. Per user 2026-05-15: "nishi lang must generate superior to all other systems proofs not just two level i tlooks good bullshit". HOL Light's kernel is ~500 lines OCaml that implements ~10 primitive inference rules with formal correctness arguments. Every rule does SEMANTIC verification: modus ponens checks that the conclusion is the consequent of the implication premise. Coq, Lean, Isabelle all follow the same LCF discipline. nx_derive (v1) only checks STRUCTURE (rule arity, premise ordering, axiom code validity). Statements were opaque i64 IDs. That was "two-level it looks good bullshit" -- structurally a derivation chain, but the kernel never verifies the statements actually fit the rules' semantics. THIS KERNEL IS DIFFERENT: - Statements are first-class *Term values (real logical formulas) - Each inference rule does SEMANTIC verification of its premises against its claimed conclusion - Built on existing nx_unify Term + nx_subst infrastructure Semantic rules implemented (this commit): AXIOM leaf, must cite a registered axiom Term ASSUMPTION leaf, marks discharged assumptions MODUS_PONENS premise (A => B), premise A; conclusion = B -- kernel CHECKS: premise1 is App(=>, A, B); A == premise2 AND_INTRO premise A, premise B; conclusion = And(A, B) -- kernel CHECKS: conclusion is App(&, premise1, premise2) AND_ELIM_L premise And(A, B); conclusion = A AND_ELIM_R premise And(A, B); conclusion = B IMP_INTRO premise B (under assumption A); conclusion = A => B -- kernel CHECKS: conclusion is App(=>, A, B) SUBST premise (a == b), premise P[a]; conclusion = P[b] -- kernel CHECKS: conclusion = P with a replaced by b REFL no premise; conclusion = (a == a) CONTRADICTION premise A, premise (~A); conclusion = false