internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
this : 𝓓 ⊬! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
⊢ ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
Tactic:
intro r hr
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
⊢ r ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
⊢ r ∈ t.tableau.1
Tactic:
have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
⊢ r ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
⊢ r ∈ t.tableau.1
Tactic:
have := by simpa using hΓ r hr₁;
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
this : r = p ∨ r ∈ t.tableau.1
⊢ r ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
this : r = p ∨ r ∈ t.tableau.1
⊢ r ∈ t.tableau.1
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
⊢ ?m.615290
Tactic:
simpa using hΓ r hr₁
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ 𝓓 ⊢! (p ⟶ Δ.disj') ⟶ p ⟶ q
Tactic:
apply deduct'!
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ [p ⟶ Δ.disj'] ⊢[𝓓]! p ⟶ q
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ [p ⟶ Δ.disj'] ⊢[𝓓]! p ⟶ q
Tactic:
apply deduct!
Proof state after:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Tactic:
have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp)
Proof state after:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Tactic:
have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this
Proof state after:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Tactic:
exact disj_allsame'! (by simpa using hΔ) this
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ p ∈ [p, p ⟶ Δ.disj']
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
⊢ p ⟶ Δ.disj' ∈ [p, p ⟶ Δ.disj']
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj'
⊢ ∀ q_1 ∈ Δ, q_1 = q
Tactic:
simpa using hΔ
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ 𝓓 ⊬! (List.remove p Γ).conj' ⟶ p ⟶ q
Tactic:
simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all))
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
⊢ ?m.706390
Tactic:
simpa [Set.insert_subset_iff] using lindenbaum this
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 → t ⊧ p ⟶ q
Tactic:
simp [Satisfies.imp_def]
Proof state after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 →
    ∀ {w' : (CanonicalModel 𝓓).Frame.World},
      t.tableau.1 ⊆ w'.tableau.1 → Satisfies (CanonicalModel 𝓓) w' p → Satisfies (CanonicalModel 𝓓) w' q
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 →
    ∀ {w' : (CanonicalModel 𝓓).Frame.World},
      t.tableau.1 ⊆ w'.tableau.1 → Satisfies (CanonicalModel 𝓓) w' p → Satisfies (CanonicalModel 𝓓) w' q
Tactic:
intro h t' htt' hp
Proof state after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : Satisfies (CanonicalModel 𝓓) t' p
⊢ Satisfies (CanonicalModel 𝓓) t' q
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : Satisfies (CanonicalModel 𝓓) t' p
⊢ Satisfies (CanonicalModel 𝓓) t' q
Tactic:
replace hp := ihp.mp hp
Proof state after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q
Tactic:
have hpq := htt' h
Proof state after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q
Tactic:
apply ihq.mpr
Proof state after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ q ∈ t'.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ q ∈ t'.tableau.1
Tactic:
apply t'.not_mem₂_iff_mem₁.mp
Proof state after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ q ∉ t'.tableau.2
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ q ∉ t'.tableau.2
Tactic:
exact not_mem₂
  (by simp_all)
  (show 𝓓 ⊢! [p, p ⟶ q].conj' ⟶ q by
    simp;
    apply andImplyIffImplyImply'!.mpr;
    apply deduct'!;
    apply deduct!;
    exact by_axm! ⨀ (by_axm! (p := p));
  )
Proof state after:
no goals