Beyond the Deductive Closure: Three Operations of Discovery and a Second-Generation Architecture for Axiom Engines

The Axiom Engine systematically explores the deductive closure of a fixed set of formal axioms, using a large language model as derivation generator and plausibility filter, with formal verification by an SMT solver. This paper, derived from that work (doi.org/10.5281/zenodo.19818672), examines a structural limit of the method and proposes a way past it. Deduction is non-ampliative: any consequence of a set of axioms was already contained in the closure of those axioms, which—though typically infinite—is fixed the instant the axioms are fixed. Genuinely new knowledge characteristically lives outside any single closure. We adopt a single organizing thesis—that discovery is the controlled expansion of a system's representation space—and distinguish three operations as its three axes: (I) deductive expansion within a system; (II) structural correlation, in which a posited and verified morphism transports content across a bridge between systems or between representations of one system; and (III) vocabulary extension, in which a new primitive is defined to solve a problem the existing vocabulary cannot express. We develop worked examples for each (analytic geometry, the Langlands program, and the Fourier transform; elliptic functions, the Lambert W function, and the Tsallis q-logarithm), distinguish two regimes of functional forcing, and show that Landauer's principle is best read as a concealed bridge between thermodynamics and information theory rather than an intra-system derivation. We isolate the common structure of Operations II and III—an act of positing, guarded by verification, since for every true posit there are infinitely many consistent but empty ones—and sketch a second-generation engine (with candidate-morphism representation, pseudocode, an honest treatment of decidability, a worked example, and a candidate bridge-quality metric based on description-length compression). We reframe the original "incompleteness detection" claim as anomaly detection relative to background knowledge, and isolate the single empirical question on which the whole program stands or falls. This is a conceptual / position paper, not an empirical result. Critique is explicitly invited.