MatchingLogic.EntryIII.Witnessed

@[instance_reducible]

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

Local decidable equality used by the witnessed-extension construction.

Equations

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

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

A theory is witnessed when every existential it contains has a Henkin implication to one of its capture-avoiding variable instances.

Equations

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

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

A witnessed theory whose Henkin name is fresh for every raw occurrence in the existential body. This is the source construction's actual stronger invariant; Witnessed is its interface needed by the basic Truth Lemma.

Equations

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

theorem MatchingLogic.FreshWitnessed.toWitnessed {S : Signature} {Gamma : Set (Pattern S ℕ)} (h : FreshWitnessed Gamma) : Witnessed Gamma

theorem MatchingLogic.Provable.swap_not {S : Signature} {Gamma : Set (Pattern S ℕ)} {p q : Pattern S ℕ} (h : Provable Gamma (p.imp q.nt)) : Provable Gamma (q.imp p.nt)

Propositional contraposition in the shape used by quantifier generalisation below.

theorem MatchingLogic.LocProvable.not_ex_of_not_fresh {S : Signature} {Gamma : Set (Pattern S ℕ)} {y : ℕ} {q : Pattern S ℕ} (hfresh : ∀ p ∈ Gamma, y ∉ FV p) (hnot : LocProvable Gamma q.nt) : LocProvable Gamma (Pattern.ex y q).nt

Local universal generalisation of a negation. The side condition is the source condition that the generalised name is absent from every premise.

theorem MatchingLogic.locConsistent_insert_captureAvoidingWitness {S : Signature} {Gamma : Set (Pattern S ℕ)} {x y : ℕ} {p : Pattern S ℕ} (hGamma : LocConsistent Gamma) (hyGamma : ∀ q ∈ Gamma, y ∉ FV q) (hyp : y ∉ p.allVars) : LocConsistent (insert ((Pattern.ex x p).imp (Pattern.captureAvoidingSubst x y p)) Gamma)

Adding one fresh Henkin implication is conservative for local consistency. This is the proof-theoretic heart of the witnessed extension.

Shared Henkin-stage infrastructure

def MatchingLogic.henkinStages {α : Type} (step : List α → α → List α) (enum : ℕ → α) (base : List α) : ℕ → List α

Iterate a witness-adjunction operation along an enumeration.

Equations

• MatchingLogic.henkinStages step enum base 0 = base
• MatchingLogic.henkinStages step enum base n.succ = step (MatchingLogic.henkinStages step enum base n) (enum n)

def MatchingLogic.henkinLimit {α : Type} (stageTheory : List α → Set α) (step : List α → α → List α) (enum : ℕ → α) (base : List α) : Set α

The union of the theories represented by all finite Henkin stages.

Equations

• MatchingLogic.henkinLimit stageTheory step enum base = {q : α | ∃ (n : ℕ), q ∈ stageTheory (MatchingLogic.henkinStages step enum base n)}

theorem MatchingLogic.henkinStages_mono {α : Type} (stageTheory : List α → Set α) (step : List α → α → List α) (enum : ℕ → α) (base : List α) (hstep : ∀ (l : List α) (phi : α), stageTheory l ⊆ stageTheory (step l phi)) : Monotone fun (n : ℕ) => stageTheory (henkinStages step enum base n)

A stage operation that only enlarges represented theories gives a monotone sequence of finite Henkin stages.

theorem MatchingLogic.henkinLimit_covers_list {α : Type} (stageTheory : List α → Set α) (step : List α → α → List α) (enum : ℕ → α) (base l : List α) (hstep : ∀ (stage : List α) (phi : α), stageTheory stage ⊆ stageTheory (step stage phi)) (hl : ∀ q ∈ l, q ∈ henkinLimit stageTheory step enum base) : ∃ (n : ℕ), ∀ q ∈ l, q ∈ stageTheory (henkinStages step enum base n)

Every finite list drawn from a Henkin limit already appears at one common finite stage.

theorem MatchingLogic.henkinLimit_locConsistent {S : Signature} (stageTheory : List (Pattern S ℕ) → Set (Pattern S ℕ)) (step : List (Pattern S ℕ) → Pattern S ℕ → List (Pattern S ℕ)) (enum : ℕ → Pattern S ℕ) (base : List (Pattern S ℕ)) (hstep : ∀ (stage : List (Pattern S ℕ)) (phi : Pattern S ℕ), stageTheory stage ⊆ stageTheory (step stage phi)) (hconsistent : ∀ (n : ℕ), LocConsistent (stageTheory (henkinStages step enum base n))) : LocConsistent (henkinLimit stageTheory step enum base)

Local consistency at every finite stage passes to the shared Henkin limit.

Finite fresh-support stages

def MatchingLogic.Pattern.listSupport {S : Signature} : List (Pattern S ℕ) → Pattern S ℕ

A binder-free pattern whose allVars contains the variables of every pattern in the list.

Equations

• MatchingLogic.Pattern.listSupport [] = MatchingLogic.Pattern.bot
• MatchingLogic.Pattern.listSupport (p :: l) = p.imp (MatchingLogic.Pattern.listSupport l)

theorem MatchingLogic.Pattern.allVars_subset_listSupport {S : Signature} {l : List (Pattern S ℕ)} {p : Pattern S ℕ} (hp : p ∈ l) : p.allVars ⊆ (listSupport l).allVars

Every member's raw-variable support lies in the list support.

Witnessed Lindenbaum extension

theorem MatchingLogic.finite_locConsistent_extend_freshWitnessed_isMCS_of_surjective {S : Signature} (enum : ℕ → Pattern S ℕ) (henum : Function.Surjective enum) (base : List (Pattern S ℕ)) (hbase : LocConsistent {q : Pattern S ℕ | q ∈ base}) : ∃ (Delta : Set (Pattern S ℕ)), {q : Pattern S ℕ | q ∈ base} ⊆ Delta ∧ IsMCS Delta ∧ FreshWitnessed Delta

The finite Henkin construction preserves the raw freshness of the adjoined witness name, not merely the ordinary witnessed property.

theorem MatchingLogic.finite_locConsistent_extend_witnessed_isMCS_of_surjective {S : Signature} (enum : ℕ → Pattern S ℕ) (henum : Function.Surjective enum) (base : List (Pattern S ℕ)) (hbase : LocConsistent {q : Pattern S ℕ | q ∈ base}) : ∃ (Delta : Set (Pattern S ℕ)), {q : Pattern S ℕ | q ∈ base} ⊆ Delta ∧ IsMCS Delta ∧ Witnessed Delta

Enumeration-parametric ordinary witnessedness follows by forgetting the freshness evidence from the stronger construction.

theorem MatchingLogic.finite_locConsistent_extend_freshWitnessed_isMCS {S : Signature} [Countable (Pattern S ℕ)] (base : List (Pattern S ℕ)) (hbase : LocConsistent {q : Pattern S ℕ | q ∈ base}) : ∃ (Delta : Set (Pattern S ℕ)), {q : Pattern S ℕ | q ∈ base} ⊆ Delta ∧ IsMCS Delta ∧ FreshWitnessed Delta

Every locally consistent finite-list theory over a countable pattern language extends to a maximal locally consistent theory with fresh Henkin witnesses.

theorem MatchingLogic.finite_locConsistent_extend_witnessed_isMCS {S : Signature} [Countable (Pattern S ℕ)] (base : List (Pattern S ℕ)) (hbase : LocConsistent {q : Pattern S ℕ | q ∈ base}) : ∃ (Delta : Set (Pattern S ℕ)), {q : Pattern S ℕ | q ∈ base} ⊆ Delta ∧ IsMCS Delta ∧ Witnessed Delta

Every locally consistent finite-list theory over a countable pattern language extends to a witnessed maximal locally consistent set.