Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq (Logic/FirstOrder/Arith/Representation.lean)

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type ?u.708404
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ (“∀' (!((Rew.substs (#0 :> fun x => ⸢v x⸣)).hom (code (codeOfPartrec ↑f))) ↔ #0 = !!⸢f (Vector.ofFn v)⸣)”)
Tactic:
haveI : M ⊧ₘ* 𝐏𝐀⁻ :=
  ModelsTheory.of_provably_subtheory M 𝐏𝐀⁻ T inferInstance (by assumption)
State after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type ?u.708404
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ M ⊧ₘ (“∀' (!((Rew.substs (#0 :> fun x => ⸢v x⸣)).hom (code (codeOfPartrec ↑f))) ↔ #0 = !!⸢f (Vector.ofFn v)⸣)”)

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
⊢ M ⊧ₘ (“∀' (!((Rew.substs (#0 :> fun x => ⸢v x⸣)).hom (code (codeOfPartrec ↑f))) ↔ #0 = !!⸢f (Vector.ofFn v)⸣)”)
Tactic:
simp [goedelNumber_def, Model.numeral_eq_natCast, models_iff, Semiformula.eval_substs, Matrix.comp_vecCons']
State after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
⊢ ∀ (x : M),
    (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f)) ↔
      x = ↑(f (Vector.ofFn v))

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
⊢ ∀ (x : M),
    (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f)) ↔
      x = ↑(f (Vector.ofFn v))
Tactic:
intro x
State after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
⊢ (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f)) ↔
    x = ↑(f (Vector.ofFn v))

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
⊢ (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f)) ↔
    x = ↑(f (Vector.ofFn v))
Tactic:
constructor
State after:
case mp
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
⊢ (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f)) →
    x = ↑(f (Vector.ofFn v))

case mpr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
⊢ x = ↑(f (Vector.ofFn v)) →
    (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f))

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type ?u.708404
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✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type ?u.708404
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
Tactic:
simpa [goedelNumber_def, Model.numeral_eq_natCast, models_iff, Semiformula.eval_substs, Matrix.comp_vecCons'] using
  consequence_iff'.mp (sound₀! (provable_iff_computable T hf v)) M
State after:
no goals

State before:
case mp
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
⊢ (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f)) →
    x = ↑(f (Vector.ofFn v))
Tactic:
intro H
State after:
case mp
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
H : (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f))
⊢ x = ↑(f (Vector.ofFn v))

State before:
case mp
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
H : (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f))
⊢ x = ↑(f (Vector.ofFn v))
Tactic:
exact code_uniq H Hfv
State after:
no goals

State before:
case mpr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
⊢ x = ↑(f (Vector.ofFn v)) →
    (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f))
Tactic:
rintro rfl
State after:
case mpr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
⊢ (Semiformula.Eval (standardModel M) (↑(f (Vector.ofFn v)) :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f))

State before:
case mpr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
⊢ (Semiformula.Eval (standardModel M) (↑(f (Vector.ofFn v)) :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f))
Tactic:
simpa
State after:
no goals