MatchingLogic.EntryIII.CanonicalExistence

def MatchingLogic.CanonicalExistenceProperty (S : Signature) : Prop

The exact one-sorted universal statement of the source's canonical Existence Lemma. It lives with the stage-system interface so the construction precedes, rather than imports, the Truth Lemma that consumes it.

Equations

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

The simultaneous finite-stage invariant

The following is the exact one-sorted form of the invariant in the proof of TR Theorem 73. A stage is a finite list at every argument position. The important app_mem field is joint: extending each argument theory separately would not establish the universal clause of canonicalInterp.

structure MatchingLogic.NaryStageSystem {S : Signature} (sigma : S.Sym) (Gamma : CanonicalCarrier S) (phi : Fin (S.arity sigma) → Pattern S ℕ) (enum : ℕ → Pattern S ℕ) : Type

The finite, simultaneous construction used in the n-ary Existence Lemma. enum is shared by every argument position because this development is one-sorted. decide is condition (1), witness is condition (2), and app_mem is condition (4) in the source proof.

• stages : ℕ → Fin (S.arity sigma) → List (Pattern S ℕ)

  The finite theory accumulated at each stage and argument position.

• base (i : Fin (S.arity sigma)) : phi i ∈ self.stages 0 i
• mono (k : ℕ) (i : Fin (S.arity sigma)) (q : Pattern S ℕ) : q ∈ self.stages k i → q ∈ self.stages (k + 1) i
• app_mem (k : ℕ) : (Pattern.app sigma fun (i : Fin (S.arity sigma)) => conj (self.stages k i)) ∈ ↑Gamma
• decide (k : ℕ) (i : Fin (S.arity sigma)) : enum k ∈ self.stages (k + 1) i ∨ (enum k).nt ∈ self.stages (k + 1) i
• witness (k : ℕ) (i : Fin (S.arity sigma)) (x : ℕ) (p : Pattern S ℕ) : enum k = Pattern.ex x p → ∃ y ∉ p.allVars, (Pattern.ex x p).imp (Pattern.captureAvoidingSubst x y p) ∈ self.stages (k + 1) i

Simultaneous fresh tuples for Lemma 80

def MatchingLogic.Pattern.tupleAllVars {S : Signature} {n : ℕ} (p : Pattern S ℕ) (Phi : Fin n → Pattern S ℕ) : Finset ℕ

A finite bound containing every raw variable (free or bound) of the existential body and of all finite-stage component conjunctions.

Equations

• p.tupleAllVars Phi = p.allVars ∪ Finset.univ.biUnion fun (i : Fin n) => (Phi i).allVars

def MatchingLogic.Pattern.tupleFreshBase {S : Signature} {n : ℕ} (p : Pattern S ℕ) (Phi : Fin n → Pattern S ℕ) : ℕ

An upper bound on all variable indices in a pattern and its tuple of parameters.

Equations

• p.tupleFreshBase Phi = (insert 0 (p.tupleAllVars Phi)).max' ⋯

def MatchingLogic.Pattern.freshTuple {S : Signature} {n : ℕ} (p : Pattern S ℕ) (Phi : Fin n → Pattern S ℕ) : Fin n → ℕ

The source's tuple of pairwise distinct fresh variables, constructed from a single finite support bound. The stronger allVars freshness makes the later raw-syntax alpha bridge possible.

Equations

• p.freshTuple Phi i = p.tupleFreshBase Phi + 1 + ↑i

theorem MatchingLogic.Pattern.freshTuple_injective {S : Signature} {n : ℕ} (p : Pattern S ℕ) (Phi : Fin n → Pattern S ℕ) : Function.Injective (p.freshTuple Phi)

theorem MatchingLogic.Pattern.freshTuple_not_mem_body_allVars {S : Signature} {n : ℕ} (p : Pattern S ℕ) (Phi : Fin n → Pattern S ℕ) (i : Fin n) : p.freshTuple Phi i ∉ p.allVars

theorem MatchingLogic.Pattern.freshTuple_not_mem_component_allVars {S : Signature} {n : ℕ} (p : Pattern S ℕ) (Phi : Fin n → Pattern S ℕ) (i j : Fin n) : p.freshTuple Phi i ∉ (Phi j).allVars

theorem MatchingLogic.Pattern.freshTuple_not_mem_body_FV {S : Signature} {n : ℕ} (p : Pattern S ℕ) (Phi : Fin n → Pattern S ℕ) (i : Fin n) : p.freshTuple Phi i ∉ FV p

theorem MatchingLogic.Pattern.freshTuple_not_mem_component_FV {S : Signature} {n : ℕ} (p : Pattern S ℕ) (Phi : Fin n → Pattern S ℕ) (i j : Fin n) : p.freshTuple Phi i ∉ FV (Phi j)

def MatchingLogic.NaryStageSystem.limit {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (i : Fin (S.arity sigma)) : Set (Pattern S ℕ)

The component theory at the limit of the finite construction.

Equations

• T.limit i = {q : MatchingLogic.Pattern S ℕ | ∃ (k : ℕ), q ∈ T.stages k i}

theorem MatchingLogic.NaryStageSystem.stage_mono {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) {k l : ℕ} (hkl : k ≤ l) (i : Fin (S.arity sigma)) {q : Pattern S ℕ} (hq : q ∈ T.stages k i) : q ∈ T.stages l i

theorem MatchingLogic.NaryStageSystem.stage_locConsistent {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (k : ℕ) (i : Fin (S.arity sigma)) : LocConsistent {q : Pattern S ℕ | q ∈ T.stages k i}

Condition (4) makes every finite stage locally consistent. This is the source's framing-to-bottom argument, factored through the singleton result in CanonicalCore.

theorem MatchingLogic.NaryStageSystem.limit_locConsistent {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (i : Fin (S.arity sigma)) : LocConsistent (T.limit i)

theorem MatchingLogic.NaryStageSystem.limit_freshWitnessed {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (henum : Function.Surjective enum) (i : Fin (S.arity sigma)) : FreshWitnessed (T.limit i)

theorem MatchingLogic.NaryStageSystem.limit_witnessed {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (henum : Function.Surjective enum) (i : Fin (S.arity sigma)) : Witnessed (T.limit i)

theorem MatchingLogic.NaryStageSystem.limit_isMCS {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (henum : Function.Surjective enum) (i : Fin (S.arity sigma)) : IsMCS (T.limit i)

theorem MatchingLogic.NaryStageSystem.limit_contains_base {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (i : Fin (S.arity sigma)) : phi i ∈ T.limit i

theorem MatchingLogic.NaryStageSystem.root_mem_canonicalInterp {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (henum : Function.Surjective enum) : Gamma ∈ canonicalInterp sigma fun (i : Fin (S.arity sigma)) => ⟨T.limit i, ⋯⟩

The joint invariant implies the universal membership condition of the canonical interpretation.

theorem MatchingLogic.NaryStageSystem.canonicalExistence_of_stageSystem {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} {enum : ℕ → Pattern S ℕ} (T : NaryStageSystem sigma Gamma phi enum) (henum : Function.Surjective enum) : ∃ (components : Fin (S.arity sigma) → CanonicalCarrier S), (∀ (i : Fin (S.arity sigma)), phi i ∈ ↑(components i)) ∧ Gamma ∈ canonicalInterp sigma components

Once the paper's simultaneous finite-stage invariant has been built, its limit gives exactly the component worlds required by Theorem 73.

theorem MatchingLogic.canonicalExistence_zero {S : Signature} {sigma : S.Sym} {Gamma : CanonicalCarrier S} {phi : Fin (S.arity sigma) → Pattern S ℕ} (harity : S.arity sigma = 0) (happ : Pattern.app sigma phi ∈ ↑Gamma) : ∃ (components : Fin (S.arity sigma) → CanonicalCarrier S), (∀ (i : Fin (S.arity sigma)), phi i ∈ ↑(components i)) ∧ Gamma ∈ canonicalInterp sigma components

The arity-zero case of the canonical Existence Lemma. It is stated separately because the tuple of component worlds is genuinely empty, and the universal clause in canonicalInterp reduces exactly to membership of the constant application in the output MCS.