Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_mem_partrec (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
y : ℕ
v : Fin k → ℕ
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)
Tactic:
let σ : Sentence ℒₒᵣ := (Rew.substs $ ⸢y⸣ :> fun i => ⸢v i⸣).hom (code $ codeOfPartrec f)
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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) ↔ y ∈ 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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)
Tactic:
have sigma : Hierarchy 𝚺 1 σ :=
  (Hierarchy.rew (Rew.substs $ ⸢y⸣ :> fun i => ⸢v i⸣) (code_sigma_one (codeOfPartrec f)))
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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) ↔ y ∈ 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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) ↔ y ∈ 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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) → y ∈ 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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
⊢ y ∈ f (Vector.ofFn v) → T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))

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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) → y ∈ f (Vector.ofFn v)
Tactic:
rintro ⟨b⟩
State after:
case mp.intro
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
b : T ⊢ (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
⊢ y ∈ f (Vector.ofFn v)

State before:
case mp.intro
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
b : T ⊢ (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
⊢ y ∈ f (Vector.ofFn v)
Tactic:
have : Semiformula.Evalbm ℕ (y :> v) (code $ codeOfPartrec f) := by
  simpa [σ, goedelNumber_def, models_iff, Semiformula.eval_rew, Matrix.empty_eq, Function.comp, Matrix.comp_vecCons'] using
    Arith.SoundOn.sound sigma ⟨b⟩
State after:
case mp.intro
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
b : T ⊢ (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
this : (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f))
⊢ y ∈ f (Vector.ofFn v)

State before:
case mp.intro
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
b : T ⊢ (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
this : (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f))
⊢ y ∈ f (Vector.ofFn v)
Tactic:
exact (codeOfPartrec_spec hf).mp this
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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
b : T ⊢ (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f))
Tactic:
simpa [σ, goedelNumber_def, models_iff, Semiformula.eval_rew, Matrix.empty_eq, Function.comp, Matrix.comp_vecCons'] using
  Arith.SoundOn.sound sigma ⟨b⟩
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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
⊢ y ∈ f (Vector.ofFn v) → T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
Tactic:
intro h
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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
h : y ∈ f (Vector.ofFn v)
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
h : y ∈ f (Vector.ofFn v)
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
Tactic:
exact Arith.sigma_one_completeness sigma (by
  simp [goedelNumber_def, models_iff, Semiformula.eval_rew, Matrix.empty_eq,
    Function.comp, Matrix.comp_vecCons', codeOfPartrec_spec hf, h])
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
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
h : y ∈ f (Vector.ofFn v)
⊢ ℕ ⊧ₘ (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
Tactic:
simp [goedelNumber_def, models_iff, Semiformula.eval_rew, Matrix.empty_eq,
  Function.comp, Matrix.comp_vecCons', codeOfPartrec_spec hf, h]
State after:
no goals