internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ m𝓓 ⊢! □(□(pᵍ ⟶ □(qᵍ ⟶ rᵍ)) ⟶ □(□(pᵍ ⟶ qᵍ) ⟶ □(pᵍ ⟶ rᵍ)))
Tactic:
refine nec! $ imp_trans! (imp_trans! (axiomK'! $ nec! ?b) axiomFour!) $ axiomK'! $ nec! $ imp_trans! (axiomK'! $ nec! imply₂!) axiomK!
Proof state after:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ m𝓓 ⊢! (pᵍ ⟶ □(qᵍ ⟶ rᵍ)) ⟶ pᵍ ⟶ qᵍ ⟶ rᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ m𝓓 ⊢! (pᵍ ⟶ □(qᵍ ⟶ rᵍ)) ⟶ pᵍ ⟶ qᵍ ⟶ rᵍ
Tactic:
apply provable_iff_provable.mpr
Proof state after:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ [] ⊢[m𝓓]! (pᵍ ⟶ □(qᵍ ⟶ rᵍ)) ⟶ pᵍ ⟶ qᵍ ⟶ rᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ [] ⊢[m𝓓]! (pᵍ ⟶ □(qᵍ ⟶ rᵍ)) ⟶ pᵍ ⟶ qᵍ ⟶ rᵍ
Tactic:
apply deduct_iff.mpr
Proof state after:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ [pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ qᵍ ⟶ rᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ [pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ qᵍ ⟶ rᵍ
Tactic:
apply deduct_iff.mpr
Proof state after:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
Tactic:
have : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ := by_axm! (by simp)
Proof state after:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
Tactic:
have : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! (pᵍ ⟶ □(qᵍ ⟶ rᵍ)) := by_axm! (by simp)
Proof state after:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this✝ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ □(qᵍ ⟶ rᵍ)
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this✝ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ □(qᵍ ⟶ rᵍ)
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
Tactic:
have : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! □(qᵍ ⟶ rᵍ) := (by assumption) ⨀ (by assumption)
Proof state after:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this✝¹ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
this✝ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ □(qᵍ ⟶ rᵍ)
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! □(qᵍ ⟶ rᵍ)
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this✝¹ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
this✝ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ □(qᵍ ⟶ rᵍ)
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! □(qᵍ ⟶ rᵍ)
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
Tactic:
exact axiomT'! this
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ pᵍ ∈ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)]
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
⊢ pᵍ ⟶ □(qᵍ ⟶ rᵍ) ∈ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)]
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this✝ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ □(qᵍ ⟶ rᵍ)
⊢ { ctx := [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] } ⊢! ?m.20225 ⟶ □(qᵍ ⟶ rᵍ)
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this✝ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ □(qᵍ ⟶ rᵍ)
⊢ { ctx := [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] } ⊢! pᵍ
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_conj₃
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! (p ⟶ q ⟶ p ⋏ q)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, GoedelTranslation.and_def]
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! □(pᵍ ⟶ □(qᵍ ⟶ pᵍ ⋏ qᵍ))
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_conj₃
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! □(pᵍ ⟶ □(qᵍ ⟶ pᵍ ⋏ qᵍ))
Tactic:
exact nec! $ imp_trans! axiomTc_GTranslate! $ axiomK'! $ nec! $ conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_disj₃
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, GoedelTranslation.or_def]
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! □(□(pᵍ ⟶ rᵍ) ⟶ □(□(qᵍ ⟶ rᵍ) ⟶ □(pᵍ ⋎ qᵍ ⟶ rᵍ)))
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_disj₃
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! □(□(pᵍ ⟶ rᵍ) ⟶ □(□(qᵍ ⟶ rᵍ) ⟶ □(pᵍ ⋎ qᵍ ⟶ rᵍ)))
Tactic:
exact nec! $ imp_trans! axiomFour! $ axiomK'! $ nec! $ imp_trans! (axiomK'! $ nec! $ disj₃!) axiomK!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p
⊢ 𝐒𝟒 ⊢! pᵍ
Tactic:
induction h.some with
| eaxm ih =>
  simp_all only [Set.mem_setOf_eq];
  obtain ⟨p, hp⟩ := ih; subst hp;
  exact nec! efq!;
| mdp hpq hp ihpq ihp =>
  exact axiomT'! $ axiomK''! (by simpa using ihpq ⟨hpq⟩) $ nec! $ ihp ⟨hp⟩;
| verum => apply verum!;
| imply₁ => exact case_imply₁;
| imply₂ => exact case_imply₂;
| conj₁ => simp only [GoedelTranslation.imp_def, GoedelTranslation.and_def]; exact nec! conj₁!;
| conj₂ => simp only [GoedelTranslation.imp_def, GoedelTranslation.and_def]; exact nec! conj₂!;
| conj₃ => exact case_conj₃;
| disj₁ => simp only [GoedelTranslation.imp_def, GoedelTranslation.or_def]; exact nec! disj₁!;
| disj₂ => simp only [GoedelTranslation.imp_def, GoedelTranslation.or_def]; exact nec! disj₂!;
| disj₃ => exact case_disj₃;
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case eaxm
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ : Superintuitionistic.Formula α
ih : p✝ ∈ Ax(𝐈𝐧𝐭)
h : 𝐈𝐧𝐭 ⊢! p✝
⊢ 𝐒𝟒 ⊢! p✝ᵍ
Tactic:
simp_all only [Set.mem_setOf_eq]
Proof state after:
case eaxm
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ : Superintuitionistic.Formula α
ih : ∃ p, Axioms.EFQ p = p✝
h : 𝐈𝐧𝐭 ⊢! p✝
⊢ 𝐒𝟒 ⊢! p✝ᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case eaxm
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ : Superintuitionistic.Formula α
ih : ∃ p, Axioms.EFQ p = p✝
h : 𝐈𝐧𝐭 ⊢! p✝
⊢ 𝐒𝟒 ⊢! p✝ᵍ
Tactic:
obtain ⟨p, hp⟩ := ih
Proof state after:
case eaxm.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝¹ q r p✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝
p : Superintuitionistic.Formula α
hp : Axioms.EFQ p = p✝
⊢ 𝐒𝟒 ⊢! p✝ᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case eaxm.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝¹ q r p✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝
p : Superintuitionistic.Formula α
hp : Axioms.EFQ p = p✝
⊢ 𝐒𝟒 ⊢! p✝ᵍ
Tactic:
subst hp
Proof state after:
case eaxm.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q r p : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! Axioms.EFQ p
⊢ 𝐒𝟒 ⊢! Axioms.EFQ pᵍ
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case eaxm.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q r p : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! Axioms.EFQ p
⊢ 𝐒𝟒 ⊢! Axioms.EFQ pᵍ
Tactic:
exact nec! efq!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case mdp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
hpq : Superintuitionistic.Deduction 𝐈𝐧𝐭 (p✝ ⟶ q✝)
hp : Superintuitionistic.Deduction 𝐈𝐧𝐭 p✝
ihpq : 𝐈𝐧𝐭 ⊢! p✝ ⟶ q✝ → 𝐒𝟒 ⊢! (p✝ ⟶ q✝)ᵍ
ihp : 𝐈𝐧𝐭 ⊢! p✝ → 𝐒𝟒 ⊢! p✝ᵍ
h : 𝐈𝐧𝐭 ⊢! q✝
⊢ 𝐒𝟒 ⊢! q✝ᵍ
Tactic:
exact axiomT'! $ axiomK''! (by simpa using ihpq ⟨hpq⟩) $ nec! $ ihp ⟨hp⟩
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
hpq : Superintuitionistic.Deduction 𝐈𝐧𝐭 (p✝ ⟶ q✝)
hp : Superintuitionistic.Deduction 𝐈𝐧𝐭 p✝
ihpq : 𝐈𝐧𝐭 ⊢! p✝ ⟶ q✝ → 𝐒𝟒 ⊢! (p✝ ⟶ q✝)ᵍ
ihp : 𝐈𝐧𝐭 ⊢! p✝ → 𝐒𝟒 ⊢! p✝ᵍ
h : 𝐈𝐧𝐭 ⊢! q✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⟶ q✝ᵍ)
Tactic:
simpa using ihpq ⟨hpq⟩
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case verum
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! ⊤
⊢ 𝐒𝟒 ⊢! ⊤ᵍ
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case imply₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⟶ q✝ ⟶ p✝
⊢ 𝐒𝟒 ⊢! (p✝ ⟶ q✝ ⟶ p✝)ᵍ
Tactic:
exact case_imply₁
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case imply₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ r✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
⊢ 𝐒𝟒 ⊢! ((p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝)ᵍ
Tactic:
exact case_imply₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case conj₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐒𝟒 ⊢! (p✝ ⋏ q✝ ⟶ p✝)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, GoedelTranslation.and_def]
Proof state after:
case conj₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⋏ q✝ᵍ ⟶ p✝ᵍ)
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case conj₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⋏ q✝ᵍ ⟶ p✝ᵍ)
Tactic:
exact nec! conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case conj₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐒𝟒 ⊢! (p✝ ⋏ q✝ ⟶ q✝)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, GoedelTranslation.and_def]
Proof state after:
case conj₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⋏ q✝ᵍ ⟶ q✝ᵍ)
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case conj₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⋏ q✝ᵍ ⟶ q✝ᵍ)
Tactic:
exact nec! conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case conj₃
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
⊢ 𝐒𝟒 ⊢! (p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝)ᵍ
Tactic:
exact case_conj₃
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case disj₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐒𝟒 ⊢! (p✝ ⟶ p✝ ⋎ q✝)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, GoedelTranslation.or_def]
Proof state after:
case disj₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⟶ p✝ᵍ ⋎ q✝ᵍ)
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case disj₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⟶ p✝ᵍ ⋎ q✝ᵍ)
Tactic:
exact nec! disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case disj₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐒𝟒 ⊢! (q✝ ⟶ p✝ ⋎ q✝)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, GoedelTranslation.or_def]
Proof state after:
case disj₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐒𝟒 ⊢! □(q✝ᵍ ⟶ p✝ᵍ ⋎ q✝ᵍ)
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case disj₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐒𝟒 ⊢! □(q✝ᵍ ⟶ p✝ᵍ ⋎ q✝ᵍ)
Tactic:
exact nec! disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4
Proof state before:
case disj₃
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ r✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐒𝟒 ⊢! ((p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝)ᵍ
Tactic:
exact case_disj₃
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
⊢ 𝐒𝟒 ⊢! pᵍ → 𝐈𝐧𝐭 ⊢! p
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
⊢ ¬𝐈𝐧𝐭 ⊢! p → ¬𝐒𝟒 ⊢! pᵍ
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
⊢ ¬𝐈𝐧𝐭 ⊢! p → ¬𝐒𝟒 ⊢! pᵍ
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : ¬𝐈𝐧𝐭 ⊢! p
⊢ ¬𝐒𝟒 ⊢! pᵍ
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : ¬𝐈𝐧𝐭 ⊢! p
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
obtain ⟨iF, _, iV, iV_hereditary, w, h⟩ := by simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr Superintuitionistic.Kripke.complete! h;
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
⊢ ¬𝐒𝟒 ⊢! pᵍ
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
let M : Modal.Standard.Kripke.Model α := { Frame := { Rel := iF.Rel }, Valuation := iV }
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
⊢ ¬𝐒𝟒 ⊢! pᵍ