MatchingLogic.EntryIII.WitnessSupply

The variable-supply hypothesis separating ordinary and fresh witnessedness.

An infinite supply of Henkin implications for each existential must contain a witness outside the finite raw-variable support of its body. Maximality and ordinary witnessedness are retained in the theorem interface to make the comparison with the canonical-model hypotheses explicit; the supply condition itself is what does the work.

def MatchingLogic.InfiniteWitnessSupply {S : Signature} (Gamma : Set (Pattern S ℕ)) : Prop

Every existential in Gamma has infinitely many Henkin names whose capture-avoiding instances are already licensed by implications in Gamma.

Equations

• One or more equations did not get rendered due to their size.

def MatchingLogic.InfiniteFreshVariableSupply {S : Signature} (Gamma : Set (Pattern S ℕ)) : Prop

The source-style variable supply for a starting theory: infinitely many names occur free in none of its patterns.

Equations

• MatchingLogic.InfiniteFreshVariableSupply Gamma = {y : ℕ | ∀ q ∈ Gamma, y ∉ MatchingLogic.FV q}.Infinite

theorem MatchingLogic.freshWitnessed_of_witnessed_of_supply {S : Signature} {Gamma : Set (Pattern S ℕ)} (hSupply : InfiniteWitnessSupply Gamma) : FreshWitnessed Gamma

An infinite supply of usable witnesses upgrades ordinary witnessedness to raw-fresh witnessedness. The proof is short: p.allVars is finite.

Henkin extension of a set with a fresh variable supply

@[instance_reducible]

noncomputable def MatchingLogic.witnessSupplyDecidableEqPattern {S : Signature} : DecidableEq (Pattern S ℕ)

Local decidable equality used by the fresh-variable supply construction.

Equations

• MatchingLogic.witnessSupplyDecidableEqPattern = Classical.decEq (MatchingLogic.Pattern S ℕ)

theorem MatchingLogic.locConsistent_extend_freshWitnessed_isMCS {S : Signature} [Countable (Pattern S ℕ)] {Gamma : Set (Pattern S ℕ)} (hGamma : LocConsistent Gamma) (hSupply : InfiniteFreshVariableSupply Gamma) : ∃ (Delta : Set (Pattern S ℕ)), Gamma ⊆ Delta ∧ IsMCS Delta ∧ FreshWitnessed Delta

A locally consistent set extends to a fresh-witnessed MCS provided the starting syntax leaves an infinite reserve of variables free in none of its members. This is the additional hypothesis that the raw-Nat formulation needs in place of the source's extension from V to V⁺.

theorem MatchingLogic.locConsistent_extend_freshWitnessed_isMCS_unrestricted_refuted : ¬∀ {Gamma : Set (Pattern WitnessCollapseSig ℕ)}, LocConsistent Gamma → ∃ (Delta : Set (Pattern WitnessCollapseSig ℕ)), Gamma ⊆ Delta ∧ IsMCS Delta ∧ FreshWitnessed Delta

The same extension statement without a variable-supply hypothesis is false. Taking the existing witnessed-but-not-fresh MCS as the starting set leaves no locally consistent proper extension in which freshness could be repaired.