21. Choose a certificate with shared premises

Read side by side

All examples · Glossary: minimum-cost certificate · Papers, proofs, Lean, and code

Proof Path Theory distinguishes a valid certificate, an inclusion-minimal certificate and a cheapest certificate. This small recorded rule system shows why those distinctions matter.

Declare the leaves and rules

There are four obligations, \(a,b,c,d\). The final rule requires all four:

Choose from four admissible leaves. Each selected leaf costs one unit and can be used more than once. Obligation nodes, the target and all rules cost zero. There are no mandatory starting leaves.

For example, the first row represents two separate rules \(\{s_1\}\Longrightarrow a\) and \(\{s_1\}\Longrightarrow b\). The table declares the available certified rules for this exercise. It does not assert that arbitrary implications are mathematically valid.

Build and check one certificate

Select the node set \(K=\{s_1,s_3,a,b,c,d,t\}\). Retain the five rules

A forward check proceeds as follows:

1. Admit the selected leaves \(s_1,s_3\).
2. Apply the first four rules to obtain \(a,b,c,d\).
3. Apply the final rule to obtain \(t\).

The selected nodes and rules form a certificate. Its cost is \(1+1=2\). The use of \(s_1\) twice does not charge for that leaf twice.

Establish the minimum and its limits

One leaf supplies only two of the four obligations. No certificate of cost zero or one can reach \(t\). The displayed cost-two certificate is therefore optimal in this finite rule system.

There is another optimum: select \(s_2,s_4\). The other four pairs all miss an obligation:

Each optimum is inclusion-minimal. Removing one of its selected leaves or used rules breaks the derivation. There is no least certificate contained in both optima: their common nodes include no admissible leaf, so they cannot start a derivation. A minimum cost therefore need not identify a unique certificate or a least certificate under inclusion.

Recognize a failed proposal

A record selecting only \(s_1\) reaches \(a,b\) but cannot fire the final rule. Its rejection concerns that record. We have already exhibited valid records for the same target. Exhausting a search budget would also leave the search unresolved, rather than establish that no certificate exists.

Try it

Add a leaf \(s_5\) with four rules supplying \(a,b,c,d\). What happens if its cost is three? What if its cost is one?

Answer: At cost three, the original cost-two pairs remain optimal. At cost one, selecting \(s_5\) gives the new minimum. The permitted rules and costs determine the optimization problem.

This example checks one supplied finite proof field. It does not establish that a selected certificate is the shortest possible proof in every system.

Papers, proofs, Lean, and code

Terms in this example: Finite proof field · Admissible leaf · Recorded inference rule · Verification closure · Inclusion-minimal certificate · Least certificate · Minimum-cost certificate

This example compares certificates in a supplied finite rule system. It illustrates verification closure and cost selection in Proof Path Theory. It does not certify arbitrary inference rules or Python implementations.

Proof Path Theory

Read · Written proofs · Lean coverage · Code and setup · Evidence

Source passages:

• Proof Path Theory: certificates and verification closure
• Proof Path Theory: alternative derivations and costs

Edition guide and reproduction instructions. Use each work’s Code and setup link for its implementation. The arithmetic check below covers this tutorial separately.

Python arithmetic check for this example: proof_certificates(). This checks the displayed rational, modular or finite-set calculations exactly.

The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.

• Previous: Separate support from multiplicity
• Next: Recover the memory hidden by a summary
• All examples
• Topic map
• Example coverage by work