Formal Proof Ontology

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

1. PURPOSE
Represent a formal proof as a finite, checkable derivation of a conclusion from declared assumptions and inference rules in a specified formal system. Distinguish syntactic derivability from semantic entailment.

2. TYPED ENTITIES
FormalSystem := (Language, Axioms, Rules)
Language := (Symbols, FormationRules)
Formula := well-formed expression in Language
Context := finite set or sequence of assumptions
Judgement := Context |- Formula
InferenceRule := (PremiseJudgements, ConclusionJudgement, SideConditions)
ProofStep := (Identifier, Judgement, RuleIdentifier, Dependencies, DischargedAssumptions)
FormalProof := (System, Context, Goal, Steps, RootStep)
ProofCertificate := serialised proof with rule and dependency references
VerificationResult := VALID | INVALID | UNDETERMINED
Countermodel := interpretation satisfying Context but not Goal

3. CORE RELATIONSHIPS
FORMAL_PROOF --USES--> FORMAL_SYSTEM
FORMAL_PROOF --DERIVES--> GOAL
FORMAL_PROOF --DEPENDS_ON--> AXIOM | ASSUMPTION | PROOF_STEP
PROOF_STEP --APPLIES--> INFERENCE_RULE
PROOF_STEP --JUSTIFIED_BY--> PREMISE_STEPS
INFERENCE_RULE --HAS--> SIDE_CONDITIONS
FORMAL_PROOF --VERIFIED_BY--> PROOF_CHECKER
COUNTERMODEL --REFUTES--> SEMANTIC_ENTAILMENT_CLAIM

4. FORMAL SEMANTICS
Gamma |-S phi : phi is derivable from Gamma in formal system S.
Gamma |=S phi : every S-model satisfying Gamma also satisfies phi.
Soundness(S): for all Gamma, phi, Gamma |-S phi implies Gamma |=S phi.
Completeness(S): for all Gamma, phi, Gamma |=S phi implies Gamma |-S phi.
Do not infer soundness or completeness for an arbitrary system without an established proof.

5. PROOF INVARIANTS
I1: Every formula conforms to the language's formation rules.
I2: Every proof step is an axiom instance, a permitted assumption, or the result of a valid inference-rule application.
I3: Each dependency points to an available earlier step or an explicitly permitted proof structure.
I4: Every rule's side conditions are checked, including freshness and variable-capture constraints.
I5: Assumptions are discharged only under rules that permit discharge.
I6: The root step derives the declared goal under exactly the permitted undischarged assumptions.
I7: A checker returns VALID only when all required obligations pass.

6. INFERENCE FLOWS
flow "ValidateFormalProof" v1.0:
  input: FormalProof P
  require: known(P.System) and well_formed(P.Goal)
  for step in dependency_order(P.Steps):
    assert well_formed(step.Judgement)
    assert dependencies_resolved(step)
    assert rule_exists(step.RuleIdentifier, P.System)
    assert rule_matches_premises(step)
    assert side_conditions_hold(step)
    assert assumption_scope_valid(step)
  assert root_judgement(P) == (P.Context |- P.Goal)
  output: VALID if every assertion succeeds else INVALID

flow "ModusPonens" v1.0:
  input: Gamma |- phi, Gamma |- (phi -> psi)
  output: Gamma |- psi
  condition: both premises use the same compatible context and formal system

flow "CountermodelCheck" v1.0:
  input: Gamma, phi, interpretation M
  if M |= Gamma and M !|= phi:
    output: COUNTERMODEL_CONFIRMED
  else:
    output: NOT_A_COUNTERMODEL
  note: failure to find a countermodel does not establish derivability

7. PROOF REPRESENTATION
Example in propositional logic:
  Assumptions: P, P -> Q
  Step 1: P                 [assumption]
  Step 2: P -> Q            [assumption]
  Step 3: Q                 [modus ponens, steps 1 and 2]
  Conclusion: {P, P -> Q} |- Q

8. SEMANTIC DISTINCTIONS
Formal proof != informal mathematical explanation.
Provability != truth in an unspecified interpretation.
Validity of derivation != soundness of the underlying formal system.
Proof certificate != checker acceptance unless the certificate is actually checked.
A proof in classical logic need not be accepted in intuitionistic logic.
Proof by contradiction and constructive proof have system-dependent rules.

9. SEMANTIC_EQUIVALENCE
Equivalent encodings may use different proof-step identifiers, formatting, or alpha-renamed bound variables if capture is avoided and rule semantics are preserved.
Do not equate proofs merely because their conclusions match.
Equivalence level: syntactic | alpha | derivational | semantic; record explicitly.

10. CONFIDENCE AND PROVENANCE
confidence.status: VERIFIED only after a specified checker has successfully checked a certificate.
confidence.status: PROPOSED for unchecked proof sketches.
provenance: record system version, axiom set, rule set, proof author, checker version, checking timestamp, and dependencies.

11. VALIDATION
Reject unknown rules, malformed terms, unbound references, invalid substitution, variable capture, illicit assumption discharge, mismatched conclusions, and circular justifications without an explicit sound cyclic-proof discipline.
Return diagnostics with failing step identifier and unmet obligation.

12. FLOW_HASH
Canonicalise: UTF-8, stable key ordering, explicit system and rule versions, normalised identifiers where semantics permit.
FLOW_HASH := SHA-256(canonical_serialisation(ontology_version, formal_system, proof_certificate, validation_rules))
Note: a hash identifies bytes under a canonicalisation scheme; it does not prove mathematical correctness.

13. UPDATE_MODEL
When axioms, rules, language, checker, or proof steps change:
  invalidate affected validation results;
  recompute dependencies and proof checks;
  regenerate FLOW_HASH;
  retain previous versions and provenance.

14. AI_CONSUMPTION
Expose typed entities, rule schemas, proof DAG, assumption scopes, proof obligations, validation status, checker identity, provenance, and confidence.
AI may suggest proof steps but must not label a proof formally verified without successful checking by the specified formal system's checker.

END FLOW ALGEBRA