MatchingLogic.EntryIII.MCSAlpha

theorem MatchingLogic.IsMCS.mem_of_provable_empty {S : Signature} {Gamma : Set (Pattern S ℕ)} {p : Pattern S ℕ} (hM : IsMCS Gamma) (h : Provable ∅ p) : p ∈ Gamma

Every empty-theory theorem belongs to every MCS.

theorem MatchingLogic.IsMCS.mem_of_provable_imp {S : Signature} {Gamma : Set (Pattern S ℕ)} {p q : Pattern S ℕ} (hM : IsMCS Gamma) (hp : p ∈ Gamma) (hpq : Provable ∅ (p.imp q)) : q ∈ Gamma

MCS membership transports along an empty-theory implication.

theorem MatchingLogic.IsMCS.imp_mem_of_mono {S : Signature} {Gamma : Set (Pattern S ℕ)} {p p' q q' : Pattern S ℕ} (hM : IsMCS Gamma) (hp : Provable ∅ (p'.imp p)) (hq : Provable ∅ (q.imp q')) (hmem : p.imp q ∈ Gamma) : p'.imp q' ∈ Gamma

Membership transport through implication monotonicity.

theorem MatchingLogic.IsMCS.ex_mem_of_mono {S : Signature} {Gamma : Set (Pattern S ℕ)} {x : ℕ} {p q : Pattern S ℕ} (hM : IsMCS Gamma) (hpq : Provable ∅ (p.imp q)) (hmem : Pattern.ex x p ∈ Gamma) : Pattern.ex x q ∈ Gamma

Membership transport through existential monotonicity.

theorem MatchingLogic.IsMCS.app_mem_of_mono {S : Signature} {Gamma : Set (Pattern S ℕ)} {sigma : S.Sym} {args args' : Fin (S.arity sigma) → Pattern S ℕ} (hM : IsMCS Gamma) (hargs : ∀ (i : Fin (S.arity sigma)), Provable ∅ ((args i).imp (args' i))) (hmem : Pattern.app sigma args ∈ Gamma) : Pattern.app sigma args' ∈ Gamma

Membership transport through pointwise application monotonicity.

theorem MatchingLogic.IsMCS.alphaEq_mem_iff {S : Signature} {Gamma : Set (Pattern S ℕ)} {p q : Pattern S ℕ} (hM : IsMCS Gamma) (halpha : p.AlphaEq q) : p ∈ Gamma ↔ q ∈ Gamma

MCS membership is invariant under the kernel-level alpha-equivalence relation.

theorem MatchingLogic.IsMCS.imp_alphaEq_mem_iff {S : Signature} {Gamma : Set (Pattern S ℕ)} {p p' q q' : Pattern S ℕ} (hM : IsMCS Gamma) (hp : p.AlphaEq p') (hq : q.AlphaEq q') : p.imp q ∈ Gamma ↔ p'.imp q' ∈ Gamma

Alpha-congruent implications have identical MCS membership.

theorem MatchingLogic.IsMCS.ex_alphaEq_mem_iff {S : Signature} {Gamma : Set (Pattern S ℕ)} {x : ℕ} {p q : Pattern S ℕ} (hM : IsMCS Gamma) (h : p.AlphaEq q) : Pattern.ex x p ∈ Gamma ↔ Pattern.ex x q ∈ Gamma

Alpha-congruent existential bodies have identical MCS membership.

theorem MatchingLogic.IsMCS.app_alphaEq_mem_iff {S : Signature} {Gamma : Set (Pattern S ℕ)} {sigma : S.Sym} {args args' : Fin (S.arity sigma) → Pattern S ℕ} (hM : IsMCS Gamma) (h : ∀ (i : Fin (S.arity sigma)), (args i).AlphaEq (args' i)) : Pattern.app sigma args ∈ Gamma ↔ Pattern.app sigma args' ∈ Gamma

Pointwise alpha-congruent application arguments have identical MCS membership.

theorem MatchingLogic.IsMCS.bot_not_mem {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) : Pattern.bot ∉ Gamma

Bottom belongs to no maximal locally consistent set.

theorem MatchingLogic.IsMCS.imp_mem_iff {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) (p q : Pattern S ℕ) : p.imp q ∈ Gamma ↔ p ∉ Gamma ∨ q ∈ Gamma

Boolean membership clause for primitive implication.