Documentation

Mathlib.Logic.Godel.GodelBetaFunction

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 #

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 #

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
Instances For
    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
    Instances For
      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