Delta Kernel Examples Mp Rejects Quantified

The Markov posit guard

In logic, the Markov principle is a rule that lets you infer existence from the impossibility of non-existence, but only under strict conditions. The Recognition Science framework's machine-checked library of formal theorems contains a declaration, mp_rejects_quantified, that pins down one of those conditions precisely. It states that the checker returns none when asked to apply the Markov posit to a formula that begins with a universal quantifier, such as "for all x, x equals x." In plain terms, the rule accepts the principle only for quantifier-free statements, and it rejects it for quantified ones. The rejection is not a convention or a policy choice; it is enforced by the checker itself, which is the executable kernel that audits every derivation.

To see what this means, contrast it with a companion declaration, mp_accepts_qf. That one shows the checker accepts the Markov posit for a quantifier-free matrix, a formula with no "for all" or "there exists" at its head. The pair of declarations demonstrates the boundary: the posit is available exactly when the formula it acts on is quantifier-free. This is a guard on the rule's applicability, and the guard is part of the kernel's behavior, not an external restriction. The declaration mp_rejects_quantified is a theorem about that behavior, verified by computation, so it is not a matter of opinion or interpretation.

The practical consequence is that any derivation using the Markov posit carries a precise, machine-checked record of what kind of formula it applied to. This matters for the framework's broader project of auditing proofs: the ledger, a discrete record of every recognition event and its cost, can distinguish between a derivation that used the posit legitimately on a quantifier-free statement and one that tried to stretch it further. The declaration does not say the Markov principle is false, nor does it say quantified statements are never provable. It says only that this particular rule, this posit, does not apply to them. Other rules, such as full induction, remain available for quantified formulas, as a separate declaration in the same file shows.

What the declaration does not claim is just as important as what it establishes. It does not prove that the Markov principle is invalid in general, only that this specific posit rejects quantified inputs. It does not say anything about whether a quantified statement like "for all x, x equals x" is true or false; that statement is provable by other means. And it does not claim that the checker's rejection is the only possible behavior, only that this is what the executable kernel does. The declaration is a narrow, precise fact about a guard, and it earns its place by making the boundary between quantifier-free and quantified applications of the Markov posit explicit and machine-checked.

/-- Markov on a quantified matrix: REJECTED by the kernel (not merely
discouraged). -/
theorem mp_rejects_quantified :
    check [] (.mpPosit (.all (.eq (.var 0) (.var 0)))) = none := by
  decide

/-- Markov on a QF matrix: accepted, posts `mp`. -/
theorem mp_accepts_qf :
    check [] (.mpPosit qfMatrix) =
      some (.impl (.neg (.neg (.ex qfMatrix))) (.ex qfMatrix), .ofMP) := by
  decide

What this page does not claim

The Markov principle is false or invalid in general. Quantified statements like "for all x, x equals x" are unprovable. The checker's rejection is the only possible behavior for a Markov-style rule.

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