Mathematical System Ontology

FLOW ALGEBRA
MATHEMATICAL SYSTEM ONTOLOGY
Kireth Semantic Library | Entity Graph | Mathematical Entities | Foundations
Version: 1.0 | Date: 2026-10-12
Authors: Mark Higgins — Sky (Recursive AI)
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/foundations-of-mathematical-entities/mathematical-system-ontology.html
Scope: Subject-based formalisation; source-page content not independently verified.

01. PURPOSE
flow MathematicalSystemOntology v1.0:
  intent: represent, validate, compare and reason over formal mathematical systems
  domain: mathematical_entities/foundations/mathematical_system
  semantics: typed, provenance-aware, revisioned

02. TYPE SIGNATURES
type Identifier = String
type Proposition = Formula
type TruthStatus = {proved, disproved, independent, unknown}
type SystemKind = {axiomatic, algebraic, logical, geometric, dynamical, probabilistic, computational, hybrid}
type System = {id: Identifier, kind: SystemKind, language: Language, signature: Signature, axioms: Set[Proposition], rules: Set[Rule], models: Set[ModelRef], version: String}
type Signature = {sorts: Set[Sort], constants: Set[Symbol], functions: Set[FunctionSymbol], predicates: Set[PredicateSymbol]}
type Rule = {premises: List[Proposition], conclusion: Proposition, side_conditions: List[Constraint]}
type Derivation = {system_id: Identifier, premises: Set[Proposition], conclusion: Proposition, steps: List[ProofStep]}
type Interpretation = {symbol_map: Map[Symbol, Denotation], domain: Set[Object]}
type ModelRef = {id: Identifier, interpretation: Interpretation, satisfies_axioms: Bool}
type Claim = {formula: Proposition, status: TruthStatus, evidence: List[Evidence], confidence: Float}

03. CORE ENTITIES
entity MathematicalSystem : System
entity FormalLanguage : Language
entity Vocabulary : Signature
entity Axiom : Proposition
entity Theorem : Proposition
entity Conjecture : Proposition
entity InferenceRule : Rule
entity FormalProof : Derivation
entity MathematicalModel : ModelRef
entity Interpretation : Interpretation
entity Constraint : Formula
entity ConsistencyResult : Claim
entity CompletenessResult : Claim
entity DecidabilityResult : Claim

04. CLASSIFICATION
classify(system):
  by_foundation: axiomatic | constructive | model_theoretic | computational
  by_logic: classical | intuitionistic | modal | many_valued | other
  by_structure: algebraic | order_theoretic | topological | geometric | analytic
  by_evolution: static | discrete_time | continuous_time | stochastic
  note: classifications overlap; they are not mutually exclusive

05. STRUCTURAL RELATIONSHIPS
relation HAS_LANGUAGE(System, Language)
relation HAS_SIGNATURE(System, Signature)
relation HAS_AXIOM(System, Proposition)
relation HAS_RULE(System, Rule)
relation HAS_MODEL(System, ModelRef)
relation DERIVES(Derivation, Proposition)
relation SATISFIES(ModelRef, Proposition)
relation INTERPRETS(Interpretation, Symbol)
relation EXTENDS(System, System)
relation RESTRICTS(System, System)
relation IS_EQUIVALENT_TO(System, System, EquivalenceCriterion)
relation IS_INTERPRETABLE_IN(System, System, Interpretation)
relation DEPENDS_ON(Proposition, Proposition)
relation CONTRADICTS(Proposition, Proposition)

06. WELL-FORMEDNESS
validate_system(S):
  require unique(S.id)
  require symbols_in(S.axioms) subset_of symbols(S.signature)
  require well_formed(S.axioms, S.language)
  require all(rule_is_well_typed(r, S.signature) for r in S.rules)
  return ValidationReport

07. AXIOMATIC SEMANTICS
axioms(S) := S.axioms
models(S) := {M | for_all a in axioms(S): M |= a}
consistent_semantically(S) := exists M: M in models(S)
consistent_syntactically(S) := not (S |- bottom)
  note: correspondence requires assumptions on the logic and proof calculus

08. DEDUCTIVE CLOSURE
Cn(S, Gamma) := {phi | Gamma union axioms(S) |- phi}
prove(S, Gamma, phi):
  check well_formed(phi)
  search derivation under S.rules
  if derivation verified: return proved with proof
  else: return unknown  # failed search is not disproof

09. SOUNDNESS AND COMPLETENESS
sound(S, calculus) := for_all phi: (S |- phi) implies (S |= phi)
complete(S, calculus) := for_all phi: (S |= phi) implies (S |- phi)
  note: properties depend on language, semantics and calculus
  note: do not infer completeness from consistency

10. MODEL VALIDATION
validate_model(M, S):
  require interpretation_respects_signature(M, S.signature)
  for each a in S.axioms: check M |= a
  return {valid: all_checks_pass, counterexamples: failed_checks}

11. SYSTEM EXTENSION
extend(S, new_axioms, new_symbols):
  S2.signature := compatible_extension(S.signature, new_symbols)
  S2.axioms := S.axioms union new_axioms
  recheck well_formedness and model existence
  do_not_assume_consistency_preservation
  return versioned(S2)

12. SYSTEM COMPARISON
compare(S1, S2):
  inspect signatures, axiom sets, rule systems and model classes
  distinguish syntactic identity from definitional equivalence
  distinguish interpretation from categorical equivalence
  output justified mappings and unresolved obligations

13. INFERENCE RULES
rule R1: HAS_AXIOM(S, p) and valid_axiom(p) => DERIVABLE(S, p)
rule R2: DERIVABLE(S, p) and DERIVABLE(S, implies(p,q)) => DERIVABLE(S, q)
rule R3: HAS_MODEL(S, M) and SATISFIES(M, p) => TRUE_IN_MODEL(p, M)
rule R4: VERIFIED_PROOF(S, p, proof) => THEOREM_OF(p, S)
rule R5: VERIFIED_COUNTERMODEL(S, p, M) => NOT_ENTAILED_BY(p, S)
  guard R5: M satisfies all axioms(S) and M does not satisfy p
rule R6: EXTENDS(S2, S1) and DERIVABLE(S1, p) => DERIVABLE(S2, p)
  guard R6: compatible language embedding and preserved inference rules

14. CONSTRAINTS
constraint no_untyped_symbols
constraint no_unverified_proof_label
constraint no_conflation_of_satisfiability_and_provability
constraint no_unjustified_equivalence
constraint no_claim_of_decidability_without_proof
constraint model_claims_require_interpretation

15. CONFIDENCE
CONFIDENCE(claim):
  if formally_checked_proof: 1.0 relative_to_assumed_axioms_and_checker
  if formally_checked_countermodel: 1.0 for non_entailment relative_to semantics
  else: calibrated_estimate(evidence_quality, method, uncertainty)
  never substitute probabilistic confidence for a proof

16. SEMANTIC_EQUIVALENCE
SEMANTIC_EQUIVALENCE(S1, S2, criterion):
  criterion in {definitional, deductive, model_theoretic, categorical}
  require explicit mappings and verified preservation conditions
  return {status: verified|rejected|unknown, witness, criterion}

17. PROVENANCE
record source_url, extraction_status, author, timestamp, revision
record theorem dependencies, proof checker version, axiom revisions
record interpretation assumptions and countermodel witnesses

18. FLOW_HASH
FLOW_HASH(S):
  payload := canonical_serialise(S.signature, S.axioms, S.rules, S.version)
  return SHA256(payload)
  note: canonical ordering and symbol normalisation required for stable hashes

19. UPDATE_MODEL
UPDATE_MODEL(S, change):
  validate(change)
  S2 := apply_change_as_new_version(S, change)
  invalidate affected proof and model caches
  rerun dependent verification
  log change, previous_hash, new_hash, provenance
  return S2

20. AI_CONSUMPTION
AI_CONSUMPTION:
  expose machine-readable entities, typed relations and proof obligations
  distinguish theorem, conjecture, assumption and model-specific fact
  require provenance for externally asserted claims
  prefer verified proofs over natural-language plausibility
  mark undecidable, untested and unresolved questions as unknown

21. EXECUTION PIPELINE
pipeline:
  input -> parse -> type_check -> normalise -> validate_axioms
  -> build_entity_graph -> evaluate_models -> attempt_proofs
  -> verify_evidence -> attach_confidence -> canonical_hash
  -> publish_versioned_representation

22. EXAMPLE
system GroupTheory:
  signature: sort G; operation mul(G,G)->G; constant e:G; operation inv(G)->G
  axioms:
    - forall x,y,z:G. mul(mul(x,y),z)=mul(x,mul(y,z))
    - forall x:G. mul(e,x)=x and mul(x,e)=x
    - forall x:G. mul(inv(x),x)=e and mul(x,inv(x))=e
  theorem_candidate: forall x:G. inv(inv(x))=x
  status: theorem only after a checked derivation

23. QUALITY ASSURANCE
checks:
  parseable_schema: required
  well_formed_formulas: required
  proof_verification: required_for_theorem_labels
  countermodel_verification: required_for_non_entailment_labels
  explicit_assumptions: required
  provenance_complete: required
  semantic_equivalence_claims: independently_checked

24. TERMINATION
output: versioned MathematicalSystem ontology graph
status: ready_for_validation
END FLOW ALGEBRA