Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Article . 2026
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Article . 2026
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Article . 2026
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Article . 2026
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Article . 2026
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Article . 2026
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Article . 2026
License: CC BY
Data sources: ZENODO
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
versions View all 7 versions
addClaim

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

Authors: Simas, Tristan;

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

Abstract

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.

Related Organizations
Keywords

structural typing, lower bounds, class systems, impossibility theorems, nominal typing, typing disciplines, information theory

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
0
Average
Average
Average
Green
Related to Research communities