internlm/Lean-Github huggingface dataset:
Theorem: Primrec.list_take
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec₂ fun s a => Nat.rec [] (fun n as => as ++ (a.get? n).toList) s
n : ℕ
as : List α
⊢ Nat.rec [] (fun n as_1 => as_1 ++ (as.get? n).toList) n = List.take n as
Tactic:
induction' n with n ih <;> simp[List.take_succ, *]
Proof state after:
no goals
Theorem: Primrec.list_lookup
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
⊢ Primrec₂ List.lookup
Tactic:
have : Primrec₂ (fun p q => bif p.1 == q.1.1 then q.1.2 else q.2.2 : α × List (α × β) → (α × β) × List (α × β) × Option β → Option β) :=
  cond (Primrec.beq.comp (fst.comp fst) (fst.comp $ fst.comp snd))
    (option_some.comp $ snd.comp $ fst.comp snd) (snd.comp $ snd.comp snd)
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
⊢ Primrec₂ List.lookup
Theorem: Primrec.list_lookup
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
⊢ Primrec₂ List.lookup
Tactic:
have : Primrec₂ (fun a l => List.recOn l none (fun p _ ih => bif a == p.1 then p.2 else ih) : α → List (α × β) → Option β) :=
  to₂ <| list_rec snd (const none) this
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
⊢ Primrec₂ List.lookup
Theorem: Primrec.list_lookup
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
⊢ Primrec₂ List.lookup
Tactic:
exact this.of_eq <| fun a ps => by
  induction' ps with p ps <;> simp[List.lookup, *]
  cases ha : a == p.1 <;> simp[ha]
Proof state after:
no goals
Theorem: Primrec.list_lookup
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
a : α
ps : List (α × β)
⊢ (List.recOn ps none fun p x ih => bif a == p.1 then some p.2 else ih) = List.lookup a ps
Tactic:
induction' ps with p ps <;> simp[List.lookup, *]
Proof state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
a : α
p : α × β
ps : List (α × β)
tail_ih✝ : (List.recOn ps none fun p x ih => bif a == p.1 then some p.2 else ih) = List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match a == p.1 with
    | true => some p.2
    | false => List.lookup a ps
Theorem: Primrec.list_lookup
Proof state before:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
a : α
p : α × β
ps : List (α × β)
tail_ih✝ : (List.recOn ps none fun p x ih => bif a == p.1 then some p.2 else ih) = List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match a == p.1 with
    | true => some p.2
    | false => List.lookup a ps
Tactic:
cases ha : a == p.1 <;> simp[ha]
Proof state after:
no goals
Theorem: Primrec.nat_omega_rec_prod
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
⊢ Primrec₂ f
Tactic:
have hm : Primrec (fun p => p.2 : α × ℕ → ℕ) := snd
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
⊢ Primrec₂ f
Theorem: Primrec.nat_omega_rec_prod
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
⊢ Primrec₂ f
Tactic:
have hl : Primrec (fun p => (List.range p.2).map fun x => (t p.1 p.2, x) : α × ℕ → List (α × ℕ)) :=
  list_map (list_range.comp snd) (Primrec₂.pair.comp₂ (ht.comp₂ (fst.comp₂ Primrec₂.left) (snd.comp₂ Primrec₂.left)) Primrec₂.right)
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
⊢ Primrec₂ f
Theorem: Primrec.nat_omega_rec_prod
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
⊢ Primrec₂ f
Tactic:
have := nat_omega_rec' (fun (p : α × ℕ) => f p.1 p.2) hm hl hg (by simp) (by rintro ⟨a, k⟩; simp[Function.comp, H])
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
this : Primrec fun p => f p.1 p.2
⊢ Primrec₂ f
Theorem: Primrec.nat_omega_rec_prod
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
this : Primrec fun p => f p.1 p.2
⊢ Primrec₂ f
Tactic:
exact to₂ this
Proof state after:
no goals
Theorem: Primrec.nat_omega_rec_prod
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
⊢ ∀ (b b' : α × ℕ), b' ∈ List.map (fun x => (t b.1 b.2, x)) (List.range b.2) → b'.2 < b.2
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec.nat_omega_rec_prod
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
⊢ ∀ (b : α × ℕ),
    g b (List.map (fun p => f p.1 p.2) (List.map (fun x => (t b.1 b.2, x)) (List.range b.2))) =
      some ((fun p => f p.1 p.2) b)
Tactic:
rintro ⟨a, k⟩
Proof state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
a : α
k : ℕ
⊢ g (a, k) (List.map (fun p => f p.1 p.2) (List.map (fun x => (t (a, k).1 (a, k).2, x)) (List.range (a, k).2))) =
    some ((fun p => f p.1 p.2) (a, k))
Theorem: Primrec.nat_omega_rec_prod
Proof state before:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
a : α
k : ℕ
⊢ g (a, k) (List.map (fun p => f p.1 p.2) (List.map (fun x => (t (a, k).1 (a, k).2, x)) (List.range (a, k).2))) =
    some ((fun p => f p.1 p.2) (a, k))
Tactic:
simp[Function.comp, H]
Proof state after:
no goals
Theorem: LO.FirstOrder.ProvabilityPredicate.kreisel_spec
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
⊢ T₀ ⊢! κ(σ) ⟷ (⦍β⦎κ(σ) ⟶ σ)
Tactic:
convert (diag (T := T₀) “x | !β.prov x → !σ”)
Proof state after:
case h.e'_5.h.e'_4
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
⊢ ⦍β⦎κ(σ) ⟶ σ = [→ ⸢fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ)⸣].hom ([→ #0].hom β.prov ⟶ [→ ].hom σ)
Theorem: LO.FirstOrder.ProvabilityPredicate.kreisel_spec
Proof state before:
case h.e'_5.h.e'_4
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
⊢ ⦍β⦎κ(σ) ⟶ σ = [→ ⸢fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ)⸣].hom ([→ #0].hom β.prov ⟶ [→ ].hom σ)
Tactic:
simp [kreisel, ←Rew.hom_comp_app, Rew.substs_comp_substs]
Proof state after:
case h.e'_5.h.e'_4
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
⊢ ⦍β⦎fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ) = [→ ⸢fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ)⸣].hom β.prov
Theorem: LO.FirstOrder.ProvabilityPredicate.kreisel_spec
Proof state before:
case h.e'_5.h.e'_4
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
⊢ ⦍β⦎fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ) = [→ ⸢fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ)⸣].hom β.prov
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.ProvabilityPredicate.loeb_theorm
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
H : T ⊢! ⦍β⦎σ ⟶ σ
⊢ T ⊢! σ
Tactic:
have d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ := imp_trans! (Subtheory.prf! (kreisel_specAux₁ σ)) H
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
H : T ⊢! ⦍β⦎σ ⟶ σ
d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ
⊢ T ⊢! σ
Theorem: LO.FirstOrder.ProvabilityPredicate.loeb_theorm
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
H : T ⊢! ⦍β⦎σ ⟶ σ
d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ
⊢ T ⊢! σ
Tactic:
have d₂ : T ⊢! ⦍β⦎κ(σ)      := Subtheory.prf! (𝓢 := T₀) (D1 $ Subtheory.prf! (kreisel_specAux₂ σ) ⨀ d₁)
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
H : T ⊢! ⦍β⦎σ ⟶ σ
d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ
d₂ : T ⊢! ⦍β⦎κ(σ)
⊢ T ⊢! σ
Theorem: LO.FirstOrder.ProvabilityPredicate.loeb_theorm
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
H : T ⊢! ⦍β⦎σ ⟶ σ
d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ
d₂ : T ⊢! ⦍β⦎κ(σ)
⊢ T ⊢! σ
Tactic:
exact d₁ ⨀ d₂
Proof state after:
no goals
Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_loeb_theorem
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Tactic:
have hκ₁ : T₀ ⊢! ⦍β⦎(κ(σ)) ⟶ ⦍β⦎σ := kreisel_specAux₁ σ
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_loeb_theorem
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Tactic:
have : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ (⦍β⦎κ(σ) ⟶ σ) := imply_left_replace! hκ₁
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
this : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎κ(σ) ⟶ σ
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_loeb_theorem
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
this : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎κ(σ) ⟶ σ
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Tactic:
have : T ⊢! (⦍β⦎σ ⟶ σ) ⟶ κ(σ) := Subtheory.prf! (𝓢 := T₀) $ imp_trans! this (kreisel_specAux₂ σ)
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
this✝ : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎κ(σ) ⟶ σ
this : T ⊢! (⦍β⦎σ ⟶ σ) ⟶ κ(σ)
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_loeb_theorem
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
this✝ : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎κ(σ) ⟶ σ
this : T ⊢! (⦍β⦎σ ⟶ σ) ⟶ κ(σ)
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Tactic:
exact imp_trans! (D2 ⨀ (D1 this)) hκ₁
Proof state after:
no goals
Theorem: LO.FirstOrder.ProvabilityPredicate.unprovable_consistency_of_Loeb
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
⊢ Consistent T → T ⊬! ~⦍β⦎⊥
Tactic:
contrapose
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
⊢ ¬T ⊬! ~⦍β⦎⊥ → ¬Consistent T
Theorem: LO.FirstOrder.ProvabilityPredicate.unprovable_consistency_of_Loeb
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
⊢ ¬T ⊬! ~⦍β⦎⊥ → ¬Consistent T
Tactic:
intro hC
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : ¬T ⊬! ~⦍β⦎⊥
⊢ ¬Consistent T
Theorem: LO.FirstOrder.ProvabilityPredicate.unprovable_consistency_of_Loeb
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : ¬T ⊬! ~⦍β⦎⊥
⊢ ¬Consistent T
Tactic:
simp [neg_equiv'!] at hC
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
⊢ ¬Consistent T
Theorem: LO.FirstOrder.ProvabilityPredicate.unprovable_consistency_of_Loeb
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
⊢ ¬Consistent T
Tactic:
have : T ⊢! ⊥ := Loeb.LT T₀ hC
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
this : T ⊢! ⊥
⊢ ¬Consistent T
Theorem: LO.FirstOrder.ProvabilityPredicate.unprovable_consistency_of_Loeb
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
this : T ⊢! ⊥
⊢ ¬Consistent T
Tactic:
apply System.not_consistent_iff_inconsistent.mpr
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
this : T ⊢! ⊥
⊢ Inconsistent T
Theorem: LO.FirstOrder.ProvabilityPredicate.unprovable_consistency_of_Loeb
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
this : T ⊢! ⊥
⊢ Inconsistent T
Tactic:
apply System.inconsistent_of_provable this
Proof state after:
no goals
Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_second
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
H : T ⊬! ~Con⦍β⦎
⊢ T ⊬! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
Tactic:
by_contra hC
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
H : T ⊬! ~Con⦍β⦎
hC : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
⊢ False
Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_second
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
H : T ⊬! ~Con⦍β⦎
hC : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
⊢ False
Tactic:
have : T ⊢! ~Con⦍β⦎ := Loeb.LT T₀ $ contra₁'! hC
Proof state after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
H : T ⊬! ~Con⦍β⦎
hC : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
this : T ⊢! ~Con⦍β⦎
⊢ False
Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_second
Proof state before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
H : T ⊬! ~Con⦍β⦎
hC : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
this : T ⊢! ~Con⦍β⦎
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.F_primrec
Proof state before:
μ : Type ?u.22616
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
inst✝ : Primcodable μ
⊢ Primrec₂ fun p f => decide (Semiformula.rel f.snd.1 f.snd.2 ∈ p.1.1)
Tactic:
apply list_mem.comp₂ (Semiformula.rel_primrec.comp₂ Primrec₂.right) (fst.comp₂ $ fst.comp₂ Primrec₂.left)
Proof state after:
no goals