internlm/Lean-Github huggingface dataset:
Theorem: truthLemma
Proof state before:
case right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
⊢ minus (·pp) X ∧ oh (·pp) X
Tactic:
constructor
Proof state after:
case right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
⊢ minus (·pp) X

case right.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
⊢ oh (·pp) X
Theorem: truthLemma
Proof state before:
case left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
⊢ plus (·pp) X
Tactic:
intro P_in_X
Proof state after:
case left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
P_in_X : (·pp) ∈ ↑X
⊢ Evaluate (M, X) (·pp)
Theorem: truthLemma
Proof state before:
case left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
P_in_X : (·pp) ∈ ↑X
⊢ Evaluate (M, X) (·pp)
Tactic:
unfold Evaluate
Proof state after:
case left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
P_in_X : (·pp) ∈ ↑X
⊢ M.val X pp
Theorem: truthLemma
Proof state before:
case left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
P_in_X : (·pp) ∈ ↑X
⊢ M.val X pp
Tactic:
rw [ii X pp] at P_in_X
Proof state after:
case left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
P_in_X : M.val X pp
⊢ M.val X pp
Theorem: truthLemma
Proof state before:
case left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
P_in_X : M.val X pp
⊢ M.val X pp
Tactic:
exact P_in_X
Proof state after:
no goals
Theorem: truthLemma
Proof state before:
case right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
⊢ minus (·pp) X
Tactic:
intro notP_in_X
Proof state after:
case right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬Evaluate (M, X) (·pp)
Theorem: truthLemma
Proof state before:
case right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬Evaluate (M, X) (·pp)
Tactic:
unfold Evaluate
Proof state after:
case right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬M.val X pp
Theorem: truthLemma
Proof state before:
case right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬M.val X pp
Tactic:
rw [← ii X pp]
Proof state after:
case right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
⊢ (·pp) ∉ ↑X
Theorem: truthLemma
Proof state before:
case right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
rcases i X with ⟨_, _, P_in_then_notP_not_in⟩
Proof state after:
case right.left.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : Saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Theorem: truthLemma
Proof state before:
case right.left.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : Saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
specialize P_in_then_notP_not_in pp
Proof state after:
case right.left.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : Saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Theorem: truthLemma
Proof state before:
case right.left.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : Saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
tauto
Proof state after:
no goals
Theorem: truthLemma
Proof state before:
case right.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
⊢ oh (·pp) X
Tactic:
intro boxPp_in_X Y X_rel_Y
Proof state after:
case right.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
pp : Char
X : ↑Worlds
boxPp_in_X : (□·pp) ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
⊢ (·pp) ∈ ↑Y
Theorem: truthLemma
Proof state before:
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
⊢ plus (~P) X ∧ minus (~P) X ∧ oh (~P) X
Tactic:
rcases IH X with ⟨plus_IH, minus_IH, _⟩
Proof state after:
case intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
plus_IH : plus P X
minus_IH : minus P X
right✝ : oh P X
⊢ plus (~P) X ∧ minus (~P) X ∧ oh (~P) X
Theorem: truthLemma
Proof state before:
case intro.intro.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
plus_IH : plus P X
minus_IH : minus P X
right✝ : oh P X
⊢ minus (~P) X ∧ oh (~P) X
Tactic:
constructor
Proof state after:
case intro.intro.right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
plus_IH : plus P X
minus_IH : minus P X
right✝ : oh P X
⊢ minus (~P) X

case intro.intro.right.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
plus_IH : plus P X
minus_IH : minus P X
right✝ : oh P X
⊢ oh (~P) X