internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
case pos
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
. left; assumption;
Proof state after:
case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
. right;
  intro w' hww';
  rw [←(hExt hww')];
  assumption;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
case pos
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
left
Proof state after:
case pos.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
case pos.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
right
Proof state after:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
intro w' hww'
Proof state after:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w' p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w' p
Tactic:
rw [←(hExt hww')]
Proof state after:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.verum
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ ⊤
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } ⊤
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.verum
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } ⊤
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } ⊤
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.verum
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } ⊤
Tactic:
apply ValidOnModel.verum
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ p ⋏ q ⟶ p
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⋏ q ⟶ p)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⋏ q ⟶ p)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⋏ q ⟶ p)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⋏ q ⟶ p)
Tactic:
apply ValidOnModel.conj₁
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ p ⋏ q ⟶ q
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⋏ q ⟶ q)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⋏ q ⟶ q)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⋏ q ⟶ q)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⋏ q ⟶ q)
Tactic:
apply ValidOnModel.conj₂
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ p ⟶ q ⟶ p ⋏ q
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q ⟶ p ⋏ q)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q ⟶ p ⋏ q)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⟶ q ⟶ p ⋏ q)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.conj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⟶ q ⟶ p ⋏ q)
Tactic:
apply ValidOnModel.conj₃
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ p ⟶ p ⋎ q
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ p ⋎ q)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ p ⋎ q)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⟶ p ⋎ q)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⟶ p ⋎ q)
Tactic:
apply ValidOnModel.disj₁
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ q ⟶ p ⋎ q
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (q ⟶ p ⋎ q)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (q ⟶ p ⋎ q)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (q ⟶ p ⋎ q)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (q ⟶ p ⋎ q)
Tactic:
apply ValidOnModel.disj₂
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ (p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.disj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)
Tactic:
apply ValidOnModel.disj₃
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.imply₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ p ⟶ q ⟶ p
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q ⟶ p)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.imply₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q ⟶ p)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⟶ q ⟶ p)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.imply₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (p ⟶ q ⟶ p)
Tactic:
apply ValidOnModel.imply₁
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.imply₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ (p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } ((p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.imply₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } ((p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } ((p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.imply₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } ((p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r)
Tactic:
apply ValidOnModel.imply₂
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.mdp
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq : F ⊧ p ⟶ q
hp : F ⊧ p
⊢ F ⊧ q
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q)
hp :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } p
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } q
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.mdp
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q)
hp :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } p
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } q
Tactic:
intros V hV
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q)
hp :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } p
V : Valuation F.World α
hV : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V, hereditary := hV } q
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.mdp
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q)
hp :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } p
V : Valuation F.World α
hV : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V, hereditary := hV } q
Tactic:
exact ValidOnModel.mdp (hpq V hV) (hp V hV)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.efq
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ F ⊧ Axioms.EFQ p
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (Axioms.EFQ p)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.efq
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (Axioms.EFQ p)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (Axioms.EFQ p)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.efq
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (Axioms.EFQ p)
Tactic:
apply ValidOnModel.efq
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.lem
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hExt : Extensive F.Rel
⊢ F ⊧ Axioms.LEM p
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hExt : Extensive F.Rel
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (Axioms.LEM p)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.lem
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hExt : Extensive F.Rel
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (Axioms.LEM p)
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hExt : Extensive F.Rel
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (Axioms.LEM p)
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.lem
Proof state before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hExt : Extensive F.Rel
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } (Axioms.LEM p)
Tactic:
exact ValidOnModel.lem hExt
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.validOnAxiomSetFrameClass_axiom
Proof state before:
α : Type u_1
inst✝ : Inhabited α
Ax : AxiomSet α
p : Formula α
h : p ∈ Ax
⊢ 𝔽(Ax) ⊧ p
Tactic:
intro F hF
Proof state after:
α : Type u_1
inst✝ : Inhabited α
Ax : AxiomSet α
p : Formula α
h : p ∈ Ax
F : Frame' α
hF : F ∈ 𝔽(Ax)
⊢ F ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.validOnAxiomSetFrameClass_axiom
Proof state before:
α : Type u_1
inst✝ : Inhabited α
Ax : AxiomSet α
p : Formula α
h : p ∈ Ax
F : Frame' α
hF : F ∈ 𝔽(Ax)
⊢ F ⊧ p
Tactic:
exact hF.realize h
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.iff_definability_memAxiomSetFrameClass
Proof state before:
α : Type u_1
inst✝ : Inhabited α
Ax : AxiomSet α
P : FrameProperty
definability : Definability Ax P
⊢ ∀ {F : Frame' α}, F ∈ 𝔽(Ax) ↔ P F
Tactic:
apply Definability.defines
Proof state after:
no goals