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 α
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
⊢ ∀ p_1 ∈ [p, p ⟶ q], p_1 ∈ 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 α
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
⊢ 𝓓 ⊢! [p, p ⟶ q].conj' ⟶ q
Tactic:
simp
Proof state after:
α : 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
⊢ 𝓓 ⊢! p ⋏ (p ⟶ q) ⟶ q
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 α
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
⊢ 𝓓 ⊢! p ⋏ (p ⟶ q) ⟶ q
Tactic:
apply andImplyIffImplyImply'!.mpr
Proof state after:
α : 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
⊢ 𝓓 ⊢! p ⟶ (p ⟶ q) ⟶ q
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 α
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
⊢ 𝓓 ⊢! p ⟶ (p ⟶ q) ⟶ 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 α
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
⊢ [p] ⊢[𝓓]! (p ⟶ q) ⟶ 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 α
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
⊢ [p] ⊢[𝓓]! (p ⟶ q) ⟶ 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 α
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
⊢ [p ⟶ q, p] ⊢[𝓓]! 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 α
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
⊢ [p ⟶ q, p] ⊢[𝓓]! q
Tactic:
exact by_axm! ⨀ (by_axm! (p := p))
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case hor
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p✝ q✝ : Formula α
a✝¹ : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p✝ ↔ p✝ ∈ t.tableau.1
a✝ : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q✝ ↔ q✝ ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p✝ ⋎ q✝ ↔ p✝ ⋎ q✝ ∈ t.tableau.1
Tactic:
simp [Satisfies.iff_models, Satisfies, *]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p ↔ 𝓓 ⊢! p
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p → 𝓓 ⊢! p

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p → 𝓓 ⊢! p

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
Tactic:
. contrapose;
  intro h;
  have : (𝓓)-Consistent (∅, {p}) := by
    simp only [Tableau.ParametricConsistent, Collection.not_mem_empty, imp_false, Set.mem_singleton_iff];
    rintro Γ Δ hΓ hΔ;
    by_contra hC;
    replace hΓ : Γ = [] := List.nil_iff.mpr hΓ;
    subst hΓ;
    have : 𝓓 ⊢! p := disj_allsame'! hΔ (hC ⨀ verum!);
    contradiction;
  obtain ⟨t', ht'⟩ := lindenbaum this;
  simp [ValidOnModel.iff_models, ValidOnModel]
  existsi t';
  apply truthlemma.not.mpr;
  apply t'.not_mem₁_iff_mem₂.mpr;
  simp_all;
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
Tactic:
. intro h t;
  suffices p ∈ t.tableau.1 by exact truthlemma.mpr this;
  exact mem₁_of_provable h;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p → 𝓓 ⊢! p
Tactic:
contrapose
Proof state after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ ¬𝓓 ⊢! p → ¬CanonicalModel 𝓓 ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ ¬𝓓 ⊢! p → ¬CanonicalModel 𝓓 ⊧ p
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ¬CanonicalModel 𝓓 ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ¬CanonicalModel 𝓓 ⊧ p
Tactic:
have : (𝓓)-Consistent (∅, {p}) := by
  simp only [Tableau.ParametricConsistent, Collection.not_mem_empty, imp_false, Set.mem_singleton_iff];
  rintro Γ Δ hΓ hΔ;
  by_contra hC;
  replace hΓ : Γ = [] := List.nil_iff.mpr hΓ;
  subst hΓ;
  have : 𝓓 ⊢! p := disj_allsame'! hΔ (hC ⨀ verum!);
  contradiction;
Proof state after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
⊢ ¬CanonicalModel 𝓓 ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
⊢ ¬CanonicalModel 𝓓 ⊧ p
Tactic:
obtain ⟨t', ht'⟩ := lindenbaum this
Proof state after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬CanonicalModel 𝓓 ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬CanonicalModel 𝓓 ⊧ p
Tactic:
simp [ValidOnModel.iff_models, ValidOnModel]
Proof state after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ∃ x, ¬Satisfies (CanonicalModel 𝓓) x p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ∃ x, ¬Satisfies (CanonicalModel 𝓓) x p
Tactic:
existsi t'
Proof state after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬Satisfies (CanonicalModel 𝓓) t' p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬Satisfies (CanonicalModel 𝓓) t' p
Tactic:
apply truthlemma.not.mpr
Proof state after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ p ∉ t'.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ p ∉ t'.tableau.1
Tactic:
apply t'.not_mem₁_iff_mem₂.mpr
Proof state after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ p ∈ t'.tableau.2
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ p ∈ t'.tableau.2
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ (𝓓)-Consistent (∅, {p})
Tactic:
simp only [Tableau.ParametricConsistent, Collection.not_mem_empty, imp_false, Set.mem_singleton_iff]
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ∀ {Γ Δ : List (Formula α)}, (∀ (p : Formula α), p ∉ Γ) → (∀ p_1 ∈ Δ, p_1 = p) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ∀ {Γ Δ : List (Formula α)}, (∀ (p : Formula α), p ∉ Γ) → (∀ p_1 ∈ Δ, p_1 = p) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
rintro Γ Δ hΓ hΔ
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΓ : ∀ (p : Formula α), p ∉ Γ
hΔ : ∀ p_1 ∈ Δ, p_1 = p
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΓ : ∀ (p : Formula α), p ∉ Γ
hΔ : ∀ p_1 ∈ Δ, p_1 = p
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
by_contra hC
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΓ : ∀ (p : Formula α), p ∉ Γ
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΓ : ∀ (p : Formula α), p ∉ Γ
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Tactic:
replace hΓ : Γ = [] := List.nil_iff.mpr hΓ
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
hΓ : Γ = []
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
hΓ : Γ = []
⊢ False
Tactic:
subst hΓ
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
⊢ False
Tactic:
have : 𝓓 ⊢! p := disj_allsame'! hΔ (hC ⨀ verum!)
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
this : 𝓓 ⊢! p
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
this : 𝓓 ⊢! p
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
Tactic:
intro h t
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p
Tactic:
suffices p ∈ t.tableau.1 by exact truthlemma.mpr this;
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
⊢ p ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
⊢ p ∈ t.tableau.1
Tactic:
exact mem₁_of_provable h
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
this : p ∈ t.tableau.1
⊢ t ⊧ p
Tactic:
exact truthlemma.mpr this
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.complete!
Proof state before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
⊢ 𝔽(Ax(𝓓)) ⊧ p → 𝓓 ⊢! p
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ 𝓓 ⊢! p
Theorem: LO.Propositional.Superintuitionistic.Kripke.complete!
Proof state before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ 𝓓 ⊢! p
Tactic:
apply deducible_of_validOnCanonicelModel.mp
Proof state after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ CanonicalModel 𝓓 ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.complete!
Proof state before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ CanonicalModel 𝓓 ⊧ p
Tactic:
exact h Canonical.realize _ _
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
⊢ 𝔽(Ax(𝓓)) ⊧ p
Tactic:
simp [-ValidOnFrame.models_iff]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
⊢ ∀ {F : Frame' α}, F ∈ 𝔽(Ax(𝓓)) → F ⊧ p