Theorem: LO.FirstOrder.Arith.sigma_one_completeness (Logic/FirstOrder/Arith/PeanoMinus.lean)

State before:
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
haveI : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_provably_subtheory M 𝐏𝐀⁻ T inferInstance (by assumption)
State after:
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ M ⊧ₘ σ

State before:
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ M ⊧ₘ σ
Tactic:
simpa [Matrix.empty_eq] using Model.pval_of_pval_nat_of_sigma_one (M := M) hσ H
State after:
no goals

State before:
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ* T
Tactic:
assumption
State after:
no goals