Theorem: LO.Modal.Standard.reducible_GL_K4Loeb (Logic/Modal/Standard/Deduction.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)
Tactic:
apply System.reducible_iff.mpr
State after:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {f : Formula α}, 𝐆𝐋 ⊢! f → 𝐊𝟒(𝐋) ⊢! f

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {f : Formula α}, 𝐆𝐋 ⊢! f → 𝐊𝟒(𝐋) ⊢! f
Tactic:
intro p h
State after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p
Tactic:
induction h using Deduction.inducition! with
| hMaxm hp =>
  rcases hp with (hK | hL)
  . obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
  . obtain ⟨_, e⟩ := hL; subst_vars; exact axiomL!;
| hMdp ihpq ihp => exact ihpq ⨀ ihp;
| hNec _ ihp => exact Necessitation.nec! ihp;
| hLoeb _ ihp => exact LoebRule.loeb! ihp;
| hHenkin => simp_all only [Bool.false_eq_true];
| _ =>
  try first
  | apply verum!;
  | apply imply₁!;
  | apply imply₂!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply dne!;
State after:
no goals

State before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : p✝ ∈ Ax(𝐆𝐋)
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
rcases hp with (hK | hL)
State after:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒(𝐋) ⊢! p✝

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝

State before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒(𝐋) ⊢! p✝

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
State after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝

State before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
. obtain ⟨_, e⟩ := hL; subst_vars; exact axiomL!;
State after:
no goals

State before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
obtain ⟨_, _, e⟩ := hK
State after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝

State before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
subst_vars
State after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! Axioms.K w✝¹ w✝

State before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! Axioms.K w✝¹ w✝
Tactic:
exact axiomK!
State after:
no goals

State before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
obtain ⟨_, e⟩ := hL
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝

State before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
subst_vars
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! Axioms.L w✝

State before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! Axioms.L w✝
Tactic:
exact axiomL!
State after:
no goals

State before:
case hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
hpq✝ : 𝐆𝐋 ⊢! p✝ ⟶ q✝
hp✝ : 𝐆𝐋 ⊢! p✝
ihpq : 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝
ihp : 𝐊𝟒(𝐋) ⊢! p✝
⊢ 𝐊𝟒(𝐋) ⊢! q✝
Tactic:
exact ihpq ⨀ ihp
State after:
no goals

State before:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasNec✝ : 𝐆𝐋.rules.nec = true
p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢! p✝
ihp : 𝐊𝟒(𝐋) ⊢! p✝
⊢ 𝐊𝟒(𝐋) ⊢! □p✝
Tactic:
exact Necessitation.nec! ihp
State after:
no goals

State before:
case hLoeb
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasLoeb✝ : 𝐆𝐋.rules.loeb = true
p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢! □p✝ ⟶ p✝
ihp : 𝐊𝟒(𝐋) ⊢! □p✝ ⟶ p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
exact LoebRule.loeb! ihp
State after:
no goals

State before:
case hHenkin
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasHenkin✝ : 𝐆𝐋.rules.henkin = true
p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢! □p✝ ⟷ p✝
a✝ : 𝐊𝟒(𝐋) ⊢! □p✝ ⟷ p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
simp_all only [Bool.false_eq_true]
State after:
no goals

State before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ~~p✝ ⟶ p✝
Tactic:
try first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
State after:
no goals

State before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ~~p✝ ⟶ p✝
Tactic:
first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
State after:
no goals

State before:
case hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ⊤
Tactic:
apply verum!
State after:
no goals

State before:
case hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply imply₁!
State after:
no goals

State before:
case hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply imply₂!
State after:
no goals

State before:
case hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply conj₁!
State after:
no goals

State before:
case hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply conj₂!
State after:
no goals

State before:
case hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply conj₃!
State after:
no goals

State before:
case hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₁!
State after:
no goals

State before:
case hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₂!
State after:
no goals

State before:
case hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply disj₃!
State after:
no goals

State before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ~~p✝ ⟶ p✝
Tactic:
apply dne!
State after:
no goals