Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main (Logic/FirstOrder/Incompleteness/SelfReference.lean)

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type ?u.32377
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ fixpoint θ ⟷ [→ ⸢fixpoint θ⸣].hom θ
Tactic:
haveI : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_provably_subtheory M 𝐏𝐀⁻ T inferInstance (by assumption)
State after:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type ?u.32377
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ M ⊧ₘ fixpoint θ ⟷ [→ ⸢fixpoint θ⸣].hom θ

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type ?u.32377
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ M ⊧ₘ fixpoint θ ⟷ [→ ⸢fixpoint θ⸣].hom θ
Tactic:
have hssbs : ∀ σ π : Semisentence ℒₒᵣ 1, ∀ z,
    Evalbm M ![z, encode σ, encode π] ssbs ↔ z = encode (σ/[(⸢π⸣ : Semiterm ℒₒᵣ Empty 0)]) := by
  simpa [goedelNumber_def, Model.numeral_eq_natCast, models_iff, Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using
  fun σ π => consequence_iff'.mp (sound₀! (ssbs_spec (T := T) σ π)) M
State after:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ M ⊧ₘ fixpoint θ ⟷ [→ ⸢fixpoint θ⸣].hom θ

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ M ⊧ₘ fixpoint θ ⟷ [→ ⸢fixpoint θ⸣].hom θ
Tactic:
simp[models_iff, Semiformula.eval_substs, Matrix.comp_vecCons']
State after:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ (Evalf (standardModel M) Empty.elim) (fixpoint θ) ↔
    (Eval (standardModel M)
        (fun i => Semiterm.Operator.val (Semiterm.Operator.GoedelNumber.goedelNumber (fixpoint θ)) ![]) Empty.elim)
      θ

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ (Evalf (standardModel M) Empty.elim) (fixpoint θ) ↔
    (Eval (standardModel M)
        (fun i => Semiterm.Operator.val (Semiterm.Operator.GoedelNumber.goedelNumber (fixpoint θ)) ![]) Empty.elim)
      θ
Tactic:
suffices Evalbm M ![] (fixpoint θ) ↔ Evalbm M ![encode (fixpoint θ)] θ by
  simpa [goedelNumber_def, Model.numeral_eq_natCast, Matrix.constant_eq_singleton] using this
State after:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ (Evalbm M ![]) (fixpoint θ) ↔ (Evalbm M ![↑(encode (fixpoint θ))]) θ

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ (Evalbm M ![]) (fixpoint θ) ↔ (Evalbm M ![↑(encode (fixpoint θ))]) θ
Tactic:
calc
  Evalbm M ![] (fixpoint θ)
  ↔ ∀ z, Evalbm M ![z, encode (diag θ), encode (diag θ)] ssbs → Evalbm M ![z] θ := by simp [goedelNumber_def,
                                                                                        fixpoint_eq, Semiformula.eval_rew,
                                                                                        Function.comp, Matrix.comp_vecCons',
                                                                                        Matrix.constant_eq_vec₂,
                                                                                        Model.numeral_eq_natCast,
                                                                                        Matrix.constant_eq_singleton]
_ ↔ Evalbm M ![encode “!(diag θ) !!(⸢diag θ⸣ : Semiterm ℒₒᵣ Empty 0)”] θ        := by simp [hssbs]
_ ↔ Evalbm M ![encode (fixpoint θ)] θ                                           := by rfl
State after:
no goals

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type ?u.32377
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

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type ?u.32377
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
Tactic:
simpa [goedelNumber_def, Model.numeral_eq_natCast, models_iff, Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using
fun σ π => consequence_iff'.mp (sound₀! (ssbs_spec (T := T) σ π)) M
State after:
no goals

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this✝ : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
this : (Evalbm M ![]) (fixpoint θ) ↔ (Evalbm M ![↑(encode (fixpoint θ))]) θ
⊢ (Evalf (standardModel M) Empty.elim) (fixpoint θ) ↔
    (Eval (standardModel M)
        (fun i => Semiterm.Operator.val (Semiterm.Operator.GoedelNumber.goedelNumber (fixpoint θ)) ![]) Empty.elim)
      θ
Tactic:
simpa [goedelNumber_def, Model.numeral_eq_natCast, Matrix.constant_eq_singleton] using this
State after:
no goals

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ (Evalbm M ![]) (fixpoint θ) ↔
    ∀ (z : M), (Evalbm M ![z, ↑(encode (diag θ)), ↑(encode (diag θ))]) ssbs → (Evalbm M ![z]) θ
Tactic:
simp [goedelNumber_def,
  fixpoint_eq, Semiformula.eval_rew,
  Function.comp, Matrix.comp_vecCons',
  Matrix.constant_eq_vec₂,
  Model.numeral_eq_natCast,
  Matrix.constant_eq_singleton]
State after:
no goals

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ (∀ (z : M), (Evalbm M ![z, ↑(encode (diag θ)), ↑(encode (diag θ))]) ssbs → (Evalbm M ![z]) θ) ↔
    (Evalbm M ![↑(encode ([→ ⸢diag θ⸣].hom (diag θ)))]) θ
Tactic:
simp [hssbs]
State after:
no goals

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ (Evalbm M ![↑(encode ([→ ⸢diag θ⸣].hom (diag θ)))]) θ ↔ (Evalbm M ![↑(encode (fixpoint θ))]) θ
Tactic:
rfl
State after:
no goals