Foundation Maximal Forcing Independence Witness Independence Witness

Witnessing independence

In mathematics, a statement is independent of a set of rules when neither the statement nor its negation follows from those rules. The classical way to prove independence is to build two models: two structures that both satisfy the rules, one where the statement is true and one where it is false. The IndependenceWitness declaration packages exactly this idea as a formal object. It pairs a yes_model with a no_model, records that both are admissible under the same admissibility condition, and records that the claim holds in the first and fails in the second.

The structure appears in the framework's machine-checked library of formal theorems, inside the foundation module on maximal forcing. The library defines a claim universe, which is a collection of possible realizations together with an admissibility predicate that says which realizations count as legitimate. A claim is a function that takes a realization and returns a truth value. An IndependenceWitness for a claim C over a universe U is then a concrete pair: two admissible realizations, one where C holds and one where it does not. The declaration requires all six fields explicitly, so no part of the witness can be left implicit.

The accompanying theorem, independent_of_witness, converts any such witness into the proposition-level Independent tag. The proof is immediate: the witness fields are exactly the components the Independent tag demands. This means the framework does not treat independence as a vague appeal to contingency. If a claim is not forced, maximal closure demands a countermodel pair, and the witness supplies it. The theorem is proved in the machine-checked library with no framework-specific axioms, so the step from witness to independence is fully verified.

What the declaration does not claim is worth stating plainly. An IndependenceWitness does not say that the claim is false, only that it is not forced. It does not say that the two models are physically real, only that they are admissible under the formal admissibility condition. It does not say that every independent claim has a witness; the structure provides a witness when one exists, and the theorem converts it. The declaration is a tool for establishing independence, not a claim about which claims are independent or what the admissibility condition should be.

/-- Explicit countermodel pair for independence of a claim over an admissible
class. -/
structure IndependenceWitness (U : ClaimUniverse.{u})
    (C : RealityClaim U.Realization) where
  yes_model : U.Realization
  no_model : U.Realization
  yes_admissible : yes_model ∈ U.admissibility.admissible
  no_admissible : no_model ∈ U.admissibility.admissible
  yes_holds : C.holds yes_model
  no_fails : ¬ C.holds no_model

/-- An explicit witness implies the proposition-level `Independent` tag. -/
theorem independent_of_witness {U : ClaimUniverse.{u}}
    {C : RealityClaim U.Realization}
    (W : IndependenceWitness U C) :
    Independent U.admissibility.admissible C := by
  exact ⟨W.yes_model, W.no_model, W.yes_admissible, W.no_admissible,
    W.yes_holds, W.no_fails⟩

What this page does not claim

An IndependenceWitness does not say the claim is false, only that it is not forced. The declaration does not say the two models are physically real, only admissible under the formal condition. It does not claim that every independent claim has a witness.

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/Foundation/MaximalForcing/IndependenceWitness.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: