appendix sectiontutorials

ch:first-order-proof-theory: ch:first-order-proof-theory

Problem and result. Construct a finite-height LJ searcher in three runnable stages. The first stage searches and checks Ax and implication; the second adds the restricted universal language; the third adds alpha-normal caching and reinstantiation. The finished program returns a checked tree, finds the quantified implication first at height three, and rejects the missing premise through height six.

Representation. The artifact chooses a small named representation: Term is Bound, Const Nat, or Eigen Nat; formulas have only unary AtomP, unary AtomQ, Imp, and All. A single Bound token keeps one-binder instantiation visible, but it cannot distinguish an outer occurrence below an inner All. Consequently, the executable language permits a bound token only outside nested universal bodies. De Bruijn indices or levels would support nested binders and make alpha-equivalence structural. A full named representation would support the same language but would require capture-avoiding renaming and a larger freshness invariant. The restricted token is appropriate only because the acceptance corpus deliberately tests the smaller language.

Stage 1: uncached Ax and implication. Reuse the artifact datatypes in a scratch Kappa module, but let the first search generate only Ax, ImpR, and ImpL; the checker rejects the two universal constructors until Stage 2. Implement equality and membership first. The complete Stage 1 checker then follows the rule order, rather than trusting a search flag:

validCore : List Formula -> Formula -> Proof -> Bool
let validCore context goal proof decreases structural proof =
  match proof
    case Ax formula ->
      formulaEq formula goal && memberFormula goal context
    case ImpR left sub ->
      match goal
        case Imp expected right ->
          formulaEq left expected &&
          validCore
            (insertFormula expected context) right sub
        case _ -> False
    case ImpL left right p q ->
      memberFormula (Imp left right) context &&
      validCore context left p &&
      validCore
        (insertFormula right context) goal q
    case AllR _ _ _ -> False
    case AllL _ _ _ -> False

Implement uncached searchCore with the same three rule families. At positive height it tries Ax, then implication-right when the goal is an implication; if that right-rule branch fails, it scans antecedent implications for implication-left before reporting failure. Each premise receives the predecessor height. Run it on $P (c), P (c) \to Q (c) \Rightarrow Q (c)$ : height two returns the ImpL tree with two Ax leaves, and validCore accepts it. Run $P (c) \Rightarrow Q (c)$ at heights zero through three: every run returns failure. This is the first complete search–certificate–checker path. Also run $P (c), P (c) \to (P (c) \to Q (c)) \Rightarrow P (c) \to Q (c)$ at height two. Implication-right fails, but implication-left closes with two Ax premises; this case detects a searcher that commits to the right rule.

Stage 2: universals and ordered eigenparameters. Add Bound, Const, Eigen, All, AllR, and AllL. Define instantiate to replace Bound in atoms and implications and to stop at nested All; that stopping clause enforces the stated language boundary. Carry eigenparameters as an introduction-ordered list. Universal-right appends the least name absent from the context, goal, and list. Universal-left scans the finite term pool followed by the eigenparameter terms. At a rule node, decrement mathematical height only for recursive premise searches. Scanning formulas or terms does not consume height. The quantified sequent $\forall x (P (x) \to Q (x)), P (c) \Rightarrow Q (c)$ now fails at height two and returns at height three:

AllL(c, ImpL(Ax(P(c)), Ax(Q(c))))

Extend the independent checker with AllR and AllL in that order. Give it the term pool as an explicit input. It checks that an AllR name equals the least name absent from the context, goal, and branch list, and that an AllL witness belongs to the pool followed by the branch eigenparameters. Add one otherwise valid forged node for each omitted condition and require both to be rejected.

Stage 3: canonical cache. A cache key stores height, sorted canonical context, canonical goal, and eigenparameter count. The cached proof numbers branch parameters by introduction order. Map the $i$ -th member of the ordered list to $ϵ_{i}$ , normalize formulas recursively, and sort the context. canonProof extends the map when it crosses AllR. decodeProof reverses the map; at a cached universal-right node it chooses the least name fresh for the requesting state and decodes the subtree under the extended inverse map. The two identityGoal runs search $\emptyset \Rightarrow \forall x (P (x) \to P (x))$ from branch lists $(e_{0})$ and $(e_{1})$ . Their root keys have the same eigenparameter count. The first decoded proof introduces $e_{1}$ , the second introduces $e_{0}$ ; the second run reuses one root entry, keeps the cache length unchanged, and validates the request-side proof.

The finished searchWork carries a separate administrative work budget so Kappa accepts the mutually recursive alternative scans. A successful branch returns Found; a completed finite failure returns NotFound; budget exhaustion returns WorkExhausted and is never cached as logical failure. Compute proofHeight from every successful tree rather than trusting the input bound.

A failing version. The in-file validAxMutant retains equality between the Ax formula and the goal but deletes context membership. The forged tree Ax (AtomQ c) is offered as a proof of $Q (c)$ from $P (c)$ . The mutant accepts it and valid rejects it; the inline harness requires both outcomes.

Acceptance test. Run the four exact commands from the README. Require first success at height three, failure at height two, failure of the missing-premise sequent at bounds zero through six, an independently valid tree, the exact printed rule tree, a right-to-left fallback, two rejected quantified-rule forgeries, a reinstantiated alpha-cache hit, a killed membership-only Ax mutant, one passing corpus test, and an empty audit.

Mathematical boundary. The Kappa program implements the Ax and implication rules plus universals for unary $P / Q$ formulas whose bound token does not occur beneath a nested universal. It does not implement the chapter’s general binding syntax. The administrative work budget is not proof height. The finite run proves neither search completeness nor cut elimination.