Gödel's Beta Function Lemma

This file proves Gödel's Beta Function Lemma, used to prove the First Incompleteness Theorem. It permits quantification over finite sequences of natural numbers in formal theories of arithmetic. This Beta Function has no connection with the unrelated Beta Function defined in analysis. Note that Nat.beta and Nat.unbeta provide similar functionality to Encodable.encodeList and Encodable.decodeList. We define these separately, because it is easier to prove that Nat.beta and Nat.unbeta are arithmetically definable, and this is hard to prove that for Encodable.encodeList and Encodable.decodeList directly. The arithmetic definability is needed for the proof of the First Incompleteness Theorem.

Main result

• beta_unbeta_coe: Gödel's Beta Function Lemma.

Implementation note

This code is a step towards eventually including a proof of Gödel's First Incompleteness Theorem and other key results from the repository https://github.com/iehality/lean4-logic.

References

• [R. Kaye, Models of Peano arithmetic][kaye1991]

Tags

Gödel, beta function

theorem Nat.coprime_mul_succ {n : ℕ} {m : ℕ} {a : ℕ} (h : n ≤ m) (ha : m - n ∣ a) : (n * a + 1).Coprime (m * a + 1)

theorem Nat.coprimes_lt {m : ℕ} (a : Fin m → ℕ) (i : Fin m) : a i < Nat.coprimes a i

def Nat.beta (n : ℕ) (i : ℕ) : ℕ

Gödel's Beta Function. This is similar to (Encodable.decodeList).get i, but it is easier to prove that it is arithmetically definable.

Equations

• n.beta i = n.unpair.1 % ((i + 1) * n.unpair.2 + 1)

def Nat.unbeta (l : List ℕ) : ℕ

Inverse of Gödel's Beta Function. This is similar to Encodable.encodeList, but it is easier to prove that it is arithmetically definable.

Equations

• Nat.unbeta l = (↑(Nat.chineseRemainderOfFinset l.get (Nat.coprimes l.get) Finset.univ ⋯ ⋯)).pair (Nat.supOfSeq l.get).factorial

theorem Nat.beta_unbeta_coe (l : List ℕ) (i : Fin l.length) : (Nat.unbeta l).beta ↑i = l.get i

Gödel's Beta Function Lemma