structure KripkeModel (W : Type) : Type

• val : W → Char → Prop
• Rel : W → W → Prop

def Evaluate {W : Type} : KripkeModel W × W → Formula → Prop

Equations

• Evaluate (fst, snd) Formula.bottom = False
• Evaluate (M, w) (·p) = M.val w p
• Evaluate (M, w) (~φ) = ¬Evaluate (M, w) φ
• Evaluate (M, w) (φ⋀ψ) = (Evaluate (M, w) φ ∧ Evaluate (M, w) ψ)
• Evaluate (M, w) (□φ) = ∀ (v : W), M.Rel w v → Evaluate (M, v) φ

@[simp]

theorem evalDis {W : Type} {M : KripkeModel W} {f g : Formula} {w : W} : Evaluate (M, w) (f⋁g) ↔ Evaluate (M, w) f ∨ Evaluate (M, w) g

def Tautology (φ : Formula) : Prop

Equations

• Tautology φ = ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) φ

def Contradiction (φ : Formula) : Prop

Equations

• Contradiction φ = ∀ (W : Type) (M : KripkeModel W) (w : W), ¬Evaluate (M, w) φ

class HasSat (α : Type) : Type

• Satisfiable : α → Prop

instance formHasSat : HasSat Formula

Equations

• formHasSat = { Satisfiable := fun (ϕ : Formula) => ∃ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) ϕ }

instance setHasSat : HasSat (Finset Formula)

Equations

• setHasSat = { Satisfiable := fun (X : Finset Formula) => ∃ (W : Type) (M : KripkeModel W) (w : W), ∀ φ ∈ X, Evaluate (M, w) φ }

theorem notsatisfnotThenTaut (φ : Formula) : ¬HasSat.Satisfiable (~φ) → Tautology φ

theorem subsetSat {X Y : Finset Formula} : HasSat.Satisfiable X → Y ⊆ X → HasSat.Satisfiable Y

@[simp]

theorem singletonSat_iff_sat (φ : Formula) : HasSat.Satisfiable {φ} ↔ HasSat.Satisfiable φ

theorem tautImp_iff_comboNotUnsat {ϕ ψ : Formula} : Tautology (ϕ↣ψ) ↔ ¬HasSat.Satisfiable {ϕ, ~ψ}

def SemImpliesSets (X Y : Finset Formula) : Prop

Equations

• SemImpliesSets X Y = ∀ (W : Type) (M : KripkeModel W) (w : W), (∀ φ ∈ X, Evaluate (M, w) φ) → ∀ ψ ∈ Y, Evaluate (M, w) ψ

def semEquiv (φ ψ : Formula) : Prop

Equations

• (φ≡ψ) = ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) φ ↔ Evaluate (M, w) ψ

theorem semEquiv.transitive : Transitive semEquiv

class VDash (α β : Type) : Type

• SemImplies : α → β → Prop

instance modelCanSemImplyForm {W : Type} : VDash (KripkeModel W × W) Formula

Equations

• modelCanSemImplyForm = { SemImplies := Evaluate }

instance modelCanSemImplySet {W : Type} : VDash (KripkeModel W × W) (Finset Formula)

Equations

• modelCanSemImplySet = { SemImplies := fun (Mw : KripkeModel W × W) (X : Finset Formula) => ∀ f ∈ X, Evaluate Mw f }

instance setCanSemImplySet : VDash (Finset Formula) (Finset Formula)

Equations

• setCanSemImplySet = { SemImplies := SemImpliesSets }

instance setCanSemImplyForm : VDash (Finset Formula) Formula

Equations

• setCanSemImplyForm = { SemImplies := fun (X : Finset Formula) (ψ : Formula) => SemImpliesSets X {ψ} }

instance formCanSemImplySet : VDash Formula (Finset Formula)

Equations

• formCanSemImplySet = { SemImplies := fun (φ : Formula) (X : Finset Formula) => SemImpliesSets {φ} X }

instance formCanSemImplyForm : VDash Formula Formula

Equations

• formCanSemImplyForm = { SemImplies := fun (φ ψ : Formula) => SemImpliesSets {φ} {ψ} }

def «term_⊨_» : Lean.TrailingParserDescr

Equations

• «term_⊨_» = Lean.ParserDescr.trailingNode `«term_⊨_» 40 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊨") (Lean.ParserDescr.cat `term 41))

def «term_≡_» : Lean.TrailingParserDescr

Equations

• «term_≡_» = Lean.ParserDescr.trailingNode `«term_≡_» 40 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "≡") (Lean.ParserDescr.cat `term 41))

def «term_⊭_» : Lean.TrailingParserDescr

Equations

• «term_⊭_» = Lean.ParserDescr.trailingNode `«term_⊭_» 40 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊭") (Lean.ParserDescr.cat `term 41))

theorem forms_to_sets {φ ψ : Formula} : φ⊨ψ → {φ}⊨{ψ}

theorem negation_not_cosatisfiable {X : Finset Formula} (φ : Formula) (phi_in : φ ∈ X) (notPhi_in : ~φ ∈ X) : ¬HasSat.Satisfiable X

theorem sat_double_neq_invariant {X : Finset Formula} (φ : Formula) : HasSat.Satisfiable (X ∪ {~~φ}) ↔ HasSat.Satisfiable (X ∪ {φ})