MatchingLogic.EntryIII.WitnessedCollapse

def MatchingLogic.pointedTheory {S : Signature} (M : Model S) (rho : ℕ → M.carrier) (u : M.carrier) : Set (Pattern S ℕ)

The complete theory of a model at one point under a fixed valuation.

Equations

• MatchingLogic.pointedTheory M rho u = {p : MatchingLogic.Pattern S ℕ | u ∈ M.denote rho p}

theorem MatchingLogic.pointedTheory_isMCS {S : Signature} (M : Model S) (rho : ℕ → M.carrier) (u : M.carrier) : IsMCS (pointedTheory M rho u)

Every pointed model theory is a maximal locally consistent set.

theorem MatchingLogic.pointedTheory_witnessed {S : Signature} (M : Model S) (rho : ℕ → M.carrier) (u : M.carrier) (hrho : Function.Surjective rho) : Witnessed (pointedTheory M rho u)

A surjective valuation gives the pointed theory a name for every semantic existential witness.

@[reducible, inline]

abbrev MatchingLogic.WitnessCollapseSig : Signature

The countermodel needs no symbols: variables and existential quantification already separate ordinary witnesses from fresh witnesses.

Equations

• MatchingLogic.WitnessCollapseSig = { Sym := Empty, arity := fun (e : Empty) => e.elim }

@[reducible, inline]

abbrev MatchingLogic.witnessCollapseModel : Model WitnessCollapseSig

The two-point empty-signature model used for the witness-collapse example.

Equations

• MatchingLogic.witnessCollapseModel = { carrier := Bool, nonempty := ⋯, interp := fun (e : MatchingLogic.WitnessCollapseSig.Sym) => Empty.elim e }

def MatchingLogic.witnessCollapseRho : ℕ → witnessCollapseModel.carrier

Variable 0 names true; every other variable names false.

Equations

• MatchingLogic.witnessCollapseRho n = decide (n = 0)

def MatchingLogic.witnessCollapseTheory : Set (Pattern WitnessCollapseSig ℕ)

The complete pointed theory at true.

Equations

• MatchingLogic.witnessCollapseTheory = MatchingLogic.pointedTheory MatchingLogic.witnessCollapseModel MatchingLogic.witnessCollapseRho true

theorem MatchingLogic.witnessCollapseTheory_isMCS : IsMCS witnessCollapseTheory

The pointed theory is a genuine maximal locally consistent set.

theorem MatchingLogic.witnessCollapseTheory_witnessed : Witnessed witnessCollapseTheory

Surjectivity of the valuation supplies an ordinary name for every semantic existential witness.

theorem MatchingLogic.witnessCollapseTheory_not_freshWitnessed : ¬FreshWitnessed witnessCollapseTheory

The existential ∃ 0. var 0 belongs to the pointed theory, but every fresh name denotes false, so no fresh Henkin implication belongs to it.

theorem MatchingLogic.witnessed_freshWitnessed_of_isMCS_counterexample : ∃ (Gamma : Set (Pattern WitnessCollapseSig ℕ)), IsMCS Gamma ∧ Witnessed Gamma ∧ ¬FreshWitnessed Gamma

A concrete counterexample to the proposed collapse theorem, including the maximality obligation.

theorem MatchingLogic.witnessed_freshWitnessed_of_isMCS_refuted : ¬∀ {Gamma : Set (Pattern WitnessCollapseSig ℕ)}, IsMCS Gamma → Witnessed Gamma → FreshWitnessed Gamma

Direct negation of the proposed implication at the counterexample signature.

theorem MatchingLogic.alpha_variant_has_a_fresh_witness : ∃ y ∉ (Pattern.var 1).allVars, (Pattern.ex 1 (Pattern.var 1)).imp (Pattern.captureAvoidingSubst 1 y (Pattern.var 1)) ∈ witnessCollapseTheory

The failure is not stable under α-renaming.

∃0. var 0 has no fresh witness above: the only variable naming the witnessing element is 0, and 0 occurs in the body, so freshness over allVars rules it out. Its α-variant ∃1. var 1 is a different raw pattern with the same meaning, and for it the name 0 is fresh — so a fresh witness exists.

This locates ONE cause of the phenomenon: on raw named syntax the choice of bound name can exhaust the supply of usable witnesses, and choosing another representative of the same α-class restores it.

It does NOT show that α is the whole story, and an earlier version of this docstring said it was. AlphaFreshWitnessed.lean refutes that: there is an MCS that is Witnessed and fails the α-RELAXED condition too, so quotienting by α would not remove the need for the stronger invariant. What does remove it is an infinite supply of usable witnesses — see WitnessSupply.lean.