internlm/Lean-Github huggingface dataset:
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 = Ω
⊢ ∀ {U : Theory α}, Ω ⊂ U → ¬(L)-Consistent U
Tactic:
rintro U ⟨hU₁, hU₂⟩
Proof state after:
case intro
α : 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 = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
⊢ ¬(L)-Consistent U
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.exists_maximal_Lconsistented_theory
Proof state before:
case intro
α : 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 = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
⊢ ¬(L)-Consistent U
Tactic:
by_contra hC
Proof state after:
case intro
α : 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 = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
hC : (L)-Consistent U
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.exists_maximal_Lconsistented_theory
Proof state before:
case intro
α : 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 = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
hC : (L)-Consistent U
⊢ False
Tactic:
have : U = Ω := hΩ₃ U hC hU₁
Proof state after:
case intro
α : 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 = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
hC : (L)-Consistent U
this : U = Ω
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.exists_maximal_Lconsistented_theory
Proof state before:
case intro
α : 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 = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
hC : (L)-Consistent U
this : U = Ω
⊢ False
Tactic:
subst_vars
Proof state after:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
U : Theory α
hC hΩ₁ : (L)-Consistent U
hΩ₂ : T ⊆ U
hΩ₃ : ∀ (U_1 : Theory α), (L)-Consistent U_1 → U ⊆ U_1 → U_1 = U
hU₁ : U ⊆ U
hU₂ : ¬U ⊆ U
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.exists_maximal_Lconsistented_theory
Proof state before:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
U : Theory α
hC hΩ₁ : (L)-Consistent U
hΩ₂ : T ⊆ U
hΩ₃ : ∀ (U_1 : Theory α), (L)-Consistent U_1 → U ⊆ U_1 → U_1 = U
hU₁ : U ⊆ U
hU₂ : ¬U ⊆ U
⊢ False
Tactic:
simp at hU₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.either_mem
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
⊢ p ∈ Ω.theory ∨ ~p ∈ Ω.theory
Tactic:
by_contra hC
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : ¬(p ∈ Ω.theory ∨ ~p ∈ Ω.theory)
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.either_mem
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : ¬(p ∈ Ω.theory ∨ ~p ∈ Ω.theory)
⊢ False
Tactic:
push_neg at hC
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.either_mem
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
⊢ False
Tactic:
cases either_consistent Ω.consistent p with
| inl h => have := Ω.maximal (Set.ssubset_insert hC.1); contradiction;
| inr h => have := Ω.maximal (Set.ssubset_insert hC.2); contradiction;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.either_mem
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert p Ω.theory
⊢ False
Tactic:
have := Ω.maximal (Set.ssubset_insert hC.1)
Proof state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert p Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.either_mem
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert p Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.either_mem
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert (~p) Ω.theory
⊢ False
Tactic:
have := Ω.maximal (Set.ssubset_insert hC.2)
Proof state after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert (~p) Ω.theory
this : ¬(L)-Consistent insert (~p) Ω.theory
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.either_mem
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert (~p) Ω.theory
this : ¬(L)-Consistent insert (~p) Ω.theory
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∈ Ω.theory ↔ Ω.theory *⊢[L]! p
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∈ Ω.theory → Ω.theory *⊢[L]! p

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∈ Ω.theory → Ω.theory *⊢[L]! p

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → p ∈ Ω.theory
Tactic:
. intro h; exact Context.by_axm! h;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → p ∈ Ω.theory
Tactic:
. intro hp;
  suffices ~p ∉ Ω.theory by apply or_iff_not_imp_right.mp $ (either_mem Ω p); assumption;
  by_contra hC;
  have hnp : Ω.theory *⊢[L]! ~p := Context.by_axm! hC;
  have := hnp ⨀ hp;
  have := not_provable_falsum Ω.consistent;
  contradiction;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∈ Ω.theory → Ω.theory *⊢[L]! p
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : p ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : p ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p
Tactic:
exact Context.by_axm! h
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → p ∈ Ω.theory
Tactic:
intro hp
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
⊢ p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
⊢ p ∈ Ω.theory
Tactic:
suffices ~p ∉ Ω.theory by apply or_iff_not_imp_right.mp $ (either_mem Ω p); assumption;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
⊢ ~p ∉ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
⊢ ~p ∉ Ω.theory
Tactic:
by_contra hC
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hC : ~p ∈ Ω.theory
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hC : ~p ∈ Ω.theory
⊢ False
Tactic:
have hnp : Ω.theory *⊢[L]! ~p := Context.by_axm! hC
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hC : ~p ∈ Ω.theory
hnp : Ω.theory *⊢[L]! ~p
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hC : ~p ∈ Ω.theory
hnp : Ω.theory *⊢[L]! ~p
⊢ False
Tactic:
have := hnp ⨀ hp
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hC : ~p ∈ Ω.theory
hnp : Ω.theory *⊢[L]! ~p
this : { ctx := Ω.theory } ⊢! Formula.falsum
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hC : ~p ∈ Ω.theory
hnp : Ω.theory *⊢[L]! ~p
this : { ctx := Ω.theory } ⊢! Formula.falsum
⊢ False
Tactic:
have := not_provable_falsum Ω.consistent
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hC : ~p ∈ Ω.theory
hnp : Ω.theory *⊢[L]! ~p
this✝ : { ctx := Ω.theory } ⊢! Formula.falsum
this : Ω.theory *⊬[L]! ⊥
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hC : ~p ∈ Ω.theory
hnp : Ω.theory *⊢[L]! ~p
this✝ : { ctx := Ω.theory } ⊢! Formula.falsum
this : Ω.theory *⊬[L]! ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
this : ~p ∉ Ω.theory
⊢ p ∈ Ω.theory
Tactic:
apply or_iff_not_imp_right.mp $ (either_mem Ω p)
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
this : ~p ∉ Ω.theory
⊢ ~p ∉ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
this : ~p ∉ Ω.theory
⊢ ~p ∉ Ω.theory
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.subset_axiomset
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ax(L) ⊆ Ω.theory
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.subset_axiomset
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ p ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ Ω.theory *⊢[L]! p
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.subset_axiomset
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ Ω.theory *⊢[L]! p
Tactic:
apply Context.of!
Proof state after:
case b
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.subset_axiomset
Proof state before:
case b
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p
Tactic:
exact ⟨Deduction.maxm (by aesop)⟩
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.subset_axiomset
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ p ∈ Ax(L)
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_verum
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ⊤ ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! ⊤
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_verum
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.unprovable_falsum
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊬[L]! ⊥
Tactic:
apply membership_iff.not.mp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ⊥ ∉ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.unprovable_falsum
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ⊥ ∉ Ω.theory
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ~p ∈ Ω.theory ↔ p ∉ Ω.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ~p ∈ Ω.theory → p ∉ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∉ Ω.theory → ~p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ~p ∈ Ω.theory → p ∉ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∉ Ω.theory → ~p ∈ Ω.theory
Tactic:
. intro hnp;
  by_contra hp;
  replace hp := membership_iff.mp hp;
  replace hnp := membership_iff.mp hnp;
  have : Ω.theory *⊢[L]! ⊥ := hnp ⨀ hp;
  have : Ω.theory *⊬[L]! ⊥ := unprovable_falsum;
  contradiction;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∉ Ω.theory → ~p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∉ Ω.theory → ~p ∈ Ω.theory
Tactic:
. intro hp;
  have := provable_iff_insert_neg_not_Lconsistent.not.mp $ membership_iff.not.mp hp;
  have := (not_imp_not.mpr $ Ω.maximal (U := insert (~p) Ω.theory)) this;
  simp [Set.ssubset_def] at this;
  apply this;
  simp;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ~p ∈ Ω.theory → p ∉ Ω.theory
Tactic:
intro hnp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hnp : ~p ∈ Ω.theory
⊢ p ∉ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hnp : ~p ∈ Ω.theory
⊢ p ∉ Ω.theory
Tactic:
by_contra hp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hnp : ~p ∈ Ω.theory
hp : p ∈ Ω.theory
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hnp : ~p ∈ Ω.theory
hp : p ∈ Ω.theory
⊢ False
Tactic:
replace hp := membership_iff.mp hp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hnp : ~p ∈ Ω.theory
hp : Ω.theory *⊢[L]! p
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hnp : ~p ∈ Ω.theory
hp : Ω.theory *⊢[L]! p
⊢ False
Tactic:
replace hnp := membership_iff.mp hnp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hnp : Ω.theory *⊢[L]! ~p
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hnp : Ω.theory *⊢[L]! ~p
⊢ False
Tactic:
have : Ω.theory *⊢[L]! ⊥ := hnp ⨀ hp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hnp : Ω.theory *⊢[L]! ~p
this : Ω.theory *⊢[L]! ⊥
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hnp : Ω.theory *⊢[L]! ~p
this : Ω.theory *⊢[L]! ⊥
⊢ False
Tactic:
have : Ω.theory *⊬[L]! ⊥ := unprovable_falsum
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hnp : Ω.theory *⊢[L]! ~p
this✝ : Ω.theory *⊢[L]! ⊥
this : Ω.theory *⊬[L]! ⊥
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : Ω.theory *⊢[L]! p
hnp : Ω.theory *⊢[L]! ~p
this✝ : Ω.theory *⊢[L]! ⊥
this : Ω.theory *⊬[L]! ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals