def combinedModel {β : Type} (collection : β → (W : Type) × KripkeModel W × W) (newVal : Char → Prop) : KripkeModel (Unit ⊕ (k : β) × (collection k).fst) × (Unit ⊕ (k : β) × (collection k).fst)

Combine a collection of pointed models with one new world using the given valuation.

Equations

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

theorem combMo_preserves_truth_at_oldWOrld {β : Type} (collection : β → (W : Type) × KripkeModel W × W) (newVal : Char → Prop) (f : Formula) (R : β) (oldWorld : (collection R).fst) : Evaluate ((combinedModel collection newVal).1, Sum.inr ⟨R, oldWorld⟩) f ↔ Evaluate ((collection R).snd.1, oldWorld) f

The combined model preserves all truths at the old worlds.

theorem combMo_sat_LR {L R : Finset Formula} {β : Set Formula} {beta_def : β = {F : Formula | f_in_TNode (~(□F)) (L, R)}} (simple_LR : Simple (L, R)) (not_closed_LR : ¬Closed (L ∪ R)) (collection : ↑β → (W : Type) × KripkeModel W × W) (all_pro_sat : ∀ (F : ↑β), ∀ f ∈ projection (L ∪ R) ∪ {~↑F}, Evaluate ((collection F).snd.1, (collection F).snd.2) f) (f : Formula) : f_in_TNode f (L, R) → Evaluate ((combinedModel collection fun (c : Char) => (·c) ∈ L ∪ R).1, (combinedModel collection fun (c : Char) => (·c) ∈ L ∪ R).2) f

The combined model for X satisfies X.

theorem Lemma1_simple_sat_iff_all_projections_sat {LR : TNode} : Simple LR → (HasSat.Satisfiable LR ↔ ¬Closed (LR.1 ∪ LR.2) ∧ ∀ (F : Formula), f_in_TNode (~(□F)) LR → HasSat.Satisfiable (projection (LR.1 ∪ LR.2) ∪ {~F}))

Lemma 1 (page 16) A simple set of formulas X is satisfiable if and only if it is not closed and for all ¬[A]R ∈ X also XA; ¬R is satisfiable.

theorem localRuleSoundness {W : Type} {Lcond Rcond : Finset Formula} {ress : List SubPair} (M : KripkeModel W) (w : W) (rule : LocalRule (Lcond, Rcond) ress) (Δ : Finset Formula) : (M, w)⊨Δ ∪ Lcond ∪ Rcond → ∃ res ∈ ress, (M, w)⊨Δ ∪ res.1 ∪ res.2

theorem ruleImpliesChildSat {C : List TNode} {LR : TNode} {ruleApp : LocalRuleApp LR C} : HasSat.Satisfiable LR → ∃ c ∈ C, HasSat.Satisfiable c

theorem oneSidedRule_implies_child_sat_L {L R : Finset Formula} {C : List TNode} {fst✝ : Finset Formula} {a✝ : List (Finset Formula)} {rule : LocalRule (fst✝, ∅) (List.map (fun (res : Finset Formula) => (res, ∅)) a✝)} {hC : C = applyLocalRule rule (L, R)} {preproof : fst✝ ⊆ L ∧ ∅ ⊆ R} {orule : OneSidedLocalRule fst✝ a✝} {X : Finset Formula} {ruleApp : LocalRuleApp (L, R) C} (def_ruleA : ruleApp = LocalRuleApp.mk (List.map (fun (res : Finset Formula) => (res, ∅)) a✝) fst✝ ∅ rule preproof) (rule_is_left : rule = LocalRule.oneSidedL orule) : HasSat.Satisfiable (L ∪ X) → ∃ c ∈ C.attach, HasSat.Satisfiable ((↑c).1 ∪ X)

theorem oneSidedRule_implies_child_sat_R {L R : Finset Formula} {C : List TNode} {snd✝ : Finset Formula} {a✝ : List (Finset Formula)} {rule : LocalRule (∅, snd✝) (List.map (fun (res : Finset Formula) => (∅, res)) a✝)} {hC : C = applyLocalRule rule (L, R)} {preproof : ∅ ⊆ L ∧ snd✝ ⊆ R} {orule : OneSidedLocalRule snd✝ a✝} {X : Finset Formula} {ruleApp : LocalRuleApp (L, R) C} (def_ruleA : ruleApp = LocalRuleApp.mk (List.map (fun (res : Finset Formula) => (∅, res)) a✝) ∅ snd✝ rule preproof) (rule_is_right : rule = LocalRule.oneSidedR orule) : HasSat.Satisfiable (R ∪ X) → ∃ c ∈ C.attach, HasSat.Satisfiable ((↑c).2 ∪ X)

theorem atmSoundness {LR : TNode} {f : Formula} (not_box_f_in_LR : f_in_TNode (~(□f)) LR) : HasSat.Satisfiable LR → HasSat.Satisfiable (projection (LR.1 ∪ LR.2) ∪ {~f})

The critical rule is sound and preserves satisfiability "downwards". NOTE: This is stronger than Lemma 1, but we do not need.

@[irreducible]

theorem localTableauAndEndNodesUnsatThenNotSat (LR : TNode) {ltLR : LocalTableau LR} : (∀ Y ∈ endNodesOf ⟨LR, ltLR⟩, ¬HasSat.Satisfiable Y) → ¬HasSat.Satisfiable LR

theorem tableauThenNotSat (X : TNode) : ClosedTableau X → ¬HasSat.Satisfiable X

theorem correctness (LR : TNode) : HasSat.Satisfiable LR → Consistent LR

Theorem 2, page 30

theorem soundTableau (φ : Formula) : Provable φ → ¬HasSat.Satisfiable {~φ}

theorem soundness (φ : Formula) : Provable φ → Tautology φ