3 Typed proof fields
On this page · Permalink · Source line 298
The first formal object is a directed hypergraph. A justification may require several premises at once, and a claim may admit several alternative justifications.
Definition 3.1: Typed proof field
A finite typed proof field is a tuple
where:
\(V\) is a finite set of claim nodes.
\({\mathcal J}\) is a finite set of justifications.
Each \(j\in{\mathcal J}\) has a finite premise set \(\operatorname{prem}(j)\subseteq V\) and one conclusion \(\operatorname{con}(j)\in V\).
\(A\subseteq V\) is the set of required premises of the declared judgment.
\(T\subseteq V\) is the nonempty target set.
\(\tau\) assigns node and justification types.
\({\mathcal E}\) is a typed evidence ledger.
\(\mathbf v\) assigns nonnegative value coordinates to nodes.
\(\mathbf c\) assigns nonnegative storage, audit, recovery, and cognitive costs.
The dependency graph contains an edge \(u\to v\) whenever \(u\in\operatorname{prem}(j)\) and \(v=\operatorname{con}(j)\) for some justification \(j\). It is required to be acyclic.
A single justification is conjunctive in its premise set. All listed premises must be available. Multiple justifications with the same conclusion are alternatives. This gives the familiar AND/OR structure of proof search without forcing it into an ordinary graph.
Definition 3.2: Admissible leaf
A node is an admissible leaf when it is a required premise, a declared axiom, or an explicitly admitted external result. Write \(L\) for this set, so \(A\subseteq L\). A certified justification with no premises can also derive a node, but it remains a justification and need not make that node a member of \(L\). The distinction matters when extracting the smallest certificate.
Required premises are not necessarily the entire assumption context. Admitted axioms and external results remain visible in the supporting ledger. The notation \(A\vdash B\) is relative to that declared background and does not erase those dependencies. A comparison between certificates must retain the assumptions under which each certificate is valid.
Definition 3.3: Certified subfield
The certified subfield \({\mathcal P}^{\mathrm{cert}}\) contains every node of \({\mathcal P}\) and only those justifications accepted by the declared certification policy. Evidence and scope are part of that policy. A certification flag records acceptance: it is not itself a proof that the rule is sound under an intended mathematical interpretation. That separate soundness contract is made explicit in Section 9.
Definition 3.4: Derivability
Let \(K\subseteq V\) be a selected node set and let \(H\subseteq{\mathcal J}\) be a selected justification set. The derivable set \(D(K,H)\) is the least subset of \(K\) satisfying:
every selected admissible leaf belongs to \(D(K,H)\).
if \(j\in H\), \(\operatorname{prem}(j)\subseteq D(K,H)\), and \(\operatorname{con}(j)\in K\), then \(\operatorname{con}(j)\in D(K,H)\).
When only certified justifications are allowed, write \(D_{\mathrm{cert}}(K,H)\).
Proposition 3.5: Finite derivability
For a finite acyclic proof field, \(D(K,H)\) is uniquely determined and can be computed in one topological pass through the dependency graph.
Proof
Acyclicity gives a topological ordering of the nodes. Begin with the selected admissible leaves. At each later node, test whether one selected incoming justification has all of its premises already derived. Add the node exactly when such a justification exists. No later step can change the status of an earlier node because all dependencies point forward. The resulting set satisfies the closure rules. Any set satisfying the rules must contain every node added by this pass, so the result is the least such set and is unique.
alternative_proofs.json. Their stored node costs are one and three. A storage objective selects the short route, while a task requiring explanatory information can prefer the richer route. Alternative derivations are OR choices, not extra conjunctive premises.