internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp
α : 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
⊢ t ⊧ p ⟶ q → p ⟶ q ∈ t.tableau.1

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:
. contrapose;
  simp_all;
  intro h;
  replace h := t.not_mem₁_iff_mem₂.mp h;
  have : (𝓓)-Consistent (insert p t.tableau.1, {q}) := by
    simp only [Tableau.ParametricConsistent];
    intro Γ Δ hΓ hΔ;
    replace hΓ : ∀ r, r ∈ Γ.remove p → r ∈ t.tableau.1 := by
      intro r hr;
      have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr;
      have := by simpa using hΓ r hr₁;
      simp_all;
    by_contra hC;
    have : 𝓓 ⊢! (Γ.remove p).conj' ⟶ (p ⟶ q) := imp_trans! (andImplyIffImplyImply'!.mp $ implyLeftRemoveConj' hC) (by
      apply deduct'!;
      apply deduct!;
      have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp);
      have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this;
      exact disj_allsame'! (by simpa using hΔ) this;
    )
    have : 𝓓 ⊬! (Γ.remove p).conj' ⟶ (p ⟶ q) := by simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all));
    contradiction;
  obtain ⟨t', ⟨⟨_, _⟩, _⟩⟩ := by simpa [Set.insert_subset_iff] using lindenbaum this;
  existsi t';
  simp_all;
  apply t'.not_mem₁_iff_mem₂.mpr;
  assumption;
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 → t ⊧ p ⟶ 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 → t ⊧ p ⟶ q
Tactic:
. simp [Satisfies.imp_def];
  intro h t' htt' hp;
  replace hp := ihp.mp hp;
  have hpq := htt' h;
  apply ihq.mpr;
  apply t'.not_mem₂_iff_mem₁.mp;
  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
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp
α : 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
⊢ t ⊧ p ⟶ q → p ⟶ q ∈ t.tableau.1
Tactic:
contrapose
Proof state after:
case himp.mp
α : 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
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp
α : 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_all
Proof state after:
case himp.mp
α : 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
⊢ p ⟶ q ∉ t.tableau.1 → ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp
α : 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
⊢ p ⟶ q ∉ t.tableau.1 → ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
intro h
Proof state after:
case himp.mp
α : 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.1
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp
α : 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.1
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
replace h := t.not_mem₁_iff_mem₂.mp h
Proof state after:
case himp.mp
α : 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
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp
α : 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
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
have : (𝓓)-Consistent (insert p t.tableau.1, {q}) := by
  simp only [Tableau.ParametricConsistent];
  intro Γ Δ hΓ hΔ;
  replace hΓ : ∀ r, r ∈ Γ.remove p → r ∈ t.tableau.1 := by
    intro r hr;
    have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr;
    have := by simpa using hΓ r hr₁;
    simp_all;
  by_contra hC;
  have : 𝓓 ⊢! (Γ.remove p).conj' ⟶ (p ⟶ q) := imp_trans! (andImplyIffImplyImply'!.mp $ implyLeftRemoveConj' hC) (by
    apply deduct'!;
    apply deduct!;
    have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp);
    have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this;
    exact disj_allsame'! (by simpa using hΔ) this;
  )
  have : 𝓓 ⊬! (Γ.remove p).conj' ⟶ (p ⟶ q) := by simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all));
  contradiction;
Proof state after:
case himp.mp
α : 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})
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp
α : 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})
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
obtain ⟨t', ⟨⟨_, _⟩, _⟩⟩ := by simpa [Set.insert_subset_iff] using lindenbaum this;
Proof state after:
case himp.mp.intro.intro.intro
α : 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})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp.intro.intro.intro
α : 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})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
existsi t'
Proof state after:
case himp.mp.intro.intro.intro
α : 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})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ t.tableau.1 ⊆ t'.tableau.1 ∧ p ∈ t'.tableau.1 ∧ q ∉ t'.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp.intro.intro.intro
α : 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})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ t.tableau.1 ⊆ t'.tableau.1 ∧ p ∈ t'.tableau.1 ∧ q ∉ t'.tableau.1
Tactic:
simp_all
Proof state after:
case himp.mp.intro.intro.intro
α : 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})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∉ t'.tableau.1
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp.intro.intro.intro
α : 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})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∉ t'.tableau.1
Tactic:
apply t'.not_mem₁_iff_mem₂.mpr
Proof state after:
case himp.mp.intro.intro.intro
α : 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})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∈ t'.tableau.2
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp.mp.intro.intro.intro
α : 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})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∈ t'.tableau.2
Tactic:
assumption
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
⊢ (𝓓)-Consistent (insert p t.tableau.1, {q})
Tactic:
simp only [Tableau.ParametricConsistent]
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 α)}, (∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1) → (∀ p ∈ Δ, p ∈ {q}) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
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 α)}, (∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1) → (∀ p ∈ Δ, p ∈ {q}) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
intro Γ Δ hΓ hΔ
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}
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
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}
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
replace hΓ : ∀ r, r ∈ Γ.remove p → r ∈ t.tableau.1 := by
  intro r hr;
  have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr;
  have := by simpa using hΓ r hr₁;
  simp_all;
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 ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
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
⊢ 𝓓 ⊬! Γ.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 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'
⊢ False
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'
⊢ False
Tactic:
have : 𝓓 ⊢! (Γ.remove p).conj' ⟶ (p ⟶ q) := imp_trans! (andImplyIffImplyImply'!.mp $ implyLeftRemoveConj' hC) (by
  apply deduct'!;
  apply deduct!;
  have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp);
  have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this;
  exact disj_allsame'! (by simpa using hΔ) this;
)
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 ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ False
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
⊢ False
Tactic:
have : 𝓓 ⊬! (Γ.remove p).conj' ⟶ (p ⟶ q) := by simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all));
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 ∈ Δ, 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