Proof Ontology

FLOW ALGEBRA
TITLE: Proof Ontology
VERSION: 1.0
DOMAIN: Mathematical Entities / Proof Entities
SOURCE: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/proof-entities/proof-ontology-2.html
AUTHORS: Mark Higgins — Sky (Recursive AI)
STATUS: Proposed formalisation; source page text not independently verified.

1. PURPOSE
Represent mathematical proofs as typed, inspectable derivations in a specified formal system. Distinguish syntactic derivability from semantic entailment and mathematical truth.

2. ENTITY TYPES
Proof: finite derivation with a conclusion and a declared proof calculus.
FormalSystem: language, axioms, and permitted inference rules.
Formula: well-formed expression of a formal language.
Axiom: formula admitted without derivation in the system.
Premise: formula assumed for a derivation or subproof.
InferenceRule: rule mapping zero or more premise formulae to a conclusion formula.
ProofStep: indexed formula with rule, dependencies, and scope.
Theorem: formula derived with no undischarged assumptions beyond system axioms.
Lemma: proved auxiliary result.
Assumption: temporary formula that may be discharged.
ProofCertificate: machine-checkable representation of derivation steps.
Countermodel: interpretation satisfying premises but falsifying a purported consequence.

3. TYPED RELATIONSHIPS
Proof --IN_SYSTEM--> FormalSystem
Proof --HAS_STEP--> ProofStep
Proof --DERIVES--> Formula
ProofStep --ASSERTS--> Formula
ProofStep --USES_RULE--> InferenceRule
ProofStep --DEPENDS_ON--> ProofStep
ProofStep --USES_PREMISE--> Premise
ProofStep --DISCHARGES--> Assumption
Lemma --SUPPORTS--> ProofStep
Countermodel --REFUTES_ENTAILMENT--> Argument

4. FORMAL SEMANTICS
Let S=(L,A,R) where L is a formal language, A is an axiom set and R is a set of inference rules.
Gamma |-S phi means there exists a finite S-derivation of phi from assumptions Gamma.
Gamma |= phi means every interpretation satisfying all members of Gamma also satisfies phi.
Soundness: if Gamma |-S phi then Gamma |= phi, provided S is sound for the chosen semantics.
Completeness: if Gamma |= phi then Gamma |-S phi, only when established for the chosen system and semantics.
Consistency: not both Gamma |-S phi and Gamma |-S not(phi), for any phi in classical logic.
A proof is valid relative to its declared calculus and correct rule applications; a valid derivation from false premises does not make the premises true.

5. CORE INFERENCE RULES (CLASSICAL NATURAL DEDUCTION)
AND_INTRO: from P and Q infer P AND Q.
AND_ELIM_LEFT: from P AND Q infer P.
AND_ELIM_RIGHT: from P AND Q infer Q.
IMPLIES_ELIM (MODUS_PONENS): from P and P -> Q infer Q.
IMPLIES_INTRO: from a subproof assuming P and deriving Q infer P -> Q, discharging P.
OR_INTRO_LEFT: from P infer P OR Q.
OR_INTRO_RIGHT: from Q infer P OR Q.
FORALL_ELIM: from forall x P(x) infer P(t), where t is free for x in P.
FORALL_INTRO: from P(a) infer forall x P(x) only when a is arbitrary and absent from undischarged assumptions on which P(a) depends.
EXISTS_INTRO: from P(t) infer exists x P(x), where substitution is capture-avoiding.
EXISTS_ELIM: from exists x P(x) and a derivation of Q under fresh witness P(a), infer Q when a occurs neither in Q nor in relevant undischarged assumptions.
Rules and side conditions must be interpreted in the selected formal system.

6. PROOF CONSTRUCTION FLOW
flow ProofVerification v1.0:
  input: FormalSystem S, assumptions Gamma, target phi, ordered steps D
  require: parseable formulas and uniquely indexed steps
  for each step s in D:
    verify s.formula is well formed in S.language
    verify s.rule belongs to S.rules or is an explicitly allowed axiom/premise
    verify all dependencies precede s and are accessible in s.scope
    verify rule conclusion follows from dependency formulas
    verify variable substitution, freshness and assumption discharge conditions
    reject on any failure, returning step index and reason
  require: final step formula equals phi (up to explicitly authorised alpha-equivalence)
  require: undischarged assumptions subset of Gamma
  output: VERIFIED_DERIVATION relative to S, Gamma, phi

7. EXECUTABLE INFERENCE EXAMPLE
Premises: P; P -> Q
Step 1: P [premise]
Step 2: P -> Q [premise]
Step 3: Q [IMPLIES_ELIM, 1, 2]
Conclusion: {P, P -> Q} |- Q

8. VALIDATION INVARIANTS
- Every step has a declared formula, rule, dependency list and scope.
- No dependency may reference a future step.
- No unbound variable or variable capture may be silently introduced.
- Discharged assumptions cannot be used outside their permitted scope.
- Soundness and completeness are properties of a specified system, never universal defaults.
- A countermodel disproves semantic entailment; absence of a proof is not itself a countermodel.
- Informal proofs require separate human or formalisation review; do not label them machine verified.

9. SEMANTIC EQUIVALENCE AND DISTINCTIONS
Proof != theorem: proof is a derivation; theorem is its derived claim.
Derivability != entailment: syntactic and semantic relations coincide only under applicable metatheorems.
Validity != soundness of an argument: a valid argument may have false premises.
ProofStep != premise: a step may be inferred rather than assumed.
Equivalent formulas must be checked under a declared logic and semantics.

10. CONFIDENCE AND PROVENANCE
CONFIDENCE:
  formal_verification: verified | failed | unverified
  source_alignment: unverified
  mathematical_scope: explicitly declared formal system
PROVENANCE:
  canonical_source: source URL above
  author_credit: Mark Higgins — Sky (Recursive AI)
  derivation_evidence: step references and rules

11. FLOW_HASH
FLOW_HASH:
  algorithm: SHA-256
  canonicalisation: UTF-8; LF line endings; deterministic ordering of structured fields
  input: canonical content excluding any populated FLOW_HASH digest field
  digest: COMPUTE_ON_PUBLICATION
Do not invent a cryptographic digest without hashing the final canonical bytes.

12. UPDATE_MODEL
UPDATE_MODEL:
  version: 1.0
  change_policy: revise on changes to inference rules, type constraints or semantics
  validation: rerun proof-step checks and regenerate digest
  backwards_compatibility: preserve prior versions for reproducibility

13. AI_CONSUMPTION
AI_CONSUMPTION:
  tasks: [proof retrieval, dependency tracing, rule checking, theorem linking, countermodel analysis]
  input_types: [Formula, FormalSystem, Proof, ProofStep]
  output_types: [VerificationResult, DependencyGraph, ProofCertificate]
  guardrails: [declare_logic, check_side_conditions, do_not_conflate_truth_and_derivability, disclose_unverified_claims]

END FLOW ALGEBRA