DRAFT — Ontology Diagnostics: Adjunction-Based Gap Detection in Scientific Knowledge Representation

Core Claim

Existing approaches to ontology quality focus on consistency (is it logically sound?) and alignment (do two ontologies match?). Neither addresses COMPLETENESS: is the ontology missing distinctions that it should have?

I present a formal meta-ontology — an ontology about ontology engineering — that formalizes the process of detecting and resolving missing distinctions using categorical adjunctions. The methodology is:

1. Formalize two related domains as categories
2. Build structure-preserving maps (functors) in both directions
3. Construct the adjunction (unit + counit morphisms)
4. Entities where unit != identity = MISSING DISTINCTIONS in the source
5. Resolve via ContextDef (non-destructive) or enrichment (destructive)
6. Verify resolutions against published literature
7. Measure improvement via loss ratio reduction

The meta-ontology itself is formalized as a pr4xis domain with 29 entities¹, 14 methodology steps¹, 13 axioms¹, and 894 machine-verified proofs².

What Exists in Literature vs What Is Novel

Exists:

• Meta-ontology (Van Inwagen 1998): philosophical study of what ontology IS. Asks “what do we mean by existence?” — DIFFERENT from our question.
• Upper ontologies (BFO, DOLCE, SUMO): top-level categories for all domains. Provide classification, not gap detection.
• Ontology alignment (Euzenat & Shvaiko 2013): matching entities across ontologies. Finds CORRESPONDENCES, not MISSING entities.
• Ontology debugging (Schlobach & Cornet 2003): finds logical INCONSISTENCIES. We find INCOMPLETENESS — a different problem.
• Ologs (Spivak & Kent 2012): categorical knowledge representation using functors. Maps between domains. Does NOT use adjunctions for gap detection.
• Category theory (Mac Lane 1971): adjunctions are standard mathematics.

Novel:

• Using adjunction unit/counit to DETECT missing ontological distinctions
• Quantifying inter-scale information loss via gap ratios
• ContextDef as non-destructive gap resolution (preserves functor validity)
• Loss threshold classification (Low/Moderate/High → different resolution types)
• The meta-ontology itself: formalizing the methodology as a praxis domain
• Empirical finding: every adjunction between biological domains at different scales has gaps, and every gap corresponds to a published distinction

The Meta-Ontology

Entities (29)

Methodology Pipeline (14 steps)

FormalizeDomains → ConstructFunctors → VerifyFunctorLaws → ConstructAdjunction
→ ComputeUnit + ComputeCounit → DetectGaps → ClassifyGaps + ComputeLossRatios
→ ProposeResolution → VerifyAgainstLiterature → ImplementResolution
→ RunMachineProofs → AssessImprovement

Key Qualities

IsAutoDetectable: Most gap types (UnitGap, CounitGap, InformationLoss, GranularityMismatch, CanonicalRepresentative) are automatically detectable by adjunction analysis. Only MissingDistinction requires human judgment to NAME the distinction — the adjunction tells you WHERE it is, the human tells you WHAT it is.

PreservesFunctorValidity: ContextResolution adds distinctions WITHOUT changing the category structure — existing functors remain valid. OntologyEnrichment adds new entities which may require updating all functors (breaking change).

SuggestedForLossLevel: Empirical classification from 3 adjunctions:

• <40% loss → GranularityRefinement (minor adjustment)
• 40-80% loss → ContextResolution (add functional modes)

• 80% loss → IntermediateDomain (domains too far apart)

Proven Axioms (13)

Empirical Validation

Computed from the codebase (not estimated)⁴:

The Molecular ⊣ Bioelectric loss of 85% triggered the IntermediateDomain recommendation. The biochemistry domain was already built as this intermediate — connecting molecular→biochemistry→bioelectricity should reduce the direct loss.

The Kv Discovery (Case Study)

The adjunction between molecular biology and bioelectricity detected that the potassium channel Kv COLLAPSES on the round-trip:

Kv → (MolecularToBioelectric) → IonChannelModulation
   → (BioelectricToMolecular) → GlyR

Kv goes in, GlyR comes out. The round-trip changed the identity.

What the adjunction detected: The bioelectric ontology treats MembranePotential (passive signal) and IonChannelModulation (active intervention) as separate concepts. But at the molecular level, BOTH are implemented by the same Kv channel. The molecular ontology was missing a distinction between constitutive and therapeutic functional modes.

How ContextDef resolved it:

(Kv, Constitutive)  → PassiveHomeostatic    — sets resting Vmem
(Kv, Therapeutic)   → TherapeuticTarget     — drug shifts Vmem

Literature verification: Kv as resting Vmem setter = textbook electrophysiology. Kv as drug target = Kofman & Levin 2024. Both roles are established. The adjunction didn’t discover new biology — it discovered a MISSING FORMALIZATION of known biology.

Discussion

Why This Matters

Most ontology engineering relies on human experts to decide which distinctions to include. This is inherently incomplete — experts model what they think is important, not what the STRUCTURE requires. Adjunctions provide an objective, automated criterion: if the round-trip changes an entity’s identity, the ontology is missing something.

Relation to Spivak’s Ologs

Spivak & Kent (2012) introduced ologs as categorical ontologies with functors for cross-domain mapping. Our contribution extends this: Spivak uses functors to CONNECT domains. I use adjunctions (paired functors) to DIAGNOSE domains. The gap detection methodology is a natural extension of the olog framework that Spivak did not explore.

Limitations

• The discrete category structure means functor mapping choices affect which gaps are detected. Different functors might reveal different gaps.
• The loss thresholds (40%/80%) are empirical from 3 adjunctions. More adjunctions needed to validate these thresholds.
• ContextDef resolves gaps but doesn’t reduce loss ratios. The loss reflects genuine abstraction, not an error.

Testable Predictions

1. Adding more adjunctions to the system should always reveal gaps (the methodology should generalize)
2. Intermediate domains should measurably reduce loss ratios
3. The loss thresholds should be stable across different scientific domains

Code & Verification

All source code, tests, and the live computational analysis are at:

https://github.com/i-am-logger/pr4xis

Re-deriving every numerical claim

git clone https://github.com/i-am-logger/pr4xis
cd pr4xis
cargo test --workspace
cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture

The first command runs the full workspace test suite. The second prints the live per-adjunction collapse percentages cited in this paper — including the 85.2% molecular-bioelectric round-trip loss that the meta-ontology classifies as “high loss → IntermediateDomain recommended”.

Key files

• The meta-ontology itself lives at crates/domains/src/formal/meta/ontology_diagnostics/ontology.rs — the pr4xis::ontology! block that encodes the 29 concepts, the 14-step methodology pipeline, and the 13 axioms about ontology engineering. The directory also contains collapse_patterns.rs (the loss-threshold classifications) and a README.md.
• The computational gap analysis is at crates/domains/src/formal/meta/gap_analysis.rs — the live functions (analyze_molecular_bioelectric(), analyze_pharmacology_molecular(), analyze_biology_bioelectric(), test_full_chain_collapse_measurement) that compute the collapse percentages from the actual functor implementations every test run.
• The three adjunctions themselves live at crates/domains/src/natural/biomedical/adjunctions.rs — MolecularBioelectricAdjunction, PharmacologyMolecularAdjunction, BiologyBioelectricAdjunction, each with unit and counit implementations and the test suite that verifies them.
• The Kv gap and its ContextDef resolution live at crates/domains/src/natural/biomedical/molecular/ontology.rs — the MolecularEntity enum, the MolecularFunctionalContext enum, and the ContextDef impl that disambiguates (Kv, Constitutive) from (Kv, Therapeutic).

Test-command index for the load-bearing claims

The “894 machine-verified tests” count in §1 is the meta-ontology subset at the time of drafting. The workspace total is 4,855 tests, re-derivable via cargo test --workspace. Both numbers update automatically with the codebase.

References

• Spivak DI, Kent RE (2012). Ologs: a categorical framework for knowledge representation. PLoS ONE.
• Spivak DI (2014). Category Theory for the Sciences. MIT Press.
• Mac Lane S (1971). Categories for the Working Mathematician. Springer.
• Euzenat J, Shvaiko P (2013). Ontology Matching. Springer.
• Schlobach S, Cornet R (2003). Non-standard reasoning in description logics. IJCAI.
• Van Inwagen P (1998). Meta-ontology. Erkenntnis.
• Rosen R (1991). Life Itself. Columbia University Press.
• Levin M (2014). Molecular bioelectrics in developmental biology. Mol Biol Cell.
• Kofman K, Levin M (2024). Bioelectric pharmacology of cancer.
• Coste B et al (2010). Piezo1 and Piezo2. Science. Nobel 2021.

Verification Footnotes

1. The meta-ontology lives at crates/domains/src/formal/meta/ontology_diagnostics/ontology.rs. The 29 concepts, 14 methodology steps, and 13 axioms are encoded in the pr4xis::ontology! block. Run cargo test -p pr4xis-domains formal::meta::ontology_diagnostics to verify the encoding compiles and the structural axioms hold. ↩ ↩2 ↩3

2. Re-derive by running cargo test --workspace. The “894” count is the meta-ontology subset at drafting time; the workspace total is computed live on every run. ↩

3. The 13 axioms about ontology engineering (including EveryAdjunctionHasGaps, PipelineIsComplete, ContextResolutionPreservesFunctors, etc.) are implemented as Rust Axiom impls in the meta-ontology directory. Each axiom has a corresponding test that verifies it holds against the actual three-adjunction analysis. Run cargo test -p pr4xis-domains formal::meta::ontology_diagnostics::tests. ↩

4. Every collapse percentage in this paper is computed live by cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture. The output prints per-adjunction unit-loss and counit-loss percentages from the actual functor implementations in crates/domains/src/natural/biomedical/adjunctions.rs. Numbers update automatically as the biomedical ontologies evolve. ↩ ↩2 ↩3 ↩4 ↩5 ↩6 ↩7

5. The Kv channel discovery — round-trip collapse and ContextDef resolution — is verified by cargo test -p pr4xis-domains test_kv_gap_is_resolved_by_context. The context resolution lives in crates/domains/src/natural/biomedical/molecular/ontology.rs as MolecularFunctionalContext. ↩