nx_classical.nx source

1// nx_classical.nx -- classical-logic axioms. 2// 3// Closes the named blocker for nonconstructive proofs (currently 4// PARTIAL in the audit). Per user 2026-05-15: "no losses". 5// 6// Adds two axioms that are sound in CLASSICAL but not INTUITIONISTIC 7// logic. The kernel core (nx_kernel_v2) stays intuitionistic; 8// classical proofs explicitly cite these axioms so the audit trail 9// always shows whether classical logic was used. 10// 11// LEM: for any A, A | ~A 12// DNE: for any A, ~~A => A 13// 14// LEM and DNE are interderivable in classical logic; we ship both 15// because each saves a step in different proof shapes. HOL Light 16// derives the rest from these (Peirce's law, RAA, etc.) via the 17// engine + the existing v2 rules. 18 19// nx_safety_envelope: 20// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 21// sil_target: SIL1 22// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 23// verdict: NOT_YET_EVALUATED 24 25import "nx_kernel_v2.nx" 26 27// LEM (law of excluded middle). Returns chain idx of the axiom (A | ~A). 28func nx_classical_lem(ch: *K2Chain, a: *Term) -> nx_int { 29 return nx_k2_axiom(ch, nx_k2_or(a, nx_k2_not(a))) 30} 31 32// DNE (double-negation elimination). Returns idx of (~~A => A). 33func nx_classical_dne(ch: *K2Chain, a: *Term) -> nx_int { 34 return nx_k2_axiom(ch, nx_k2_imp(nx_k2_not(nx_k2_not(a)), a)) 35} 36 37// Peirce's law: ((A => B) => A) => A. Derivable from LEM/DNE; we 38// ship it as a one-line axiom emitter so engine paths can use it 39// directly without redoing the derivation each call. 40func nx_classical_peirce(ch: *K2Chain, a: *Term, b: *Term) -> nx_int { 41 let inner: *Term = nx_k2_imp(nx_k2_imp(a, b), a) 42 return nx_k2_axiom(ch, nx_k2_imp(inner, a)) 43} 44 45// Convenience: bulk-register all three for a given pair (A, B). Returns 46// the chain index of the LEM axiom for A; the others are next two. 47func nx_classical_register_basics(ch: *K2Chain, a: *Term, b: *Term) -> nx_int { 48 let lem_idx: nx_int = nx_classical_lem(ch, a) 49 let _dne_idx: nx_int = nx_classical_dne(ch, a) 50 let _pei_idx: nx_int = nx_classical_peirce(ch, a, b) 51 return lem_idx 52}