Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.membership_iff (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 ↔ Ω.theory *⊢[L]! p
Tactic:
constructor
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

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

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;
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 → Ω.theory *⊢[L]! p
Tactic:
intro h
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

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

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

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

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

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

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

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

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

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

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