internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ~~p✝ ⟶ p✝
Tactic:
apply dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐊𝟒(𝐇)
Tactic:
apply System.reducible_iff.mpr
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {f : Formula α}, 𝐊𝟒(𝐋) ⊢! f → 𝐊𝟒(𝐇) ⊢! f
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {f : Formula α}, 𝐊𝟒(𝐋) ⊢! f → 𝐊𝟒(𝐇) ⊢! f
Tactic:
intro p h
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒(𝐋) ⊢! p
⊢ 𝐊𝟒(𝐇) ⊢! p
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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 | hFour)
  . obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
  . obtain ⟨_, e⟩ := hFour; subst_vars; exact axiomFour!;
| 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : p✝ ∈ Ax(𝐊𝟒(𝐋))
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Tactic:
rcases hp with (hK | hFour)
Proof 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 α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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 α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
Proof state after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Tactic:
. obtain ⟨_, e⟩ := hFour; subst_vars; exact axiomFour!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! Axioms.K w✝¹ w✝
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! Axioms.K w✝¹ w✝
Tactic:
exact axiomK!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Tactic:
obtain ⟨_, e⟩ := hFour
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.Four w✝ = p✝
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.Four w✝ = p✝
⊢ 𝐊𝟒(𝐇) ⊢! p✝
Tactic:
subst_vars
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! Axioms.Four w✝
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! Axioms.Four w✝
Tactic:
exact axiomFour!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Loeb_K4Henkin
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒(𝐇) ⊢! ~~p✝ ⟶ p✝
Tactic:
apply dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐇) ≤ₛ 𝐊𝟒𝐇
Tactic:
apply System.reducible_iff.mpr
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {f : Formula α}, 𝐊𝟒(𝐇) ⊢! f → 𝐊𝟒𝐇 ⊢! f
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {f : Formula α}, 𝐊𝟒(𝐇) ⊢! f → 𝐊𝟒𝐇 ⊢! f
Tactic:
intro p h
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒(𝐇) ⊢! p
⊢ 𝐊𝟒𝐇 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof 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 | hFour)
  . obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
  . obtain ⟨_, e⟩ := hFour; subst_vars; exact axiomFour!;
| hMdp ihpq ihp => exact ihpq ⨀ ihp;
| hNec _ ihp => exact Necessitation.nec! ihp;
| hHenkin _ ihp => exact HenkinRule.henkin! ihp;
| hLoeb => 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : p✝ ∈ Ax(𝐊𝟒(𝐇))
⊢ 𝐊𝟒𝐇 ⊢! p✝
Tactic:
rcases hp with (hK | hFour)
Proof 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 α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒𝐇 ⊢! p✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof 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 α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒𝐇 ⊢! p✝
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
Proof state after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒𝐇 ⊢! p✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒𝐇 ⊢! p✝
Tactic:
. obtain ⟨_, e⟩ := hFour; subst_vars; exact axiomFour!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒𝐇 ⊢! p✝
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒𝐇 ⊢! p✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof 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
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! Axioms.K w✝¹ w✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! Axioms.K w✝¹ w✝
Tactic:
exact axiomK!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒𝐇 ⊢! p✝
Tactic:
obtain ⟨_, e⟩ := hFour
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.Four w✝ = p✝
⊢ 𝐊𝟒𝐇 ⊢! p✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.Four w✝ = p✝
⊢ 𝐊𝟒𝐇 ⊢! p✝
Tactic:
subst_vars
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! Axioms.Four w✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! Axioms.Four w✝
Tactic:
exact axiomFour!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hHenkin
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasHenkin✝ : 𝐊𝟒(𝐇).rules.henkin = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐇) ⊢! □p✝ ⟷ p✝
ihp : 𝐊𝟒𝐇 ⊢! □p✝ ⟷ p✝
⊢ 𝐊𝟒𝐇 ⊢! p✝
Tactic:
exact HenkinRule.henkin! ihp
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hLoeb
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasLoeb✝ : 𝐊𝟒(𝐇).rules.loeb = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐇) ⊢! □p✝ ⟶ p✝
a✝ : 𝐊𝟒𝐇 ⊢! □p✝ ⟶ p✝
⊢ 𝐊𝟒𝐇 ⊢! p✝
Tactic:
simp_all only [Bool.false_eq_true]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒𝐇 ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_K4H
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒𝐇 ⊢! ~~p✝ ⟶ p✝
Tactic:
apply dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒𝐇 ≤ₛ 𝐆𝐋
Tactic:
apply normal_reducible
Proof state after:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {p : Formula α}, p ∈ Ax(𝐊𝟒𝐇) → 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {p : Formula α}, p ∈ Ax(𝐊𝟒𝐇) → 𝐆𝐋 ⊢! p
Tactic:
intro p hp
Proof state after:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hp : p ∈ Ax(𝐊𝟒𝐇)
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hp : p ∈ Ax(𝐊𝟒𝐇)
⊢ 𝐆𝐋 ⊢! p
Tactic:
rcases hp with (hK | hFour) | hH
Proof state after:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
Proof state after:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hFour; subst_vars; exact axiomFour!;
Proof state after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hH; subst_vars; exact axiomH!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p
⊢ 𝐆𝐋 ⊢! p
Tactic:
subst_vars
Proof state after:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
w✝¹ w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
w✝¹ w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
Tactic:
exact axiomK!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hFour
Proof state after:
case hMaxm.inl.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.Four w✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inl.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.Four w✝
Tactic:
exact axiomFour!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hH
Proof state after:
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.H w✝
Theorem: LO.Modal.Standard.reducible_K4Henkin_GL
Proof state before:
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.H w✝
Tactic:
exact axiomH!
Proof state after:
no goals
Theorem: LO.Modal.Standard.equivalent_GL_K4Loeb
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 =ₛ 𝐊𝟒(𝐋)
Tactic:
apply Equiv.antisymm_iff.mpr
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋) ∧ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Theorem: LO.Modal.Standard.equivalent_GL_K4Loeb
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋) ∧ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)

case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Theorem: LO.Modal.Standard.equivalent_GL_K4Loeb
Proof state before:
case left
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)

case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Tactic:
. exact reducible_GL_K4Loeb;
Proof state after:
case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Theorem: LO.Modal.Standard.equivalent_GL_K4Loeb
Proof state before:
case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Tactic:
. exact Reducible.trans (reducible_K4Loeb_K4Henkin) $ Reducible.trans reducible_K4Henkin_K4H reducible_K4Henkin_GL
Proof state after:
no goals
Theorem: LO.Modal.Standard.equivalent_GL_K4Loeb
Proof state before:
case left
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)
Tactic:
exact reducible_GL_K4Loeb
Proof state after:
no goals
Theorem: LO.Modal.Standard.equivalent_GL_K4Loeb
Proof state before:
case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Tactic:
exact Reducible.trans (reducible_K4Loeb_K4Henkin) $ Reducible.trans reducible_K4Henkin_K4H reducible_K4Henkin_GL
Proof state after:
no goals