(Big) Disjunction and Conjunction

Here we define ⋀ and ⋁ on formulas and seveal helper lemmas.

Conjunction

def Con : List Formula → Formula

Equations

• Con [] = ⊤
• Con [f] = f
• Con (f :: rest) = f⋀Con rest

@[simp]

theorem conempty : Con ∅ = ⊤

@[simp]

theorem consingle {f : Formula} : Con [f] = f

theorem listEq_to_conEq {l1 l2 : List Formula} : l1 = l2 → Con l1 = Con l2

theorem conEvalHT {X : List Formula} {f : Formula} {W : Type} {M : KripkeModel W} {w : W} : evaluate M w (Con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (Con X)

theorem conEval {W : Type} {M : KripkeModel W} {X : List Formula} {w : W} : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f

theorem in_voc_con (n : ℕ ⊕ ℕ) (L : List Formula) : n ∈ (Con L).voc ↔ ∃ φ ∈ L, n ∈ φ.voc

Vocabulary of Conjunction

Disjunction

def dis : List Formula → Formula

Equations

• dis [] = ⊥
• dis [f] = f
• dis (f :: rest) = f⋁dis rest

@[simp]

theorem disempty : dis ∅ = ⊥

@[simp]

theorem dissingle {f : Formula} : dis [f] = f

theorem listEq_to_disEq {l1 l2 : List Formula} : l1 = l2 → dis l1 = dis l2

theorem disEvalHT {X : List Formula} {f : Formula} {W : Type} {M : KripkeModel W} {w : W} : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)

theorem disEval {W : Type} {M : KripkeModel W} {X : List Formula} {w : W} : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f

theorem in_voc_dis (n : ℕ ⊕ ℕ) (L : List Formula) : n ∈ (dis L).voc ↔ ∃ φ ∈ L, n ∈ φ.voc

Vocabulary of Disjunction

Disjunction of Conjunctions

def discon : List (List Formula) → Formula

Equations

• discon [] = ⊥
• discon [X] = Con X
• discon (X :: rest) = Con X⋁discon rest

@[simp]

theorem disconempty : discon {∅} = ⊤

@[simp]

theorem disconsingle {f : Formula} : discon [[f]] = f

theorem disconEvalHT {X : List Formula} (XS : List (List Formula)) : discon (X :: XS)≡Con X⋁discon XS

theorem disconEval' {W : Type} {M : KripkeModel W} {w : W} {N : ℕ} (XS : List (List Formula)) : XS.length = N → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)

theorem disconEval {W : Type} {M : KripkeModel W} {w : W} (XS : List (List Formula)) : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

theorem disconOr {XS YS : List (List Formula)} : discon (XS ∪ YS)≡discon XS⋁discon YS

Pairwise Union

def pairunionList : List (List Formula) → List (List Formula) → List (List Formula)

Equations

• pairunionList x✝¹ x✝ = (List.map (fun (xl : List Formula) => List.map (fun (yl : List Formula) => xl ++ yl) x✝) x✝¹).flatten

def pairunionFinset : Finset (Finset Formula) → Finset (Finset Formula) → Finset (Finset Formula)

Equations

• pairunionFinset x✝¹ x✝ = x✝¹.biUnion fun (ga : Finset Formula) => x✝.biUnion fun (gb : Finset Formula) => {ga ∪ gb}

class HasUplus (α : Type → Type) : Type

• pairunion : α (α Formula) → α (α Formula) → α (α Formula)

def «term_⊎_» : Lean.TrailingParserDescr

Equations

• «term_⊎_» = Lean.ParserDescr.trailingNode `«term_⊎_» 77 77 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊎") (Lean.ParserDescr.cat `term 78))

instance listHasUplus : HasUplus List

Equations

• listHasUplus = { pairunion := pairunionList }

instance finsetHasUplus : HasUplus Finset

Equations

• finsetHasUplus = { pairunion := pairunionFinset }

theorem disconAnd {XS YS : List (List Formula)} : discon (XS⊎YS)≡discon XS⋀discon YS

theorem union_elem_uplus {XS YS : Finset (Finset Formula)} {X Y : Finset Formula} : X ∈ XS → Y ∈ YS → X ∪ Y ∈ XS⊎YS

theorem mapCon_mapForall {W : Type} {X : List (List Formula × List Program)} (M : KripkeModel W) (w : W) (φ : Formula) (g : List Formula × List Program → Formula → List Formula) : (∃ f ∈ List.map (fun (Fδ : List Formula × List Program) => Con (g Fδ φ)) X, evaluate M w f) ↔ ∃ fs ∈ List.map (fun (Fδ : List Formula × List Program) => g Fδ φ) X, ∀ f ∈ fs, evaluate M w f

Helper for oneSidedLocalRuleTruth, used with g = Yset.