internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
. exact hΓ₁ _ hΓ;
Proof state after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
. exact hΔ₁ _ hΔ;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T
Tactic:
exact hΓ₁ _ hΓ
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
exact hΔ₁ _ hΔ
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
⊢ ∀ c ⊆ {T | (L)-Consistent T},
    IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ {T | (L)-Consistent T}, ∀ s ∈ c, s ⊆ ub
Tactic:
intro c hc chain hnc
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∃ ub ∈ {T | (L)-Consistent T}, ∀ s ∈ c, s ⊆ ub
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∃ ub ∈ {T | (L)-Consistent T}, ∀ s ∈ c, s ⊆ ub
Tactic:
existsi (⋃₀ c)
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ⋃₀ c ∈ {T | (L)-Consistent T} ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ⋃₀ c ∈ {T | (L)-Consistent T} ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
simp only [ParametricConsistent, Set.mem_setOf_eq, Set.mem_sUnion]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥) ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥) ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
. intro Γ;
  by_contra hC;
  obtain ⟨hΓs, hΓd⟩ := by simpa using hC;
  obtain ⟨U, hUc, hUs⟩ :=
    Set.subset_mem_chain_of_finite c hnc chain
      (s := ↑Γ.toFinset) (by simp)
      (by intro p hp; simp_all);
  simp [List.coe_toFinset] at hUs;
  have : (L)-Consistent U := hc hUc;
  have : ¬(L)-Consistent U := by
    simp only [ParametricConsistent, not_forall, not_not, exists_prop];
    existsi Γ;
    constructor;
    . intro p hp; exact hUs hp;
    . assumption;
  contradiction;
Proof state after:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
. intro s a;
  exact Set.subset_sUnion_of_mem a;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro Γ
Proof state after:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
⊢ (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
⊢ (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
by_contra hC
Proof state after:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
⊢ False
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
⊢ False
Tactic:
obtain ⟨hΓs, hΓd⟩ := by simpa using hC;
Proof state after:
case left.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
obtain ⟨U, hUc, hUs⟩ :=
  Set.subset_mem_chain_of_finite c hnc chain
    (s := ↑Γ.toFinset) (by simp)
    (by intro p hp; simp_all)
Proof state after:
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : ↑Γ.toFinset ⊆ U
⊢ False
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : ↑Γ.toFinset ⊆ U
⊢ False
Tactic:
simp [List.coe_toFinset] at hUs
Proof state after:
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
⊢ False
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
⊢ False
Tactic:
have : (L)-Consistent U := hc hUc
Proof state after:
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ False
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ False
Tactic:
have : ¬(L)-Consistent U := by
  simp only [ParametricConsistent, not_forall, not_not, exists_prop];
  existsi Γ;
  constructor;
  . intro p hp; exact hUs hp;
  . assumption;
Proof state after:
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this✝ : (L)-Consistent U
this : ¬(L)-Consistent U
⊢ False
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this✝ : (L)-Consistent U
this : ¬(L)-Consistent U
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
⊢ ?m.149979
Tactic:
simpa using hC
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
⊢ (↑Γ.toFinset).Finite
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
⊢ ↑Γ.toFinset ⊆ ⋃₀ c
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
p : Formula α
hp : p ∈ ↑Γ.toFinset
⊢ p ∈ ⋃₀ c
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
p : Formula α
hp : p ∈ ↑Γ.toFinset
⊢ p ∈ ⋃₀ c
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ¬(L)-Consistent U
Tactic:
simp only [ParametricConsistent, not_forall, not_not, exists_prop]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∃ x, (∀ p ∈ x, p ∈ U) ∧ L ⊢! x.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∃ x, (∀ p ∈ x, p ∈ U) ∧ L ⊢! x.conj' ⟶ ⊥
Tactic:
existsi Γ
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ (∀ p ∈ Γ, p ∈ U) ∧ L ⊢! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ (∀ p ∈ Γ, p ∈ U) ∧ L ⊢! Γ.conj' ⟶ ⊥
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∀ p ∈ Γ, p ∈ U

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ L ⊢! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory
Proof state before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∀ p ∈ Γ, p ∈ U

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ L ⊢! Γ.conj' ⟶ ⊥
Tactic:
. intro p hp; exact hUs hp;
Proof state after:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ L ⊢! Γ.conj' ⟶ ⊥