Encyclopedia Delta Delta Kernel Check Forced

ARTICLE 3 claims 3 theorems

Delta Kernel Check Forced

A proof that uses no special assumptions is marked as forced, and the machine-checked library records exactly which assumptions it used.

Verify this page

The forced verdict

In formal logic, a proof is a tree of inference steps that starts from assumptions and ends at a conclusion. The Recognition Science framework's machine-checked library of formal theorems defines a ledger, a discrete record of every special assumption a proof consumes. Most proofs draw on such assumptions, called posits, which include the law of the excluded middle, the limited principle of omniscience, and Markov's principle. The declaration Forced marks the special case where a derivation checks out with an empty ledger: the proof used none of those posits, so its conclusion holds by the framework's own rules alone.

The definition is direct. A derivation is a fully annotated natural-deduction tree for intuitionistic Heyting arithmetic over the distinction signature, with no types and no terms inhabiting types. The kernel is the total function check that audits such a tree in a context and either rejects it as ill-formed or returns the proved formula together with the exact set of posits consumed. Forced holds when check returns the formula with the empty ledger. This is the framework's kernel-native certificate for a claim that needs no special assumptions.

The rules that post to the ledger are exactly three: the law of the excluded middle, the limited principle of omniscience, and Markov's principle, the last restricted to quantifier-free matrices so it stays honestly weaker than excluded middle. Every other rule, including the distinction axioms and the induction schema, is structural and posts nothing. A derivation that uses only structural rules is forced; one that uses a posit is merely conditional, and its ledger names the posit.

What Forced does not claim is just as precise. It does not claim that the conclusion is true in any external or metaphysical sense; it claims only that the derivation is complete and uses no posits. It does not claim that the framework's structural rules are themselves assumption-free, only that no posit was consumed. And it does not claim that a forced derivation is the only kind worth having: conditional derivations with named posits remain fully valid, with their assumptions made explicit.

THEOREM Forced · IndisputableMonolith/DeltaKernel/Check.lean
Forced · IndisputableMonolith/DeltaKernel/Check.lean:214 
/-- FORCED verdict: the tree checks with an empty ledger. This is the
kernel-native σ0 / DELTA_FORCED certificate. -/
def Forced (Γ : Ctx) (d : Deriv) (φ : DFormula) : Prop :=
  check Γ d = some (φ, Ledger.empty)
THEOREM check · IndisputableMonolith/DeltaKernel/Check.lean
check · IndisputableMonolith/DeltaKernel/Check.lean:103 
/-- The kernel: audit a derivation tree in a context. Returns the proved
formula and the exact posit ledger, or `none` if the tree is ill-formed.
Total, structural, and `Prop`-free: the object logic never touches the
host's propositions. -/
def check (Γ : Ctx) : Deriv → Option (DFormula × Ledger)
  | .hyp i =>
      match Γ[i]? with
      | some φ => some (φ, .empty)
      | none => none
  | .eqRefl t => some (.eq t t, .empty)
  | .eqSubst φ t s dEq dT =>
      match check Γ dEq, check Γ dT with
      | some (cEq, o₁), some (cT, o₂) =>
          if cEq = DFormula.eq t s then
            if cT = φ.subst 0 t then some (φ.subst 0 s, o₁.union o₂)
            else none
          else none
      | _, _ => none
  | .succNeZero t => some (.neg (.eq (.succ t) .zero), .empty)
  | .succInj d =>
      match check Γ d with
      | some (.eq (.succ t) (.succ s), o) => some (.eq t s, o)
      | _ => none
  | .addZero t => some (.eq (.add t .zero) t, .empty)
  | .addSucc t s => some (.eq (.add t (.succ s)) (.succ (.add t s)), .empty)
  | .mulZero t => some (.eq (.mul t .zero) .zero, .empty)
  | .mulSucc t s => some (.eq (.mul t (.succ s)) (.add (.mul t s) t), .empty)
  | .ind φ d₀ dS =>
      match check Γ d₀, check Γ dS with
      | some (c₀, o₁), some (cS, o₂) =>
          if c₀ = φ.subst 0 .zero then
            if cS = DFormula.all (.impl φ φ.stepSucc) then
              -- Stratification: induction on a quantified formula posts the
              -- FULL-IND tier flag; on a QF formula it stays in the QF tier.
              -- Whether FULL-IND is "forced by initiality" or a strength step
              -- is the measured question the flag exists to answer.
              let base := o₁.union o₂
              let o := if φ.isQF then base else base.union .ofIndFull
              some (.all φ, o)
            else none
          else none
      | _, _ => none
  | .implIntro φ d =>
      match check (φ :: Γ) d with
      | some (ψ, o) => some (.impl φ ψ, o)
      | none => none
  | .implElim d₁ d₂ =>
      match check Γ d₁, check Γ d₂ with
      | some (.impl φ ψ, o₁), some (φ', o₂) =>
          if φ' = φ then some (ψ, o₁.union o₂) else none
      | _, _ => none
  | .conjIntro d₁ d₂ =>
      match check Γ d₁, check Γ d₂ with
      | some (φ, o₁), some (ψ, o₂) => some (.conj φ ψ, o₁.union o₂)
      | _, _ => none
  | .conjElim1 d =>
      match check Γ d with
      | some (.conj φ _, o) => some (φ, o)
      | _ => none
  | .conjElim2 d =>
      match check Γ d with
      | some (.conj _ ψ, o) => some (ψ, o)
      | _ => none
  | .disjIntro1 ψ d =>
      match check Γ d with
      | some (φ, o) => some (.disj φ ψ, o)
      | none => none
  | .disjIntro2 φ d =>
      match check Γ d with
      | some (ψ, o) => some (.disj φ ψ, o)
      | none => none
  | .disjElim d dL dR =>
      match check Γ d with
      | some (.disj φ ψ, o) =>
          match check (φ :: Γ) dL, check (ψ :: Γ) dR with
          | some (χ₁, o₁), some (χ₂, o₂) =>
              if χ₁ = χ₂ then some (χ₁, (o.union o₁).union o₂) else none
          | _, _ => none
      | _ => none
  | .flsElim φ d =>
      match check Γ d with
      | some (.fls, o) => some (φ, o)
      | _ => none
  | .allIntro d =>
      match check (Γ.map (DFormula.lift 1 0)) d with
      | some (φ, o) => some (.all φ, o)
      | none => none
  | .allElim t d =>
      match check Γ d with
      | some (.all φ, o) => some (φ.subst 0 t, o)
      | _ => none
  | .exIntro φ t d =>
      match check Γ d with
      | some (c, o) =>
          if c = φ.subst 0 t then some (.ex φ, o) else none
      | none => none
  | .exElim ψ d dBody =>
      match check Γ d with
      | some (.ex φ, o) =>
          match check (φ :: Γ.map (DFormula.lift 1 0)) dBody with
          | some (ψ', o₂) =>
              if ψ' = ψ.lift 1 0 then some (ψ, o.union o₂) else none
          | none => none
      | _ => none
  | .emPosit φ => some (.disj φ φ.neg, .ofEM)
  | .lpoPosit φ =>
      some (.impl (.all (.disj φ φ.neg)) (.disj (.ex φ) (.all φ.neg)), .ofLPO)
  | .mpPosit φ =>
      if φ.isQF then some (.impl (.neg (.neg (.ex φ))) (.ex φ), .ofMP)
      else none
THEOREM check · IndisputableMonolith/DeltaKernel/Check.lean
check · IndisputableMonolith/DeltaKernel/Check.lean:103 
/-- The kernel: audit a derivation tree in a context. Returns the proved
formula and the exact posit ledger, or `none` if the tree is ill-formed.
Total, structural, and `Prop`-free: the object logic never touches the
host's propositions. -/
def check (Γ : Ctx) : Deriv → Option (DFormula × Ledger)
  | .hyp i =>
      match Γ[i]? with
      | some φ => some (φ, .empty)
      | none => none
  | .eqRefl t => some (.eq t t, .empty)
  | .eqSubst φ t s dEq dT =>
      match check Γ dEq, check Γ dT with
      | some (cEq, o₁), some (cT, o₂) =>
          if cEq = DFormula.eq t s then
            if cT = φ.subst 0 t then some (φ.subst 0 s, o₁.union o₂)
            else none
          else none
      | _, _ => none
  | .succNeZero t => some (.neg (.eq (.succ t) .zero), .empty)
  | .succInj d =>
      match check Γ d with
      | some (.eq (.succ t) (.succ s), o) => some (.eq t s, o)
      | _ => none
  | .addZero t => some (.eq (.add t .zero) t, .empty)
  | .addSucc t s => some (.eq (.add t (.succ s)) (.succ (.add t s)), .empty)
  | .mulZero t => some (.eq (.mul t .zero) .zero, .empty)
  | .mulSucc t s => some (.eq (.mul t (.succ s)) (.add (.mul t s) t), .empty)
  | .ind φ d₀ dS =>
      match check Γ d₀, check Γ dS with
      | some (c₀, o₁), some (cS, o₂) =>
          if c₀ = φ.subst 0 .zero then
            if cS = DFormula.all (.impl φ φ.stepSucc) then
              -- Stratification: induction on a quantified formula posts the
              -- FULL-IND tier flag; on a QF formula it stays in the QF tier.
              -- Whether FULL-IND is "forced by initiality" or a strength step
              -- is the measured question the flag exists to answer.
              let base := o₁.union o₂
              let o := if φ.isQF then base else base.union .ofIndFull
              some (.all φ, o)
            else none
          else none
      | _, _ => none
  | .implIntro φ d =>
      match check (φ :: Γ) d with
      | some (ψ, o) => some (.impl φ ψ, o)
      | none => none
  | .implElim d₁ d₂ =>
      match check Γ d₁, check Γ d₂ with
      | some (.impl φ ψ, o₁), some (φ', o₂) =>
          if φ' = φ then some (ψ, o₁.union o₂) else none
      | _, _ => none
  | .conjIntro d₁ d₂ =>
      match check Γ d₁, check Γ d₂ with
      | some (φ, o₁), some (ψ, o₂) => some (.conj φ ψ, o₁.union o₂)
      | _, _ => none
  | .conjElim1 d =>
      match check Γ d with
      | some (.conj φ _, o) => some (φ, o)
      | _ => none
  | .conjElim2 d =>
      match check Γ d with
      | some (.conj _ ψ, o) => some (ψ, o)
      | _ => none
  | .disjIntro1 ψ d =>
      match check Γ d with
      | some (φ, o) => some (.disj φ ψ, o)
      | none => none
  | .disjIntro2 φ d =>
      match check Γ d with
      | some (ψ, o) => some (.disj φ ψ, o)
      | none => none
  | .disjElim d dL dR =>
      match check Γ d with
      | some (.disj φ ψ, o) =>
          match check (φ :: Γ) dL, check (ψ :: Γ) dR with
          | some (χ₁, o₁), some (χ₂, o₂) =>
              if χ₁ = χ₂ then some (χ₁, (o.union o₁).union o₂) else none
          | _, _ => none
      | _ => none
  | .flsElim φ d =>
      match check Γ d with
      | some (.fls, o) => some (φ, o)
      | _ => none
  | .allIntro d =>
      match check (Γ.map (DFormula.lift 1 0)) d with
      | some (φ, o) => some (.all φ, o)
      | none => none
  | .allElim t d =>
      match check Γ d with
      | some (.all φ, o) => some (φ.subst 0 t, o)
      | _ => none
  | .exIntro φ t d =>
      match check Γ d with
      | some (c, o) =>
          if c = φ.subst 0 t then some (.ex φ, o) else none
      | none => none
  | .exElim ψ d dBody =>
      match check Γ d with
      | some (.ex φ, o) =>
          match check (φ :: Γ.map (DFormula.lift 1 0)) dBody with
          | some (ψ', o₂) =>
              if ψ' = ψ.lift 1 0 then some (ψ, o.union o₂) else none
          | none => none
      | _ => none
  | .emPosit φ => some (.disj φ φ.neg, .ofEM)
  | .lpoPosit φ =>
      some (.impl (.all (.disj φ φ.neg)) (.disj (.ex φ) (.all φ.neg)), .ofLPO)
  | .mpPosit φ =>
      if φ.isQF then some (.impl (.neg (.neg (.ex φ))) (.ex φ), .ofMP)
      else none

What this page does not claim

Forced does not claim the conclusion is true in any external sense, only that the derivation is complete and uses no posits. Forced does not claim the structural rules are assumption-free, only that no posit was consumed. Forced does not claim conditional derivations are invalid; they remain fully valid with their assumptions named.

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/Check.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND