MatchingLogic.EntryIII.LocalTheory

@[instance_reducible]

noncomputable def MatchingLogic.instDecidableEqPatternLocalTheory {S : Signature} {Var : Type} : DecidableEq (Pattern S Var)

Local decidable equality used for finite local theories.

Equations

• MatchingLogic.instDecidableEqPatternLocalTheory = Classical.decEq (MatchingLogic.Pattern S Var)

theorem MatchingLogic.Provable.imp_refl {S : Signature} {Var : Type} [DecidableEq Var] (Gamma : Set (Pattern S Var)) (phi : Pattern S Var) : Provable Gamma (phi.imp phi)

Reflexivity of implication.

theorem MatchingLogic.Provable.imp_trans {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi psi chi : Pattern S Var} (h1 : Provable Gamma (phi.imp psi)) (h2 : Provable Gamma (psi.imp chi)) : Provable Gamma (phi.imp chi)

Transitivity of implication.

theorem MatchingLogic.Provable.imp_of {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi psi : Pattern S Var} (h : Provable Gamma phi) : Provable Gamma (psi.imp phi)

A theorem remains derivable under an arbitrary antecedent.

theorem MatchingLogic.Provable.and_elim_left {S : Signature} {Var : Type} [DecidableEq Var] (Gamma : Set (Pattern S Var)) (phi psi : Pattern S Var) : Provable Gamma ((phi.and psi).imp phi)

Left conjunction elimination.

theorem MatchingLogic.Provable.and_elim_right {S : Signature} {Var : Type} [DecidableEq Var] (Gamma : Set (Pattern S Var)) (phi psi : Pattern S Var) : Provable Gamma ((phi.and psi).imp psi)

Right conjunction elimination.

theorem MatchingLogic.Provable.or_intro_left {S : Signature} {Var : Type} [DecidableEq Var] (Gamma : Set (Pattern S Var)) (phi psi : Pattern S Var) : Provable Gamma (phi.imp (phi.or psi))

Left disjunction introduction.

theorem MatchingLogic.Provable.or_intro_right {S : Signature} {Var : Type} [DecidableEq Var] (Gamma : Set (Pattern S Var)) (phi psi : Pattern S Var) : Provable Gamma (psi.imp (phi.or psi))

Right disjunction introduction.

theorem MatchingLogic.Provable.imp_and {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {alpha beta gamma : Pattern S Var} (h1 : Provable Gamma (alpha.imp beta)) (h2 : Provable Gamma (alpha.imp gamma)) : Provable Gamma (alpha.imp (beta.and gamma))

Combine two consequences with the same antecedent.

Definition 67: finite-premise local derivability

def MatchingLogic.LocProvable {S : Signature} {Var : Type} [DecidableEq Var] (Gamma : Set (Pattern S Var)) (phi : Pattern S Var) : Prop

Γ ⊢loc φ: a finite list of premises from Γ has a theorem implication to φ. Lists, rather than finite sets, are the pinned representation of the finite conjunction and make its bracketing explicit.

Equations

• MatchingLogic.LocProvable Gamma phi = ∃ (l : List (MatchingLogic.Pattern S Var)), (∀ delta ∈ l, delta ∈ Gamma) ∧ MatchingLogic.Provable ∅ ((MatchingLogic.conj l).imp phi)

def MatchingLogic.LocConsistent {S : Signature} {Var : Type} [DecidableEq Var] (Gamma : Set (Pattern S Var)) : Prop

Definition 68: local consistency.

Equations

• MatchingLogic.LocConsistent Gamma = ¬MatchingLogic.LocProvable Gamma MatchingLogic.Pattern.bot

def MatchingLogic.IsMCS {S : Signature} {Var : Type} [DecidableEq Var] (Gamma : Set (Pattern S Var)) : Prop

Definition 68: a locally consistent set with no locally consistent strict extension.

Equations

• MatchingLogic.IsMCS Gamma = (MatchingLogic.LocConsistent Gamma ∧ ∀ {Delta : Set (MatchingLogic.Pattern S Var)}, Gamma ⊂ Delta → ¬MatchingLogic.LocConsistent Delta)

theorem MatchingLogic.LocProvable.mono {S : Signature} {Var : Type} [DecidableEq Var] {Gamma Delta : Set (Pattern S Var)} {phi : Pattern S Var} (hGD : Gamma ⊆ Delta) (h : LocProvable Gamma phi) : LocProvable Delta phi

theorem MatchingLogic.LocProvable.of_mem {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi : Pattern S Var} (h : phi ∈ Gamma) : LocProvable Gamma phi

theorem MatchingLogic.LocProvable.of_provable {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi : Pattern S Var} (h : Provable ∅ phi) : LocProvable Gamma phi

theorem MatchingLogic.LocProvable.mp {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi psi : Pattern S Var} (hphi : LocProvable Gamma phi) (himp : LocProvable Gamma (phi.imp psi)) : LocProvable Gamma psi

theorem MatchingLogic.LocProvable.and_intro {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi psi : Pattern S Var} (hphi : LocProvable Gamma phi) (hpsi : LocProvable Gamma psi) : LocProvable Gamma (phi.and psi)

theorem MatchingLogic.LocProvable.deduction_insert {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi psi : Pattern S Var} (h : LocProvable (insert phi Gamma) psi) : LocProvable Gamma (phi.imp psi)

A single added local premise can be discharged inside the finite-premise definition. This is propositional only; it does not use the global deduction theorem, which would be unsound for unrestricted quantifier generalisation.

Proposition 69: maximal-consistent-set closure

theorem MatchingLogic.IsMCS.mem_iff_locProvable {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi : Pattern S Var} (hM : IsMCS Gamma) : phi ∈ Gamma ↔ LocProvable Gamma phi

Proposition 69(1): membership is exactly local derivability.

theorem MatchingLogic.IsMCS.neg_mem_iff_not_mem {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi : Pattern S Var} (hM : IsMCS Gamma) : phi.nt ∈ Gamma ↔ phi ∉ Gamma

Proposition 69(2): an MCS contains precisely one of a pattern and its negation.

theorem MatchingLogic.IsMCS.and_mem_iff {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi psi : Pattern S Var} (hM : IsMCS Gamma) : phi.and psi ∈ Gamma ↔ phi ∈ Gamma ∧ psi ∈ Gamma

Proposition 69(3), binary case.

theorem MatchingLogic.IsMCS.conj_mem_iff {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} (hM : IsMCS Gamma) (l : List (Pattern S Var)) : conj l ∈ Gamma ↔ ∀ phi ∈ l, phi ∈ Gamma

Proposition 69(3), for the repository's finite-list conjunction.

theorem MatchingLogic.IsMCS.or_mem_iff {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi psi : Pattern S Var} (hM : IsMCS Gamma) : phi.or psi ∈ Gamma ↔ phi ∈ Gamma ∨ psi ∈ Gamma

Proposition 69(4), binary case.

theorem MatchingLogic.IsMCS.mp_mem {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} {phi psi : Pattern S Var} (hM : IsMCS Gamma) (hphi : phi ∈ Gamma) (himp : phi.imp psi ∈ Gamma) : psi ∈ Gamma

Proposition 69(5).