Delta Kernel Sigma Uses Full Ind

The induction tier scan

In formal logic, proofs are often built from smaller pieces. One powerful piece is full induction, a rule that lets you prove a statement about all objects by showing it holds for a base case and then for each successor. The Recognition Science framework's machine-checked library of formal theorems defines a function called usesFullInd, which is a simple test: it scans a proof's structure and reports whether that proof contains an induction step applied to a formula with quantifiers, meaning a statement like "for all numbers" or "there exists a number."

The key result is a theorem stating that this syntactic scan exactly matches the framework's internal ledger, a discrete record of events that tracks which reasoning principles a proof relies on. The theorem usesFullInd_eq_scan_indFull proves that the scan's boolean output is identical to the ledger's full-induction flag. This means a proof's use of full induction is not a subtle semantic matter; it is a visible, structural fact about the proof tree itself. A third party can verify it by walking through the proof's syntax, without needing to understand the checking algorithm.

This matters for the framework's notion of a forced proof, one that uses no unproven assumptions. The framework proves that a forced proof is exactly one whose structure contains no posit symbols and no full-induction node. The theorem forced_syntactic_audit establishes this: if a proof is forced, then the scan shows it is posit-free and does not use full induction. This makes the framework's strongest claims auditable by a simple tree-walk, independent of the kernel's implementation details.

What usesFullInd does not claim is equally important. It does not say that full induction is invalid or that proofs using it are wrong. It is purely a descriptive tool, a way to classify proofs by their syntactic features. The declaration does not evaluate the truth of the formulas involved, nor does it determine whether a proof is correct. It only reports on the presence of a particular structural pattern, much like a word processor's find function reports whether a word appears in a document.

/-- The grep scan for the induction tier agrees with the `indFull` flag of the
syntactic ledger. -/
theorem usesFullInd_eq_scan_indFull (d : Deriv) :
    usesFullInd d = (scanLedger d).indFull := by
  induction d with
  | hyp _ => rfl
  | eqRefl _ => rfl
  | eqSubst _ _ _ dEq dT ihE ihT =>
      simp [usesFullInd, scanLedger, Ledger.union, ihE, ihT]
  | succNeZero _ => rfl
  | succInj d ih => simpa [usesFullInd, scanLedger] using ih
  | addZero _ => rfl
  | addSucc _ _ => rfl
  | mulZero _ => rfl
  | mulSucc _ _ => rfl
  | ind φ d₀ dS ih₀ ihS =>
      cases hqf : φ.isQF <;>
        simp [usesFullInd, scanLedger, hqf, Ledger.union, Ledger.ofIndFull,
          ih₀, ihS]
  | implIntro _ d ih => simpa [usesFullInd, scanLedger] using ih
  | implElim d₁ d₂ ih₁ ih₂ =>
      simp [usesFullInd, scanLedger, Ledger.union, ih₁, ih₂]
  | conjIntro d₁ d₂ ih₁ ih₂ =>
      simp [usesFullInd, scanLedger, Ledger.union, ih₁, ih₂]
  | conjElim1 d ih => simpa [usesFullInd, scanLedger] using ih
  | conjElim2 d ih => simpa [usesFullInd, scanLedger] using ih
  | disjIntro1 _ d ih => simpa [usesFullInd, scanLedger] using ih
  | disjIntro2 _ d ih => simpa [usesFullInd, scanLedger] using ih
  | disjElim d dL dR ih ihL ihR =>
      simp [usesFullInd, scanLedger, Ledger.union, ih, ihL, ihR]
  | flsElim _ d ih => simpa [usesFullInd, scanLedger] using ih
  | allIntro d ih => simpa [usesFullInd, scanLedger] using ih
  | allElim _ d ih => simpa [usesFullInd, scanLedger] using ih
  | exIntro _ _ d ih => simpa [usesFullInd, scanLedger] using ih
  | exElim _ d dBody ih ihB =>
      simp [usesFullInd, scanLedger, Ledger.union, ih, ihB]
  | emPosit _ => rfl
  | lpoPosit _ => rfl
  | mpPosit _ => rfl

/-- A FORCED verdict (empty ledger) implies the tree is posit-free AND stayed
in the QF induction tier: the `σ0 @ QF-IND` certificate is a pure syntactic
occurrence fact, auditable by tree-walk with no knowledge of the checker. -/
theorem forced_syntactic_audit {Γ : Ctx} {d : Deriv} {φ : DFormula}
    (h : Forced Γ d φ) :
    positFree d = true ∧ usesFullInd d = false := by
  have hscan : Ledger.empty = scanLedger d := scan_eq_check h
  constructor
  · rw [positFree_eq_scan_isForced, ← hscan]; rfl
  · rw [usesFullInd_eq_scan_indFull, ← hscan]; rfl

What this page does not claim

The declaration does not judge whether full induction is a valid reasoning principle. It does not evaluate the truth of any formula or the correctness of a proof. It does not claim that proofs using full induction are forbidden or flawed.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/DeltaKernel/Sigma.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: