internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Tactic:
have : ∃ w, (∀ i, Vector.get w i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w := by
  simpa using Part.eq_some_iff.mp h
Proof state after:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
this : ∃ w, (∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
this : ∃ w, (∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Tactic:
rcases this with ⟨w, hw, hy⟩
Proof state after:
case mpr.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
w : Vector ℕ n✝
hw : ∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)
hy : y ∈ f w
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
case mpr.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
w : Vector ℕ n✝
hw : ∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)
hy : y ∈ f w
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Tactic:
exact ⟨w.get, (ihf y w.get).mpr (by simpa[Part.eq_some_iff] using hy),
  fun i => (ihg i (w.get i) v).mpr (by simpa[Part.eq_some_iff] using hw i)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
⊢ ∃ w, (∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w
Tactic:
simpa using Part.eq_some_iff.mp h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
w : Vector ℕ n✝
hw : ∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)
hy : y ∈ f w
⊢ f (Vector.ofFn w.get) = Part.some y
Tactic:
simpa[Part.eq_some_iff] using hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
w : Vector ℕ n✝
hw : ∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)
hy : y ∈ f w
i : Fin n✝
⊢ g i (Vector.ofFn v) = Part.some (w.get i)
Tactic:
simpa[Part.eq_some_iff] using hw i
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ ((Semiformula.Evalfm ℕ (y :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) ∧
      ∀ x < y,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel ℕ) ![x_1, x] (y :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) ↔
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Tactic:
simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons', ihf, Vector.ofFn_vecCons]
Proof state after:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0) ↔
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0) ↔
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Tactic:
constructor
Proof state after:
case mp
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0) →
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y

case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y →
    f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
case mp
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0) →
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Tactic:
rintro ⟨hy, h⟩
Proof state after:
case mp.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
case mp.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Tactic:
simp[Part.eq_some_iff]
Proof state after:
case mp.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ f (y ::ᵥ Vector.ofFn v) = 0 ∧ ∀ {m : ℕ}, m < y → ¬f (m ::ᵥ Vector.ofFn v) = 0
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
case mp.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ f (y ::ᵥ Vector.ofFn v) = 0 ∧ ∀ {m : ℕ}, m < y → ¬f (m ::ᵥ Vector.ofFn v) = 0
Tactic:
exact ⟨by simpa using hy, by intro z hz; simpa using h z hz⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ f (y ::ᵥ Vector.ofFn v) = 0
Tactic:
simpa using hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ ∀ {m : ℕ}, m < y → ¬f (m ::ᵥ Vector.ofFn v) = 0
Tactic:
intro z hz
Proof state after:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
z : ℕ
hz : z < y
⊢ ¬f (z ::ᵥ Vector.ofFn v) = 0
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
z : ℕ
hz : z < y
⊢ ¬f (z ::ᵥ Vector.ofFn v) = 0
Tactic:
simpa using h z hz
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y →
    f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
Tactic:
intro h
Proof state after:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
h : (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
⊢ f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
    ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof state before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
h : (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
⊢ f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
    ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
Tactic:
simpa using Nat.mem_rfind.mp (Part.eq_some_iff.mp h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_code
Proof state before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
hc : c.eval f
y : ℕ
v : Fin k → ℕ
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
Tactic:
simpa[code, models_iff, Semiformula.eval_rew, Matrix.empty_eq, Function.comp,
  Matrix.comp_vecCons', ←Part.eq_some_iff] using models_codeAux hc y v
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeOfPartrec_spec
Proof state before:
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)
Tactic:
have : ∃ c, ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn v) := by
  rcases Nat.ArithPart₁.exists_code (of_partrec hf) with ⟨c, hc⟩
  exact ⟨c, models_code hc⟩
Proof state after:
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
this : ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeOfPartrec_spec
Proof state before:
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
this : ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)
Tactic:
exact Classical.epsilon_spec this y v
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeOfPartrec_spec
Proof state before:
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
⊢ ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
Tactic:
rcases Nat.ArithPart₁.exists_code (of_partrec hf) with ⟨c, hc⟩
Proof state after:
case intro
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
c : Code k
hc : c.eval f
⊢ ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeOfPartrec_spec
Proof state before:
case intro
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
c : Code k
hc : c.eval f
⊢ ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
Tactic:
exact ⟨c, models_code hc⟩
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 → ℕ
⊢ 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)
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
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)
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))
⊢ 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)))
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
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)
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 σ
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) ↔ y ∈ 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
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))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_mem_partrec
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
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⟩
Proof 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)
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))
⊢ 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⟩
Proof 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)