Impossibility Theorems for Fixed-Axis Classification Systems

Stream: Type theory

[Tristan Simas]

Hi everyone. I formalized a proof that the structural vs. nominal typing debate can't be won: any fixed-axis type system necessarily fails for some domain. The core result: for a type system with fixed axes (like structure, inheritance, hierarchy), there exists a domain whose requirements cannot be fully captured. This isn't a limitation of specific languages, it's a mathematical impossibility result.

What's in the zip

Full Lean 4 formalization (compiles with lake build) Instantiations for Python, TypeScript, Java, and Rust The axioms for type system structure are extracted from actual language specifications, not invented

Main theorem: For any fixed-axis type framework, there exists a domain D such that no complete typing is achievable.

Please let me know if this doesn't hold and why. If there is an error this is a great opportunity to learn!
https://zenodo.org/records/18173678