Proof that any fixed-axis type system fails for some domain (formalized in Lean)(zenodo.org)
zenodo.org
Proof that any fixed-axis type system fails for some domain (formalized in Lean)
https://zenodo.org/records/18123532
https://zenodo.org/records/18123532
The core result: for a type system with fixed axes (like behavior, structure, 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.