internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := (CanonicalModel L).Valuation } p
Tactic:
exact iff_valid_on_canonicalModel_deducible.not.mpr h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.and_inj
Proof state before:
α : Type u
p₁ q₁ p₂ q₂ : Formula α
⊢ p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Wedge.wedge]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.or_inj
Proof state before:
α : Type u
p₁ q₁ p₂ q₂ : Formula α
⊢ p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Vee.vee]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.imp_inj
Proof state before:
α : Type u
p₁ q₁ p₂ q₂ : Formula α
⊢ p₁ ⟶ p₂ = q₁ ⟶ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Arrow.arrow]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.neg_inj
Proof state before:
α : Type u
p q : Formula α
⊢ ~p = ~q ↔ p = q
Tactic:
simp [NegAbbrev.neg]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.degree_not
Proof state before:
α : Type u
p : Formula α
⊢ (~p).degree = p.degree
Tactic:
simp [NegAbbrev.neg]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Theory.iSigma₀_subset_EA
Proof state before:
L : Language
inst✝² : L.ORing
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : L.Exp
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' 𝐈𝚺₀ ⊆ 𝐄𝐀
Tactic:
simp only [Theory.iSigma, Theory.indH, Theory.add_def, Set.image_union, Set.union_assoc]
Proof state after:
L : Language
inst✝² : L.ORing
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : L.Exp
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪
      ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Hierarchy 𝚺 0) ⊆
    ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪ (𝐄𝐗𝐏 ∪ indScheme ℒₒᵣ(exp) (Hierarchy 𝚺 0))
Theorem: LO.FirstOrder.Arith.Theory.iSigma₀_subset_EA
Proof state before:
L : Language
inst✝² : L.ORing
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : L.Exp
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪
      ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Hierarchy 𝚺 0) ⊆
    ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪ (𝐄𝐗𝐏 ∪ indScheme ℒₒᵣ(exp) (Hierarchy 𝚺 0))
Tactic:
exact Set.union_subset_union_right _ (Set.subset_union_of_subset_right Theory.coe_indH_subset_indH _)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModelExp_unique'
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 0 → M
⊢ Structure.func Language.Zero.zero x✝ = Structure.func Language.Zero.zero x✝
Tactic:
simp[Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModelExp_unique'
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 0 → M
⊢ Structure.func Language.One.one x✝ = Structure.func Language.One.one x✝
Tactic:
simp[Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModelExp_unique'
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 2 → M
⊢ Structure.func Language.Add.add x✝ = Structure.func Language.Add.add x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModelExp_unique'
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 2 → M
⊢ Structure.func Language.Mul.mul x✝ = Structure.func Language.Mul.mul x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModelExp_unique'
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 1 → M
⊢ Structure.func Language.Exp.exp x✝ = Structure.func Language.Exp.exp x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModelExp_unique'
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
r : ℒₒᵣ(exp).Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(=) x✝ = Structure.rel op(=) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModelExp_unique'
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
r : ℒₒᵣ(exp).Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(<) x✝ = Structure.rel op(<) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Standard.modelsSuccInd_exp
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
⊢ ℕ ⊧ₘ ∀ᶠ* succInd p
Tactic:
simp [Empty.eq_elim, succInd, models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons',
  Semiformula.eval_substs, Semiformula.eval_rew_q Rew.toS, Function.comp]
Proof state after:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
⊢ ∀ (ε : ℕ → ℕ),
    (Semiformula.Eval (standardModelExp ℕ) ![0] ε) p →
      (∀ (x : ℕ),
          (Semiformula.Eval (standardModelExp ℕ) ![x] ε) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] ε) p) →
        ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] ε) p
Theorem: LO.FirstOrder.Arith.Standard.modelsSuccInd_exp
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
⊢ ∀ (ε : ℕ → ℕ),
    (Semiformula.Eval (standardModelExp ℕ) ![0] ε) p →
      (∀ (x : ℕ),
          (Semiformula.Eval (standardModelExp ℕ) ![x] ε) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] ε) p) →
        ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] ε) p
Tactic:
intro e hzero hsucc x
Proof state after:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
x : ℕ
⊢ (Semiformula.Eval (standardModelExp ℕ) ![x] e) p
Theorem: LO.FirstOrder.Arith.Standard.modelsSuccInd_exp
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
x : ℕ
⊢ (Semiformula.Eval (standardModelExp ℕ) ![x] e) p
Tactic:
induction' x with x ih
Proof state after:
case zero
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
⊢ (Semiformula.Eval (standardModelExp ℕ) ![0] e) p

case succ
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
x : ℕ
ih : (Semiformula.Eval (standardModelExp ℕ) ![x] e) p
⊢ (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
Theorem: LO.FirstOrder.Arith.Standard.modelsSuccInd_exp
Proof state before:
case zero
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
⊢ (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
Tactic:
exact hzero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Standard.modelsSuccInd_exp
Proof state before:
case succ
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
x : ℕ
ih : (Semiformula.Eval (standardModelExp ℕ) ![x] e) p
⊢ (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
Tactic:
exact hsucc x ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Standard.modelsTheory_elementaryArithmetic
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ℕ ⊧ₘ* 𝐄𝐀
Tactic:
simp [Theory.elementaryArithmetic, Theory.indScheme]
Proof state after:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ((∀ i ∈ 𝐏𝐀⁻, (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) i) ∧ ℕ ⊧ₘ* 𝐄𝐗𝐏) ∧
    ∀ (f : Sentence ℒₒᵣ(exp)) (x : Semiformula ℒₒᵣ(exp) ℕ 1),
      Hierarchy 𝚺 0 x → f = ∀ᶠ* succInd x → (standardModelExp ℕ).toStruc ⊧ f
Theorem: LO.FirstOrder.Arith.Standard.modelsTheory_elementaryArithmetic
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ((∀ i ∈ 𝐏𝐀⁻, (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) i) ∧ ℕ ⊧ₘ* 𝐄𝐗𝐏) ∧
    ∀ (f : Sentence ℒₒᵣ(exp)) (x : Semiformula ℒₒᵣ(exp) ℕ 1),
      Hierarchy 𝚺 0 x → f = ∀ᶠ* succInd x → (standardModelExp ℕ).toStruc ⊧ f
Tactic:
exact ⟨⟨by intro σ hσ; simpa [models_iff] using models_peanoMinus.realize hσ, models_exponential⟩,
  by rintro σ p _ rfl; exact modelsSuccInd_exp p⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Standard.modelsTheory_elementaryArithmetic
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ∀ i ∈ 𝐏𝐀⁻, (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) i
Tactic:
intro σ hσ
Proof state after:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
σ : Semiformula ℒₒᵣ Empty 0
hσ : σ ∈ 𝐏𝐀⁻
⊢ (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) σ
Theorem: LO.FirstOrder.Arith.Standard.modelsTheory_elementaryArithmetic
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
σ : Semiformula ℒₒᵣ Empty 0
hσ : σ ∈ 𝐏𝐀⁻
⊢ (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) σ
Tactic:
simpa [models_iff] using models_peanoMinus.realize hσ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Standard.modelsTheory_elementaryArithmetic
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ∀ (f : Sentence ℒₒᵣ(exp)) (x : Semiformula ℒₒᵣ(exp) ℕ 1),
    Hierarchy 𝚺 0 x → f = ∀ᶠ* succInd x → (standardModelExp ℕ).toStruc ⊧ f
Tactic:
rintro σ p _ rfl
Proof state after:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
a✝ : Hierarchy 𝚺 0 p
⊢ (standardModelExp ℕ).toStruc ⊧ ∀ᶠ* succInd p
Theorem: LO.FirstOrder.Arith.Standard.modelsTheory_elementaryArithmetic
Proof state before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
a✝ : Hierarchy 𝚺 0 p
⊢ (standardModelExp ℕ).toStruc ⊧ ∀ᶠ* succInd p
Tactic:
exact modelsSuccInd_exp p
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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₃!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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)
Proof 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✝
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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₀);
Proof 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✝
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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₀);
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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
Proof 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✝
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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₀)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof 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
Proof 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✝