18 Versioned proof objects
On this page · Permalink · Source line 1758
A proof archive changes. Claims are strengthened, corrected, refuted, or split. A reproducible theory therefore needs stable identifiers and explicit version relations.
Definition 18.1: Versioned proof object
A versioned proof object is a sequence
whose nodes and justifications carry stable identifiers. Each transition records additions, removals, altered scopes, evidence changes, and a digest of its parent version.
Definition 18.2: Append-only certified update
An update \({\mathcal P}_i\to{\mathcal P}_{i+1}\) is append-only certified when every existing node, admissible-leaf status, evidence record, interpretation, and certified justification remains unchanged. The later field may add records and certified rules but may not withdraw an earlier admitted leaf or change the scope of an earlier inference.
Theorem 18.3: Derivability is monotone under append-only updates
Every target derivable in \({\mathcal P}_i\) remains derivable in \({\mathcal P}_{i+1}\) under an append-only certified update.
Proof
A certificate in \({\mathcal P}_i\) uses only nodes and certified justifications that remain unchanged in \({\mathcal P}_{i+1}\). The same selected subfield therefore satisfies the same derivability closure in the later version.
Retractions and semantic changes are not append-only. They require invalidation analysis.
Definition 18.4: Syntactic affected set
For a changed node set \(X\subseteq V\), define
where descendants are computed in the declared dependency graph.
Theorem 18.5: Minimal closed syntactic review set
The set \(\operatorname{Aff}(X)\) is the unique smallest node set \(Y\) such that \(X\subseteq Y\) and \(Y\) is closed under outgoing dependency edges: whenever \(u\in Y\) and \(u\to v\) is a declared dependency edge, then \(v\in Y\).
Proof
By construction, every node reachable from \(X\) lies in \(\operatorname{Aff}(X)\), so the set contains \(X\) and is closed under outgoing edges. Let \(Y\) be any other set with those two properties. Every directed path beginning in \(X\) remains inside \(Y\) by induction on path length. Hence every descendant of \(X\) lies in \(Y\), and \(\operatorname{Aff}(X)\subseteq Y\).
The theorem is intentionally syntactic. A descendant can survive after rechecking. The affected set says where review is required, not where falsehood is guaranteed.