Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb (Logic/Modal/Standard/Provability/Basic.lean)

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐊𝟒(𝐋) ⊢! p
⊢ ∀ {f : realization L α}, T ⊢! f[β] p
Tactic:
intro f
State after:
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐊𝟒(𝐋) ⊢! p
f : realization L α
⊢ T ⊢! f[β] p

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐊𝟒(𝐋) ⊢! p
f : realization L α
⊢ T ⊢! f[β] p
Tactic:
induction h using Deduction.inducition! with
| hNec _ ih => exact HilbertBernays₁.D1s (T₀ := T₀) ih;
| hMaxm hp =>
  rcases hp with (hK | hFour)
  . obtain ⟨p, q, e⟩ := hK; subst_vars; apply HilbertBernays₂.D2s (T₀ := T₀);
  . obtain ⟨p, e⟩ := hFour; subst_vars; apply HilbertBernays₃.D3s (T₀ := T₀);
| hLoeb _ ih => exact Loeb.LT T₀ ih;
| hHenkin => simp_all only [Bool.false_eq_true];
| hMdp ihpq ihp =>
  simp [interpretation] at ihpq;
  exact ihpq ⨀ ihp;
| hDne =>
  dsimp [interpretation];
  exact imp_trans! (conj₁'! $ iffComm'! NegationEquiv.negneg_equiv!) dne!;
| _ =>
  dsimp;
  first
  | apply verum!;
  | apply imply₁!;
  | apply imply₂!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
State after:
no goals

State before:
case hNec
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
hasNec✝ : 𝐊𝟒(𝐋).rules.nec = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐋) ⊢! p✝
ih : T ⊢! f[β] p✝
⊢ T ⊢! f[β] □p✝
Tactic:
exact HilbertBernays₁.D1s (T₀ := T₀) ih
State after:
no goals

State before:
case hMaxm
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hp : p✝ ∈ Ax(𝐊𝟒(𝐋))
⊢ T ⊢! f[β] p✝
Tactic:
rcases hp with (hK | hFour)
State after:
case hMaxm.inl
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ T ⊢! f[β] p✝

case hMaxm.inr
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ T ⊢! f[β] p✝

State before:
case hMaxm.inl
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ T ⊢! f[β] p✝

case hMaxm.inr
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ T ⊢! f[β] p✝
Tactic:
. obtain ⟨p, q, e⟩ := hK; subst_vars; apply HilbertBernays₂.D2s (T₀ := T₀);
State after:
case hMaxm.inr
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ T ⊢! f[β] p✝

State before:
case hMaxm.inr
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ T ⊢! f[β] p✝
Tactic:
. obtain ⟨p, e⟩ := hFour; subst_vars; apply HilbertBernays₃.D3s (T₀ := T₀);
State after:
no goals

State before:
case hMaxm.inl
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ T ⊢! f[β] p✝
Tactic:
obtain ⟨p, q, e⟩ := hK
State after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝¹ : Formula α
f : realization L α
p✝ p q : Formula α
e : Axioms.K p q = p✝
⊢ T ⊢! f[β] p✝

State before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝¹ : Formula α
f : realization L α
p✝ p q : Formula α
e : Axioms.K p q = p✝
⊢ T ⊢! f[β] p✝
Tactic:
subst_vars
State after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝ : Formula α
f : realization L α
p q : Formula α
⊢ T ⊢! f[β] Axioms.K p q

State before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝ : Formula α
f : realization L α
p q : Formula α
⊢ T ⊢! f[β] Axioms.K p q
Tactic:
apply HilbertBernays₂.D2s (T₀ := T₀)
State after:
no goals

State before:
case hMaxm.inr
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ T ⊢! f[β] p✝
Tactic:
obtain ⟨p, e⟩ := hFour
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝¹ : Formula α
f : realization L α
p✝ p : Formula α
e : Axioms.Four p = p✝
⊢ T ⊢! f[β] p✝

State before:
case hMaxm.inr.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝¹ : Formula α
f : realization L α
p✝ p : Formula α
e : Axioms.Four p = p✝
⊢ T ⊢! f[β] p✝
Tactic:
subst_vars
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝ : Formula α
f : realization L α
p : Formula α
⊢ T ⊢! f[β] Axioms.Four p

State before:
case hMaxm.inr.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝ : Formula α
f : realization L α
p : Formula α
⊢ T ⊢! f[β] Axioms.Four p
Tactic:
apply HilbertBernays₃.D3s (T₀ := T₀)
State after:
no goals

State before:
case hLoeb
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
hasLoeb✝ : 𝐊𝟒(𝐋).rules.loeb = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐋) ⊢! □p✝ ⟶ p✝
ih : T ⊢! f[β] □p✝ ⟶ p✝
⊢ T ⊢! f[β] p✝
Tactic:
exact Loeb.LT T₀ ih
State after:
no goals

State before:
case hHenkin
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
hasHenkin✝ : 𝐊𝟒(𝐋).rules.henkin = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐋) ⊢! □p✝ ⟷ p✝
a✝ : T ⊢! f[β] □p✝ ⟷ p✝
⊢ T ⊢! f[β] p✝
Tactic:
simp_all only [Bool.false_eq_true]
State after:
no goals

State before:
case hMdp
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
hpq✝ : 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝
hp✝ : 𝐊𝟒(𝐋) ⊢! p✝
ihpq : T ⊢! f[β] p✝ ⟶ q✝
ihp : T ⊢! f[β] p✝
⊢ T ⊢! f[β] q✝
Tactic:
simp [interpretation] at ihpq
State after:
case hMdp
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
hpq✝ : 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝
hp✝ : 𝐊𝟒(𝐋) ⊢! p✝
ihpq : T ⊢! (f[β] p✝) ⟶ f[β] q✝
ihp : T ⊢! f[β] p✝
⊢ T ⊢! f[β] q✝

State before:
case hMdp
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
hpq✝ : 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝
hp✝ : 𝐊𝟒(𝐋) ⊢! p✝
ihpq : T ⊢! (f[β] p✝) ⟶ f[β] q✝
ihp : T ⊢! f[β] p✝
⊢ T ⊢! f[β] q✝
Tactic:
exact ihpq ⨀ ihp
State after:
no goals

State before:
case hDne
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
⊢ T ⊢! f[β] ~~p✝ ⟶ p✝
Tactic:
dsimp [interpretation]
State after:
case hDne
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
⊢ T ⊢! (((f[β] p✝) ⟶ ⊥) ⟶ ⊥) ⟶ f[β] p✝

State before:
case hDne
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
⊢ T ⊢! (((f[β] p✝) ⟶ ⊥) ⟶ ⊥) ⟶ f[β] p✝
Tactic:
exact imp_trans! (conj₁'! $ iffComm'! NegationEquiv.negneg_equiv!) dne!
State after:
no goals

State before:
case hDisj₃
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ r✝ : Formula α
⊢ T ⊢! f[β] (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
State after:
no goals

State before:
case hVerum
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
⊢ T ⊢! f[β] ⊤
Tactic:
apply verum!
State after:
no goals

State before:
case hImply₁
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply imply₁!
State after:
no goals

State before:
case hImply₂
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ r✝ : Formula α
⊢ T ⊢! f[β] (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply imply₂!
State after:
no goals

State before:
case hConj₁
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply conj₁!
State after:
no goals

State before:
case hConj₂
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply conj₂!
State after:
no goals

State before:
case hConj₃
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply conj₃!
State after:
no goals

State before:
case hDisj₁
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₁!
State after:
no goals

State before:
case hDisj₂
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₂!
State after:
no goals

State before:
case hDisj₃
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ r✝ : Formula α
⊢ T ⊢! f[β] (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply disj₃!
State after:
no goals