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

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋎ q ∈ Ω.theory ↔ p ∈ Ω.theory ∨ q ∈ Ω.theory
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋎ q ∈ Ω.theory → p ∈ Ω.theory ∨ q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋎ q ∈ Ω.theory → p ∈ Ω.theory ∨ q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory
Tactic:
. intro hpq;
  replace hpq := membership_iff.mp hpq;
  by_contra hC; simp [not_or] at hC;
  have ⟨hp, hq⟩ := hC;
  replace hp := membership_iff.mp $ iff_mem_neg.mpr hp;
  replace hq := membership_iff.mp $ iff_mem_neg.mpr hq;
  have : Ω.theory *⊢[L]! ⊥ := disj₃'! hp hq hpq;
  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 q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory
Tactic:
. rintro (hp | hq);
  . apply membership_iff.mpr;
    exact disj₁'! (membership_iff.mp hp);
  . apply membership_iff.mpr;
    exact disj₂'! (membership_iff.mp hq);
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋎ q ∈ Ω.theory → p ∈ Ω.theory ∨ q ∈ Ω.theory
Tactic:
intro hpq
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⋎ q ∈ Ω.theory
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⋎ q ∈ Ω.theory
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory
Tactic:
replace hpq := membership_iff.mp hpq
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory
Tactic:
by_contra hC
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : ¬(p ∈ Ω.theory ∨ q ∈ Ω.theory)
⊢ False

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : ¬(p ∈ Ω.theory ∨ q ∈ Ω.theory)
⊢ False
Tactic:
simp [not_or] at hC
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
⊢ False

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
⊢ False
Tactic:
have ⟨hp, hq⟩ := hC
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : p ∉ Ω.theory
hq : q ∉ Ω.theory
⊢ False

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : p ∉ Ω.theory
hq : q ∉ Ω.theory
⊢ False
Tactic:
replace hp := membership_iff.mp $ iff_mem_neg.mpr hp
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hq : q ∉ Ω.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 q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hq : q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
⊢ False
Tactic:
replace hq := membership_iff.mp $ iff_mem_neg.mpr hq
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
⊢ False

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
⊢ False
Tactic:
have : Ω.theory *⊢[L]! ⊥ := disj₃'! hp hq hpq
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
this : Ω.theory *⊢[L]! ⊥
⊢ False

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
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 q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
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 q : Formula α
hpq : Ω.theory *⊢[L]! p ⋎ q
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
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 q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory
Tactic:
rintro (hp | hq)
State after:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory

case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory

State before:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory

case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Tactic:
. apply membership_iff.mpr;
  exact disj₁'! (membership_iff.mp hp);
State after:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory

State before:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Tactic:
. apply membership_iff.mpr;
  exact disj₂'! (membership_iff.mp hq);
State after:
no goals

State before:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
State after:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋎ q

State before:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋎ q
Tactic:
exact disj₁'! (membership_iff.mp hp)
State after:
no goals

State before:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
State after:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋎ q

State before:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋎ q
Tactic:
exact disj₂'! (membership_iff.mp hq)
State after:
no goals