internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_mem_partrec
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_mem_partrec
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_mem_partrec
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_mem_partrec
Proof 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])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_mem_partrec
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_computable
Proof 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 → ℕ
⊢ f (Vector.ofFn v) ∈ ↑f (Vector.ofFn v)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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)
Proof 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)⸣)”)
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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']
Proof 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))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_computable_code_uniq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. σ
hf : Partrec f
x : α
y : σ
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x
Tactic:
let f' : Vector ℕ 1 →. ℕ := fun x => Part.bind (decode (α := α) x.head) fun a => (f a).map encode
Proof state after:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. σ
hf : Partrec f
x : α
y : σ
f' : Vector ℕ 1 →. ℕ := fun x => (↑(decode x.head)).bind fun a => Part.map encode (f a)
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. σ
hf : Partrec f
x : α
y : σ
f' : Vector ℕ 1 →. ℕ := fun x => (↑(decode x.head)).bind fun a => Part.map encode (f a)
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x
Tactic:
have : Nat.Partrec' f' :=
  Nat.Partrec'.part_iff.mpr
    (Partrec.bind (Computable.ofOption $ Primrec.to_comp $ Primrec.decode.comp Primrec.vector_head)
    (Partrec.to₂ <| Partrec.map (hf.comp .snd) (Computable.encode.comp₂ .right)))
Proof state after:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. σ
hf : Partrec f
x : α
y : σ
f' : Vector ℕ 1 →. ℕ := fun x => (↑(decode x.head)).bind fun a => Part.map encode (f a)
this : Nat.Partrec' f'
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. σ
hf : Partrec f
x : α
y : σ
f' : Vector ℕ 1 →. ℕ := fun x => (↑(decode x.head)).bind fun a => Part.map encode (f a)
this : Nat.Partrec' f'
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x
Tactic:
simpa [f', Matrix.constant_eq_singleton] using
  provable_iff_mem_partrec this (y := encode y) (v := ![encode x])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation_computable
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
hf : Computable f
a : α
f' : Vector ℕ 1 → ℕ := fun x => (Option.map (fun x => encode (f x)) (decode x.head)).get!
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣].hom (graphTotal f)) ↔ #0 = !!⸢f a⸣)”)
Tactic:
have : Nat.Partrec' (f' : Vector ℕ 1 →. ℕ) :=
  Nat.Partrec'.part_iff.mpr <| Computable.partrec <|
      (Primrec.option_get!).to_comp.comp <|
        Computable.option_map
          (Computable.decode.comp .vector_head) <|
            Computable.encode.comp₂ <| hf.comp₂ .right
Proof state after:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
hf : Computable f
a : α
f' : Vector ℕ 1 → ℕ := fun x => (Option.map (fun x => encode (f x)) (decode x.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣].hom (graphTotal f)) ↔ #0 = !!⸢f a⸣)”)
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation_computable
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
hf : Computable f
a : α
f' : Vector ℕ 1 → ℕ := fun x => (Option.map (fun x => encode (f x)) (decode x.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣].hom (graphTotal f)) ↔ #0 = !!⸢f a⸣)”)
Tactic:
simpa [f', Matrix.comp_vecCons', Matrix.constant_eq_singleton] using
  provable_computable_code_uniq T this ![encode a]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation_computable₂
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
hf : Computable₂ f
a : α
b : β
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
Tactic:
let f' : Vector ℕ 2 → ℕ := fun v =>
  Option.get! ((decode v.head).bind fun x => (decode v.tail.head).map fun y => (encode $ f x y))
Proof state after:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
hf : Computable₂ f
a : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation_computable₂
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
hf : Computable₂ f
a : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
Tactic:
have : Nat.Partrec' (f' : Vector ℕ 2 →. ℕ) :=
  Nat.Partrec'.part_iff.mpr <| Computable.partrec <|
      (Primrec.option_get!).to_comp.comp <|
        Computable.option_bind
          (Computable.decode.comp .vector_head) <|
            Computable.option_map
              (Computable.decode.comp $ Computable.vector_head.comp $ Computable.vector_tail.comp .fst) <|
                Computable.encode.comp₂ <| hf.comp₂ (Computable.snd.comp₂ .left) .right
Proof state after:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
hf : Computable₂ f
a : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation_computable₂
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
hf : Computable₂ f
a : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
Tactic:
simpa [f', Matrix.comp_vecCons' (fun x : ℕ => (⸢x⸣ : Semiterm ℒₒᵣ Empty 1)),
  Matrix.constant_eq_singleton, graphTotal₂] using
    provable_computable_code_uniq T this ![encode a, encode b]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.pred_representation
Proof state before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
hp : RePred p
x : α
⊢ T ⊢! [→ ⸢x⸣].hom (pred p) ↔ p x
Tactic:
simpa [pred, ←Rew.hom_comp_app, Rew.substs_comp_substs] using
  representation hp (T := T) (x := x) (y := ())
Proof state after:
no goals
Theorem: LO.Polarity.alt_alt
Proof state before:
Γ : Polarity
⊢ Γ.alt.alt = Γ
Tactic:
rcases Γ <;> simp
Proof state after:
no goals
Theorem: LO.SigmaPiDelta.alt_alt
Proof state before:
Γ : SigmaPiDelta
⊢ Γ.alt.alt = Γ
Tactic:
rcases Γ <;> simp
Proof state after:
no goals
Theorem: LO.LogicalConnective.Prop.iff_eq
Proof state before:
p q : Prop
⊢ p ⟷ q = (p ↔ q)
Tactic:
simp[LogicalConnective.iff, iff_iff_implies_and_implies]
Proof state after:
no goals
Theorem: LO.LogicalConnective.HomClass.map_iff
Proof state before:
F : Type u_1
α : outParam (Type u_2)
β : outParam (Type u_3)
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
inst✝¹ : FunLike F α β
inst✝ : HomClass F α β
f : F
a b : α
⊢ f (a ⟷ b) = f a ⟷ f b
Tactic:
simp[LogicalConnective.iff]
Proof state after:
no goals
Theorem: Matrix.conj_hom_prop
Proof state before:
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
n : ℕ
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
v : Fin n → α
⊢ f (conj v) = ∀ (i : Fin n), f (v i)
Tactic:
induction' n with n ih <;> simp[conj]
Proof state after:
case succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ f (v 0) ∧ f (conj (vecTail v)) ↔ ∀ (i : Fin (n + 1)), f (v i)