def Saturated : Finset Formula → Prop

Equations

• Saturated x✝ = ∀ (P Q : Formula), (~~P ∈ x✝ → P ∈ x✝) ∧ (P⋀Q ∈ x✝ → P ∈ x✝ ∧ Q ∈ x✝) ∧ (~(P⋀Q) ∈ x✝ → ~P ∈ x✝ ∨ ~Q ∈ x✝)

def ModelGraph (Worlds : Set (Finset Formula)) : Type

Equations

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

theorem truthLemma {Worlds : Set (Finset Formula)} (MG : ModelGraph Worlds) (X : ↑Worlds) (P : Formula) : P ∈ ↑X → Evaluate (↑MG, X) P