Constructive Proof Ontology

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

1. PURPOSE
Represent constructive proofs as typed, auditable derivations that provide witnesses for existential claims and effective constructions for disjunctions, without assuming unrestricted classical principles.

2. TYPES
  Proposition, Context, Assumption, ProofTerm, ProofStep, InferenceRule,
  Witness, Type, Algorithm, Construction, Dependency, VerificationResult.

3. CORE ENTITIES
  ConstructiveProof(id, proposition, context, proof_term, logic, status)
  ExistentialClaim(variable, domain, predicate)
  Witness(value, domain, evidence)
  DisjunctionProof(branch, branch_proof)
  ImplicationProof(assumption, derivation)
  UniversalProof(variable, arbitrary_element_proof)
  EqualityProof(lhs, rhs, justification)

4. RELATIONSHIPS
  proves(ProofTerm, Proposition)
  depends_on(ProofStep, Assumption | ProofStep)
  constructs(ProofTerm, Witness)
  inhabits(ProofTerm, Type)
  discharges(ProofStep, Assumption)
  verifies(VerificationResult, ProofTerm)
  instantiates(ProofTerm, UniversalClaim)

5. FORMAL SEMANTICS (INTUITIONISTIC)
  Gamma |- t : A         proof term t establishes proposition A in context Gamma
  Gamma |- a : A; Gamma |- b : B
  -------------------------------- AND-INTRO
  Gamma |- (a,b) : A /\ B

  Gamma |- a : A
  -------------------------- OR-LEFT
  Gamma |- inl(a) : A \/ B

  Gamma |- b : B
  -------------------------- OR-RIGHT
  Gamma |- inr(b) : A \/ B

  Gamma, x:A |- t:B
  -------------------------- IMPLIES-INTRO
  Gamma |- lambda x.t : A -> B

  Gamma |- f:A -> B; Gamma |- a:A
  -------------------------------- IMPLIES-ELIM
  Gamma |- f(a):B

  Gamma |- w:D; Gamma |- p:P(w)
  -------------------------------- EXISTS-INTRO
  Gamma |- (w,p): exists x:D. P(x)

  Gamma, x:D |- t:P(x)
  -------------------------------- FORALL-INTRO (x not free in undischarged assumptions)
  Gamma |- lambda x.t : forall x:D. P(x)

6. EXECUTABLE FLOW
  flow ConstructiveProofValidation v1.0:
    input: proposition:A, context:Gamma, proof_term:t, logic:INTUITIONISTIC
    require well_formed(A) and well_formed(Gamma)
    typecheck t against A under Gamma
    check each rule application and discharged assumption
    if A is existential: extract witness w and proof of predicate(w)
    if A is disjunction: extract chosen branch and branch proof
    verify dependencies are available and no unapproved axioms are introduced
    output: VerificationResult(validity, witness?, dependencies, diagnostics)

7. INFERENCE FLOWS
  [CONSTRUCTIVE_EXISTENCE]
    GIVEN Gamma |- (w,p) : exists x:D.P(x)
    INFER witness(w), Gamma |- p:P(w)

  [CONSTRUCTIVE_DISJUNCTION]
    GIVEN Gamma |- inl(a):A \/ B
    INFER Gamma |- a:A

  [PROOF_COMPOSITION]
    GIVEN Gamma |- f:A -> B AND Gamma |- a:A
    INFER Gamma |- f(a):B

  [UNIVERSAL_INSTANTIATION]
    GIVEN Gamma |- u:forall x:D.P(x) AND Gamma |- d:D
    INFER Gamma |- u(d):P(d)

8. SEMANTIC DISTINCTIONS
  constructive_proof != classical_proof: classical excluded middle is not assumed by default.
  proof_of_not_not_A != proof_of_A in general intuitionistic logic.
  constructive_existence != merely showing nonexistence leads to contradiction.
  mathematical_induction can be constructive when the induction principle is admitted.
  constructive_proof != executable_program in all interpretations; extraction depends on formalisation.

9. VALIDATION
  V1: every referenced proof step exists and is well typed.
  V2: all proof obligations are discharged.
  V3: existential introduction includes a valid witness and predicate proof.
  V4: disjunction introduction identifies a supported branch.
  V5: no implicit use of excluded middle or double-negation elimination.
  V6: dependencies and chosen axioms are declared.
  V7: verified status requires an actual checker result, not a confidence score.

10. CONFIDENCE
  confidence is metadata for provenance or automated extraction, not a substitute for proof validity.
  verified_proof := checker_accepts(proof_term, proposition, context, axioms).

11. SEMANTIC_EQUIVALENCE
  'constructive demonstration' ~ 'constructive proof' when witness/proof obligations match.
  'proof by construction' is related but may be narrower than constructive logic.
  Preserve differences between constructive and classical entailment.

12. FLOW_HASH
  Canonicalise UTF-8 source: normalise line endings, serialise typed entities and ordered proof dependencies, exclude the FLOW_HASH field itself; calculate SHA-256 of canonical bytes. A digest is not asserted here because no canonical source payload was supplied.

13. UPDATE_MODEL
  On changes to assumptions, inference rules, proposition, proof term, or dependencies:
    invalidate prior verification; re-typecheck; regenerate provenance and hash.

14. AI_CONSUMPTION
  Provide machine-readable typed graph, proof obligations, assumptions, rule trace, witness extraction, validation status, provenance, and explicit logic profile.
  Never label a generated derivation as formally verified without checker execution.

END FLOW ALGEBRA