Conjecture Ontology

FLOW ALGEBRA
CONJECTURE ONTOLOGY
Kireth Semantic Library — Mathematical Entities / Proof Entities
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/proof-entities/conjecture-ontology.html
Version: 1.0 | Locale: en-GB | Date: 2026-10-14
Authors: Mark Higgins — Sky (Recursive AI)
Status: Proposed formalisation; source-page text not independently verified.

1. ONTOLOGY IDENTITY
ontology_id: kireth:proof-entities:conjecture
entity_type: MathematicalConjecture
parent_types: MathematicalStatement, ProofEntity
related_types: Theorem, Lemma, Counterexample, Proof, Hypothesis, OpenProblem
purpose: Represent a precisely stated mathematical claim whose proof or disproof has not yet been established in the specified knowledge context.

2. TYPED ENTITIES
Conjecture {id:IRI, statement:Formula, language:FormalLanguage?, assumptions:Set[Formula], domain:Domain, status:Status, provenance:Source, created_at:DateTime?, updated_at:DateTime?}
Status := OPEN | PROVED | DISPROVED | INDEPENDENT_RELATIVE_TO_SYSTEM | WITHDRAWN | UNKNOWN
Proof {id:IRI, conclusion:Formula, premises:Set[Formula], system:FormalSystem, verified:Boolean}
Counterexample {id:IRI, witness:Entity, target:Conjecture, verified:Boolean}
FormalSystem {id:IRI, axioms:Set[Formula], inference_rules:Set[Rule]}
Evidence {id:IRI, conjecture:IRI, kind:COMPUTATIONAL|HEURISTIC|PARTIAL_PROOF|PROOF|COUNTEREXAMPLE, scope:Description, verified:Boolean}

3. RELATIONSHIP ALGEBRA
Conjecture --asserts--> Formula
Conjecture --assumes--> Formula
Conjecture --concerns--> Domain
Conjecture --supported_by--> Evidence
Conjecture --challenged_by--> Evidence
Conjecture --proved_by--> Proof
Conjecture --disproved_by--> Counterexample
Conjecture --generalises--> Statement
Conjecture --specialises--> Statement
Conjecture --depends_on--> Statement
Conjecture --has_status--> Status
Proof --uses_axioms_of--> FormalSystem

4. FORMAL SEMANTICS
Let T be a formal theory and phi a well-formed closed formula.
Conjecture(T, phi) := proposed(phi) AND status(phi,T)=OPEN.
Proved(T,phi) iff T |- phi with an accepted, verified derivation.
Disproved(T,phi) iff T |- NOT(phi), or a sound counterexample refutes a universally quantified claim under its stated assumptions.
Independent(T,phi) iff T does not prove phi and T does not prove NOT(phi), subject to an established metatheoretic proof and the stated assumptions about T.
Semantic entailment T |= phi and syntactic provability T |- phi are distinct relations; equivalence requires appropriate soundness/completeness assumptions.
Absence of a known proof is not proof of independence.
Finite computational verification does not establish an unrestricted universal claim.

5. EXECUTABLE INFERENCE FLOWS (PSEUDOCODE)
flow RegisterConjecture(statement, assumptions, domain, source):
  REQUIRE well_formed(statement)
  REQUIRE assumptions_are_explicit(assumptions)
  STORE statement, assumptions, domain, source
  SET status = OPEN unless independently verified evidence justifies another status
  EMIT Conjecture

flow VerifyProof(conjecture, candidate_proof, system):
  REQUIRE proof_conclusion(candidate_proof) == conjecture.statement
  REQUIRE proof_assumptions(candidate_proof) compatible_with conjecture.assumptions
  IF mechanically_or_independently_verified(candidate_proof, system):
    SET conjecture.status = PROVED
    LINK conjecture --proved_by--> candidate_proof
  ELSE: RETAIN status and RECORD unverified_candidate

flow VerifyCounterexample(conjecture, candidate):
  REQUIRE conjecture.statement has a refutable universal or otherwise witness-refutable form
  REQUIRE candidate satisfies all domain restrictions and assumptions
  IF evaluate_statement(candidate) == FALSE AND independently_verified(candidate):
    SET conjecture.status = DISPROVED
    LINK conjecture --disproved_by--> candidate
  ELSE: RETAIN status

flow EvidenceUpdate(conjecture, evidence):
  RECORD evidence.kind, evidence.scope, evidence.provenance
  IF evidence.kind == COMPUTATIONAL: DO NOT infer PROVED from bounded tests alone
  IF evidence.kind == PARTIAL_PROOF: DO NOT infer full theorem

6. VALIDATION RULES
V01: Every conjecture has a unique stable identifier and well-formed statement.
V02: Quantifier scope, assumptions and mathematical domain are explicit.
V03: PROVED requires an accepted verified proof relative to the stated system.
V04: DISPROVED requires a sound refutation under the same assumptions.
V05: INDEPENDENT_RELATIVE_TO_SYSTEM names the formal system and independence evidence.
V06: Contradictory status assertions are flagged for review, not silently merged.
V07: Evidence records distinguish empirical support, computation and deduction.
V08: Provenance, version and revision history are retained.

7. SEMANTIC EQUIVALENCE AND DISTINCTIONS
Conjecture != Theorem: a theorem has an accepted proof in the relevant context.
Conjecture != Axiom: an axiom is assumed within a theory rather than posed for proof.
Conjecture != Hypothesis: hypothesis is broader and may be empirical; a mathematical conjecture asserts a mathematical proposition.
Conjecture != OpenProblem: an open problem may request a construction, classification or computation rather than assert one proposition.
Equivalent conjectures require proof of logical equivalence under aligned assumptions; textual similarity is insufficient.

8. CONFIDENCE AND PROVENANCE
CONFIDENCE := {level: LOW|MEDIUM|HIGH, basis: FORMAL_PROOF|EXPERT_REVIEW|COMPUTATIONAL_TEST|HEURISTIC, scope: Description}
Confidence expresses strength of available evidence, never substitutes for a proof.
PROVENANCE := {source_url, author, date, verification_method, revision}

9. FLOW HASH AND UPDATE MODEL
FLOW_HASH := SHA256(canonical_utf8(ontology_id, version, typed_entities, relations, inference_flows, validation_rules))
Note: FLOW_HASH is a generation specification, not a precomputed digest.
UPDATE_MODEL := append-only evidence history; version each change to statement, assumptions, proof status or semantics; invalidate dependent inferences when assumptions change.

10. AI CONSUMPTION
AI_CONSUMPTION := {
  ingest: typed_ontology,
  reason: provenance_aware_formal_inference,
  verify: proof_or_counterexample_validation,
  output: status_with_assumptions_and_evidence,
  safeguards: [never_present_open_conjecture_as_theorem, distinguish_experiment_from_proof, report_uncertainty, preserve_provenance]
}

11. EXAMPLE
Conjecture C: For every integer n >= 1, P(n) holds.
Tests P(1), ..., P(1000) all true -> evidence of bounded verification; C remains OPEN.
A verified inductive proof with a valid base case and induction step -> C becomes PROVED.
A verified integer k >= 1 with NOT P(k) -> C becomes DISPROVED.

END FLOW ALGEBRA