internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Standard.models_succInd
Proof state before:
n : ℕ
μ : Type v
e✝ : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModel ℕ) ![0] e) p
hsucc : ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] e) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
x : ℕ
⊢ (Semiformula.Eval (standardModel ℕ) ![x] e) p
Tactic:
induction' x with x ih
Proof state after:
case zero
n : ℕ
μ : Type v
e✝ : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModel ℕ) ![0] e) p
hsucc : ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] e) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
⊢ (Semiformula.Eval (standardModel ℕ) ![0] e) p

case succ
n : ℕ
μ : Type v
e✝ : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModel ℕ) ![0] e) p
hsucc : ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] e) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
x : ℕ
ih : (Semiformula.Eval (standardModel ℕ) ![x] e) p
⊢ (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
Theorem: LO.FirstOrder.Arith.Standard.models_succInd
Proof state before:
case zero
n : ℕ
μ : Type v
e✝ : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModel ℕ) ![0] e) p
hsucc : ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] e) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
⊢ (Semiformula.Eval (standardModel ℕ) ![0] e) p
Tactic:
exact hzero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Standard.models_succInd
Proof state before:
case succ
n : ℕ
μ : Type v
e✝ : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModel ℕ) ![0] e) p
hsucc : ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] e) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
x : ℕ
ih : (Semiformula.Eval (standardModel ℕ) ![x] e) p
⊢ (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
Tactic:
exact hsucc x ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.oRing_consequence_of
Proof state before:
T : Theory ℒₒᵣ
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence ℒₒᵣ
H :
  ∀ (M : Type w) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M] [inst_5 : M ⊧ₘ* T],
    M ⊧ₘ σ
M : Type ?u.361593
x✝⁶ : Zero M
x✝⁵ : One M
x✝⁴ : Add M
x✝³ : Mul M
x✝² : LT M
s : Structure ℒₒᵣ M
x✝¹ : Structure.ORing ℒₒᵣ M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
rcases standardModel_unique M s
Proof state after:
case refl
T : Theory ℒₒᵣ
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence ℒₒᵣ
H :
  ∀ (M : Type w) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M] [inst_5 : M ⊧ₘ* T],
    M ⊧ₘ σ
M : Type ?u.361593
x✝⁶ : Zero M
x✝⁵ : One M
x✝⁴ : Add M
x✝³ : Mul M
x✝² : LT M
x✝¹ : Structure.ORing ℒₒᵣ M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Theorem: LO.FirstOrder.Arith.oRing_consequence_of
Proof state before:
case refl
T : Theory ℒₒᵣ
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence ℒₒᵣ
H :
  ∀ (M : Type w) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M] [inst_5 : M ⊧ₘ* T],
    M ⊧ₘ σ
M : Type ?u.361593
x✝⁶ : Zero M
x✝⁵ : One M
x✝⁴ : Add M
x✝³ : Mul M
x✝² : LT M
x✝¹ : Structure.ORing ℒₒᵣ M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
exact H M
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.substs_diag
Proof state before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ σ : Semisentence ℒₒᵣ 1
⊢ [→ ⸢σ⸣].hom (diag θ) = ∀' ([→ #0, ⸢σ⸣, ⸢σ⸣].hom ssbs ⟶ [→ #0].hom θ)
Tactic:
simp [diag, Rew.q_substs, ←Rew.hom_comp_app, Rew.substs_comp_substs]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.fixpoint_eq
Proof state before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
⊢ fixpoint θ = ∀' ([→ #0, ⸢diag θ⸣, ⸢diag θ⸣].hom ssbs ⟶ [→ #0].hom θ)
Tactic:
simp [fixpoint, substs_diag]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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)
Proof 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 θ
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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
Proof 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 θ
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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']
Proof 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)
      θ
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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
Proof 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 θ))]) θ
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.provableSentence_representation
Proof state before:
T : Theory ℒₒᵣ
inst✝¹⁰ : 𝐄𝐐 ≼ T
inst✝⁹ : 𝐏𝐀⁻ ≼ T
inst✝⁸ : SigmaOneSound T
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
U : Theory L
inst✝¹ : DecidablePred U
inst✝ : U.Computable
σ : Sentence L
⊢ T ⊢! [→ ⸢σ⸣].hom (provableSentence U) ↔ U ⊢! σ
Tactic:
simpa using pred_representation (T := T) (provable_RePred U) (x := σ)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.goedel_spec
Proof state before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
⊢ T ⊢! G ⟷ ~[→ ⸢G⸣].hom (provableSentence T)
Tactic:
simpa using SelfReference.main T (~provableSentence T)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ Undecidable T G
Tactic:
suffices ¬(T ⊢! G ∨ T ⊢! ~G) by
  simpa[System.Undecidable, not_or] using this
Proof state after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ ¬(T ⊢! G ∨ T ⊢! ~G)
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ ¬(T ⊢! G ∨ T ⊢! ~G)
Tactic:
rintro (H | H)
Proof state after:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
⊢ False

case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
⊢ False
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
this : ¬(T ⊢! G ∨ T ⊢! ~G)
⊢ Undecidable T G
Tactic:
simpa[System.Undecidable, not_or] using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
⊢ False
Tactic:
have h₁ : T ⊢! ~(provableSentence T)/[⸢G⸣] := System.and_left! (goedel_spec T) ⨀ H
Proof state after:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
⊢ False
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
⊢ False
Tactic:
have h₂ : T ⊢! (provableSentence T)/[⸢G⸣]  := by simpa using (provableSentence_representation (L := ℒₒᵣ)).mpr H
Proof state after:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
h₂ : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
h₂ : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Tactic:
exact (Gentzen.inconsistent_of_provable_and_refutable! h₂ h₁).not_con (consistent_of_sigmaOneSound T)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
⊢ T ⊢! [→ ⸢G⸣].hom (provableSentence T)
Tactic:
simpa using (provableSentence_representation (L := ℒₒᵣ)).mpr H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
⊢ False
Tactic:
have : T ⊢! ~G ⟷ (provableSentence T)/[⸢G⸣] := Gentzen.not_contra! (goedel_spec T)
Proof state after:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Tactic:
have : T ⊢! (provableSentence T)/[⸢G⸣] := System.and_left! this ⨀ H
Proof state after:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this✝ : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
this : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this✝ : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
this : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Tactic:
have : T ⊢! G := (provableSentence_representation (L := ℒₒᵣ)).mp this
Proof state after:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this✝¹ : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
this✝ : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
this : T ⊢! G
⊢ False
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent
Proof state before:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this✝¹ : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
this✝ : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
this : T ⊢! G
⊢ False
Tactic:
exact (Gentzen.inconsistent_of_provable_and_refutable! this H).not_con (consistent_of_sigmaOneSound T)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.trueArithWithStarUnbounded.cumulative
Proof state before:
c : ℕ
⊢ (fun n =>
      “!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ ↑n)) <
          !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”) =
    (fun n =>
        “!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ ↑n)) <
            !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”) ∘
      Fin.castSucc
Tactic:
simp[Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
letI : Structure Language.unit ℕ := modelStar c
Proof state after:
c : ℕ
this : Structure Language.unit ℕ := modelStar c
⊢ Satisfiable (trueArithWithStarUnbounded c)
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this : Structure Language.unit ℕ := modelStar c
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.Zero ℒₒᵣ⋆ ℕ := ⟨rfl⟩
Proof state after:
c : ℕ
this✝ : Structure Language.unit ℕ := modelStar c
this : Structure.Zero ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝ : Structure Language.unit ℕ := modelStar c
this : Structure.Zero ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.One ℒₒᵣ⋆ ℕ := ⟨rfl⟩
Proof state after:
c : ℕ
this✝¹ : Structure Language.unit ℕ := modelStar c
this✝ : Structure.Zero ℒₒᵣ⋆ ℕ
this : Structure.One ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝¹ : Structure Language.unit ℕ := modelStar c
this✝ : Structure.Zero ℒₒᵣ⋆ ℕ
this : Structure.One ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.Add ℒₒᵣ⋆ ℕ := ⟨fun _ _ => rfl⟩
Proof state after:
c : ℕ
this✝² : Structure Language.unit ℕ := modelStar c
this✝¹ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝ : Structure.One ℒₒᵣ⋆ ℕ
this : Structure.Add ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝² : Structure Language.unit ℕ := modelStar c
this✝¹ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝ : Structure.One ℒₒᵣ⋆ ℕ
this : Structure.Add ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.Eq ℒₒᵣ⋆ ℕ := ⟨fun _ _ => iff_of_eq rfl⟩
Proof state after:
c : ℕ
this✝³ : Structure Language.unit ℕ := modelStar c
this✝² : Structure.Zero ℒₒᵣ⋆ ℕ
this✝¹ : Structure.One ℒₒᵣ⋆ ℕ
this✝ : Structure.Add ℒₒᵣ⋆ ℕ
this : Structure.Eq ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝³ : Structure Language.unit ℕ := modelStar c
this✝² : Structure.Zero ℒₒᵣ⋆ ℕ
this✝¹ : Structure.One ℒₒᵣ⋆ ℕ
this✝ : Structure.Add ℒₒᵣ⋆ ℕ
this : Structure.Eq ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.LT ℒₒᵣ⋆ ℕ := ⟨fun _ _ => iff_of_eq rfl⟩
Proof state after:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
have : ℕ ⊧ₘ* starUnbounded c := by
  simp [starUnbounded, models_iff]; exact Fin.prop
Proof state after:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)