internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋏ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∧ q ∈ t.tableau.1

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1 → p ⋏ q ∈ t.tableau.1
Tactic:
. intro h; constructor <;> exact mdp₁ h (by simp)
Proof state after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1 → p ⋏ q ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1 → p ⋏ q ∈ t.tableau.1
Tactic:
. rintro ⟨hp, hq⟩;
  by_contra hC;
  have : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj' := by simp;
  have : 𝓓 ⊬! [p, q].conj' ⟶ [p ⋏ q].disj' := t.consistent (by aesop) (by simpa using t.not_mem₁_iff_mem₂.mp hC);
  contradiction;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋏ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∧ q ∈ t.tableau.1
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋏ q ∈ t.tableau.1
⊢ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋏ q ∈ t.tableau.1
⊢ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1
Tactic:
constructor <;> exact mdp₁ h (by simp)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋏ q ∈ t.tableau.1
⊢ 𝓓 ⊢! p ⋏ q ⟶ q
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1 → p ⋏ q ∈ t.tableau.1
Tactic:
rintro ⟨hp, hq⟩
Proof state after:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
⊢ p ⋏ q ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
⊢ p ⋏ q ∈ t.tableau.1
Tactic:
by_contra hC
Proof state after:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
⊢ False
Tactic:
have : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj' := by simp;
Proof state after:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ False
Tactic:
have : 𝓓 ⊬! [p, q].conj' ⟶ [p ⋏ q].disj' := t.consistent (by aesop) (by simpa using t.not_mem₁_iff_mem₂.mp hC)
Proof state after:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this✝ : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
this : 𝓓 ⊬! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this✝ : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
this : 𝓓 ⊬! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
⊢ 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ ∀ p_1 ∈ [p, q], p_1 ∈ t.tableau.1
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ ∀ p_1 ∈ [p ⋏ q], p_1 ∈ t.tableau.2
Tactic:
simpa using t.not_mem₁_iff_mem₂.mp hC
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 ↔ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∨ q ∈ t.tableau.1

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∨ q ∈ t.tableau.1

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
Tactic:
. intro h;
  by_contra hC; simp [not_or] at hC;
  have : p ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.1;
  have : q ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.2;
  have : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj' := by simp;
  have : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj' := t.consistent (by simp_all) (by simp_all);
  contradiction;
Proof state after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
Tactic:
. intro h;
  cases h with
  | inl h => exact mdp₁ h disj₁!
  | inr h => exact mdp₁ h disj₂!
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
Tactic:
by_contra hC
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : ¬(p ∈ t.tableau.1 ∨ q ∈ t.tableau.1)
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : ¬(p ∈ t.tableau.1 ∨ q ∈ t.tableau.1)
⊢ False
Tactic:
simp [not_or] at hC
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
⊢ False
Tactic:
have : p ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.1
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this : p ∈ t.tableau.2
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this : p ∈ t.tableau.2
⊢ False
Tactic:
have : q ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.2
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝ : p ∈ t.tableau.2
this : q ∈ t.tableau.2
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝ : p ∈ t.tableau.2
this : q ∈ t.tableau.2
⊢ False
Tactic:
have : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj' := by simp;
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False
Tactic:
have : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj' := t.consistent (by simp_all) (by simp_all)
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝² : p ∈ t.tableau.2
this✝¹ : q ∈ t.tableau.2
this✝ : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
this : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝² : p ∈ t.tableau.2
this✝¹ : q ∈ t.tableau.2
this✝ : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
this : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝ : p ∈ t.tableau.2
this : q ∈ t.tableau.2
⊢ 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ ∀ p_1 ∈ [p ⋎ q], p_1 ∈ t.tableau.1
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ ∀ p_1 ∈ [p, q], p_1 ∈ t.tableau.2
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
⊢ p ⋎ q ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
⊢ p ⋎ q ∈ t.tableau.1
Tactic:
cases h with
| inl h => exact mdp₁ h disj₁!
| inr h => exact mdp₁ h disj₂!
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mpr.inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ∈ t.tableau.1
⊢ p ⋎ q ∈ t.tableau.1
Tactic:
exact mdp₁ h disj₁!
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or
Proof state before:
case mpr.inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : q ∈ t.tableau.1
⊢ p ⋎ q ∈ t.tableau.1
Tactic:
exact mdp₁ h disj₂!
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_of_provable
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → p ∈ t.tableau.1
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
⊢ p ∈ t.tableau.1
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_of_provable
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
⊢ p ∈ t.tableau.1
Tactic:
exact mdp₁ mem₁_verum $ dhyp! h
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.frame_def
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t₁ t₂ : SCT 𝓓
⊢ (CanonicalModel 𝓓).Rel t₁ t₂ ↔ t₁.tableau.1 ⊆ t₂.tableau.1
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.valuation_def
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
a : α
⊢ (CanonicalModel 𝓓).Valuation t a ↔ atom a ∈ t.tableau.1
Tactic:
rfl
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 : Formula α
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p ↔ p ∈ t.tableau.1
Tactic:
induction p using rec' generalizing t with
| himp p q ihp ihq =>
  constructor;
  . 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;
  . 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));
      );
| _ => simp [Satisfies.iff_models, Satisfies, *];
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.truthlemma
Proof state before:
case himp
α : 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:
constructor
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
⊢ 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