Impossibility Theorems for Fixed-Axis Classification Systems: With Application to Type Theory

Classification systems (type systems, ontologies, taxonomies, schemas) operate over fixed sets of classification axes. We prove this architectural choice has unavoidable consequences: any fixed-axis system is incomplete for some domain. This is not a limitation of specific implementations; it is an information-theoretic impossibility. The Core Theorems All proofs in Lean 4 (2700+ lines, 142+ theorems, 0 sorry): Fixed Axis Incompleteness: For any axis set A and any axis a ∉ A, there exists a domain D that A cannot serve. The information required to answer D's queries does not exist in A. Parameterized Immunity: For any domain D, there exists an axis set A_D that is complete for D. This set is computable: A_D = ⋃_{q ∈ D} requires(q). The Asymmetry: Fixed systems guarantee failure for some domain. Parameterized systems guarantee success for all domains. One dominates the other absolutely. Uniqueness: For any domain D, all minimal complete axis sets have equal cardinality. "Dimension" is well-defined for classification problems. Minimality ⇒ Orthogonality: Every minimal complete axis set is orthogonal. Orthogonality is not imposed; it is derived from minimality. The Prescriptive Force. These are not design recommendations. They are mathematical necessities: Given any domain D, the required axes are computable, not chosen.Missing axes cause impossibility, not difficulty. No implementation overcomes a missing axis.The choice of axis-parameterization is forced by the requirement of domain-agnosticism.Application to Type Systems. We instantiate the framework to programming language type systems, proving: (B, S) (Bases and Namespace) is the unique minimal complete representation of class semantics(B, S, H) extends this for hierarchical configuration systems (adding a Scope axis)B-inclusive systems strictly dominate B-exclusive systems when B ≠ ∅ (in type system terminology: nominal typing dominates structural typing)Systems using only {S} require Ω(n) error localization; systems using {B, S} achieve O(1)The Broader Claim. The impossibility theorems apply to any classification system with fixed dimensions, not only type systems. Biological taxonomies, library classification schemes, database schemas, knowledge graphs: all are subject to the same constraints. A fixed set of axes guarantees domains that cannot be served. Corollary (Incoherence of Preference). Claiming "classification system design is a matter of preference" while accepting the uniqueness theorem instantiates P ∧ ¬P. Uniqueness entails ¬∃ alternatives; preference presupposes ∃ alternatives. The mathematics admits no choice.