Gödel's first incompleteness theorem

Stream: general

[Palalansoukî]

A few weeks ago, I successfully proved Gödel's first incompleteness theorem using Lean, You can find the details on my GitHub repository here, likely the first of its kind, accoding to Missing theorems from Freek Wiedijk's list of 100 theorems (Do I need to write a paper or something to update this list?). I would greatly appreciate your insights to ensure the accuracy of the proof.

Furthermore, there's an ongoing attempt within Mathlib to prove the incompleteness theorem, as mentioned here. I'm interested in contributing to this effort. Given the potentially different definitions in use, a direct transplant might be challenging. Regardless, is there something I can make a contribution? I'm considering porting some theorems about computability to Mathlib.

[Aaron Anderson]

Great work!

[Aaron Anderson]

I'm the one who made that note about that approach to incompleteness - along with adding most of the Model_Theory folder, building initially on work by @Floris van Doorn and @Jesse Michael Han.
I haven't had much time to work on mathlib for a while, so I'm unlikely to try very hard to work on that direction soon.

[Aaron Anderson]

Thus I'm not sure what I'd recommend as an immediate next step, but I'd be happy to talk over potential plans.

[Alex J. Best]

Regarding updating freeks list. If you make a PR to mathlib editing the file docs/100.yaml adding a link to your repo (you can look at independence of CH as an example for the format), this will update the mathlib website. One of the maintainers generally emails freek periodically to ask him to update his page with our new theorems I think rather than mailing him every time, but this may indeed be a good opportunity for someone to mail him.

[Ruben Van de Velde]

If we pick up the fundamental theorem of symmetric polynomials and Lindemann, there'd be even more :)

[Palalansoukî]

Aaron Anderson said:

Thus I'm not sure what I'd recommend as an immediate next step, but I'd be happy to talk over potential plans.

In the context of the computability of formulae and terms, Lean4-logic has proven the primitive recursiveness of the WType satisfying some conditions. Link to the proof. I believe this approach presents several advantages compared to current strategies.

1. The recursion of WType is likely simpler and more straightforward to prove than specific recursion for formulae and terms.

2. Many countable types, including formula and term, are isomorphic to WType or its subtypes. This fact enables us to prove that numerous types are Primcodable, and their recursion is primitive recursive.

One issue with this approach is its significant inefficiency (for example, encode “0 = 1” is too huge for computers to handle). but from a mathematical standpoint, there may be no problem.

[Palalansoukî]

Additionally, it is necessary to prove that the graph of partial recursive functions can be expressed in $\Sigma_1$ formula of arithmetic​. This is proved by the equivalence of the class ArithPart₁ (the name might be inappropriate; Sigma₁ might be more suitable?) defined below and the class Primrec'.

inductive ArithPart₁ : ∀ {n}, (Vector ℕ n →. ℕ) → Prop
  | zero {n} : @ArithPart₁ n (fun _ => 0)
  | one {n} : @ArithPart₁ n (fun _ => 1)
  | add {n} (i j : Fin n) : @ArithPart₁ n (fun v => v.get i + v.get j : Vector ℕ n → ℕ)
  | mul {n} (i j : Fin n) : @ArithPart₁ n (fun v => v.get i * v.get j : Vector ℕ n → ℕ)
  | proj {n} (i : Fin n) : @ArithPart₁ n (fun v => v.get i : Vector ℕ n → ℕ)
  | equal {n} (i j : Fin n) : @ArithPart₁ n (fun v => isEqNat (v.get i) (v.get j) : Vector ℕ n → ℕ)
  | lt {n} (i j : Fin n) : @ArithPart₁ n (fun v => isLtNat (v.get i) (v.get j) : Vector ℕ n → ℕ)
  | comp {m n f} (g : Fin n → Vector ℕ m →. ℕ) :
    ArithPart₁ f → (∀ i, ArithPart₁ (g i)) → ArithPart₁ fun v => (mOfFn fun i => g i v) >>= f
  | rfind {n} {f : Vector ℕ (n + 1) → ℕ} :
    ArithPart₁ (n := n + 1) f → ArithPart₁ (fun v => rfind fun n => some (f (n ::ᵥ v) = 0))

I believe proving this fact in Mathlib is relatively straightforward. Initially, I am considering porting these two to Mathlib.

[Hunter Monroe]

Congratulations @Palalansoukî; this is impressive. I would be interested to help port this to mathlib. The work seems huge even focusing on key theorems--submitting additions outside logic, removing overlaps, adding documentation, etc. There are 11K lines over 50 files and maintainers prefer 30-300 lines per PR. A good place to start might be the first two hundred lines of arith that would add to Nat and then additions elsewhere.

[Palalansoukî]

Many of the theorems proved in Arith (mainly about Gödel's beta function lemma and computability) are natural extensions of Mathlib, and I agree that Arith is certainly a good place to start.

[Hunter Monroe]

We have submitted PR #8887 which incorporates code for Godel's Beta Function, drawing from the lean4-logic repository. 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.

[Hunter Monroe]

@Mario Carneiro could you look at #8619, which will eventually be needed to include Godel's First Incompleteness Theorem in mathlib, from lean4-logic? Lean4-logic by @Palalansoukî uses nat_omega_rec in several places. Many thanks.

[Hunter Monroe]

@Mario Carneiro could you help with two strategic questions? First, what would be a sensible likely successful approach to including @Palalansoukî proof of Gödel's first incompleteness theorem and possibly Godel's completeness theorem in mathlib? Is this a realistic endeavor? His repository logic4-lean has 10K lines of code--so should the emphasis be on extracting minimal proofs that integrate tightly with mathlib's code on model theory etc? As suggested by @Eric Wieser he has separated some coprime theorems #9005 from Godel's Beta Function #8887, and his proof also depends on #8619 which you have seen.

Second, what would represent a minimum viable pull request on complexity theory? My PR #8931 has definitions of P, NP, NP-Completeness, and poly time reductions, without theorems. I could readily add an example of a language in P and NP, consisting of every bit string, with a TM that returns "[true]" on any input. Going further eg an example of NP completeness would require universal TM via bounded halting, and Cook Levin is even harder. Showing that poly time reducibility is transitive would require composability of TMs. After rereading three years of discussions and seeing all the failed PRs, I wanted to understand what is needed for a successful PR before investing more time.

Thanks!

[Mario Carneiro]

My main suggestion is to break things into small pieces and make sure that things are integrated well with the rest of the library

[Mario Carneiro]

#8931 is a bit too definition-heavy. I think a MVP PR should have one definition and a handful of theorems about it

[Mario Carneiro]

like, even the BitString definition is likely to cause discussion

[Hunter Monroe]

It is impossible to define whether an arbitrary type is in P. With a unary alphabet, P=NP. With a sufficiently inefficient encoding, anything computable is in P (use unary and append the time to halt with separator character). If the encoding encrypts strings, nothing is in P (if one way functions exist). Replacing BitString (List Bool) with List Γ with a finite nonunary alphabet is an option. I will hold off on any work until that issue is sorted out. (My tone is exaggerated on purpose, tell me if I have missed the point.)

[Mario Carneiro]

Note that Primcodable is built to handle exactly this issue

[Mario Carneiro]

it doesn't really matter if weird instances exist, because we use canonical instances to prove all the interesting theorems

[Martin Dvořák]

Mario Carneiro said:

like, even the BitString definition is likely to cause discussion

Because it should be abbrev instead?