Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ~p ∈ Ω.theory ↔ p ∉ Ω.theory
Tactic:
constructor
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

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;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∉ Ω.theory → ~p ∈ Ω.theory

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;
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
⊢ ~p ∈ Ω.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
have := provable_iff_insert_neg_not_Lconsistent.not.mp $ membership_iff.not.mp hp
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this : ¬¬(L)-Consistent insert (~p) Ω.theory
⊢ ~p ∈ Ω.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this : ¬¬(L)-Consistent insert (~p) Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
have := (not_imp_not.mpr $ Ω.maximal (U := insert (~p) Ω.theory)) this
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : ¬Ω.theory ⊂ insert (~p) Ω.theory
⊢ ~p ∈ Ω.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : ¬Ω.theory ⊂ insert (~p) Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
simp [Set.ssubset_def] at this
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : insert (p ⟶ ⊥) Ω.theory ⊆ Ω.theory
⊢ ~p ∈ Ω.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : insert (p ⟶ ⊥) Ω.theory ⊆ Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
apply this
State after:
case mpr.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : insert (p ⟶ ⊥) Ω.theory ⊆ Ω.theory
⊢ ~p ∈ insert (p ⟶ ⊥) Ω.theory

State before:
case mpr.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : insert (p ⟶ ⊥) Ω.theory ⊆ Ω.theory
⊢ ~p ∈ insert (p ⟶ ⊥) Ω.theory
Tactic:
simp
State after:
no goals