Commit 2024-02-26 04:29 42c0da37

View on Github →

feat(Logic): Godel Beta Function (toward first incompleteness theorem) (#8887) This file proves Gödel's Beta Function Lemma, used to prove the First Incompleteness Theorem. 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.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/ChineseRemainder.lean

added def Nat.chineseRemainderOfFinset

added theorem Nat.chineseRemainderOfFinset_lt_prod

added def Nat.chineseRemainderOfList

added theorem Nat.chineseRemainderOfList_lt_prod

added theorem Nat.chineseRemainderOfList_modEq_unique

added theorem Nat.chineseRemainderOfList_nil

added theorem Nat.chineseRemainderOfList_perm

added def Nat.chineseRemainderOfMultiset

added theorem Nat.chineseRemainderOfMultiset_lt_prod

added theorem Nat.modEq_list_prod_iff'

added theorem Nat.modEq_list_prod_iff

Modified Mathlib/Data/Nat/ModEq.lean

added theorem Nat.chineseRemainder_modEq_unique

added theorem Nat.mod_eq_of_modEq

added theorem Nat.mod_lcm

Created Mathlib/Logic/Godel/GodelBetaFunction.lean

added def Nat.beta

added theorem Nat.beta_unbeta_coe

added theorem Nat.coprime_mul_succ

added theorem Nat.coprimes_lt

added def Nat.unbeta

Modified docs/references.bib