internlm/Lean-Github huggingface dataset:
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
Γ : 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:
. assumption;
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 α)
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
Tactic:
intro p hp
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 : Formula α
hp : p ∈ Γ
⊢ p ∈ U
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 : Formula α
hp : p ∈ Γ
⊢ p ∈ U
Tactic:
exact hUs hp
Proof state after:
no goals
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
Γ : 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:
assumption
Proof state after:
no goals
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
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 : Set (Formula α)
a : 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 : Set (Formula α)
a : s ∈ c
⊢ s ⊆ ⋃₀ c
Tactic:
exact Set.subset_sUnion_of_mem a
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
⊢ (L)-Consistent (T₁ ∪ T₂)
Tactic:
intro Δ hΔ
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∪ T₂
⊢ L ⊬! Δ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∪ T₂
⊢ L ⊬! Δ.conj' ⟶ ⊥
Tactic:
simp at hΔ
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
⊢ L ⊬! Δ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
⊢ L ⊬! Δ.conj' ⟶ ⊥
Tactic:
have := @h Δ₁ Δ₂ (by intro _ h; simpa using List.of_mem_filter h;) (by intro _ h; simpa using List.of_mem_filter h;)
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ L ⊬! Δ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ L ⊬! Δ.conj' ⟶ ⊥
Tactic:
exact unprovable_imp_trans! (by
  apply FiniteContext.deduct'!;
  apply iff_provable_list_conj.mpr;
  intro q hq;
  cases (hΔ q hq);
  . exact iff_provable_list_conj.mp (conj₁'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa);
  . exact iff_provable_list_conj.mp (conj₂'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa);
) this
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
⊢ ∀ p ∈ Δ₁, p ∈ T₁
Tactic:
intro _ h
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h✝ : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
p✝ : Formula α
h : p✝ ∈ Δ₁
⊢ p✝ ∈ T₁
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h✝ : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
p✝ : Formula α
h : p✝ ∈ Δ₁
⊢ p✝ ∈ T₁
Tactic:
simpa using List.of_mem_filter h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
⊢ ∀ p ∈ Δ₂, p ∈ T₂
Tactic:
intro _ h
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h✝ : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
p✝ : Formula α
h : p✝ ∈ Δ₂
⊢ p✝ ∈ T₂
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h✝ : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
p✝ : Formula α
h : p✝ ∈ Δ₂
⊢ p✝ ∈ T₂
Tactic:
simpa using List.of_mem_filter h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ L ⊢! Δ₁.conj' ⋏ Δ₂.conj' ⟶ Δ.conj'
Tactic:
apply FiniteContext.deduct'!
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ [Δ₁.conj' ⋏ Δ₂.conj'] ⊢[L]! Δ.conj'
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ [Δ₁.conj' ⋏ Δ₂.conj'] ⊢[L]! Δ.conj'
Tactic:
apply iff_provable_list_conj.mpr
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ ∀ p ∈ Δ, { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! p
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ ∀ p ∈ Δ, { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! p
Tactic:
intro q hq
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
cases (hΔ q hq)
Proof state after:
case h.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₁
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q

case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
case h.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₁
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q

case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
. exact iff_provable_list_conj.mp (conj₁'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa);
Proof state after:
case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
. exact iff_provable_list_conj.mp (conj₂'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa);
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
case h.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₁
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
exact iff_provable_list_conj.mp (conj₁'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₁
⊢ decide (q ∈ T₁) = true
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
exact iff_provable_list_conj.mp (conj₂'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.intro_union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ decide (q ∈ T₂) = true
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.exists_maximal_Lconsistented_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
⊢ ∃ Ω, T ⊆ Ω.theory
Tactic:
have ⟨Ω, hΩ₁, hΩ₂, hΩ₃⟩ := exists_maximal_Lconsistent_theory consisT
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ ∃ Ω, T ⊆ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.exists_maximal_Lconsistented_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ ∃ Ω, T ⊆ Ω.theory
Tactic:
existsi ⟨
  Ω,
  hΩ₁,
  by
    rintro U ⟨hU₁, hU₂⟩;
    by_contra hC;
    have : U = Ω := hΩ₃ U hC hU₁;
    subst_vars;
    simp at hU₂,
⟩
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ T ⊆ { theory := Ω, consistent := ⋯, maximal := ⋯ }.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.exists_maximal_Lconsistented_theory
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ T ⊆ { theory := Ω, consistent := ⋯, maximal := ⋯ }.theory
Tactic:
exact hΩ₂
Proof state after:
no goals