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?

[Palalansoukî]

This is off-topic, but I've opened PR #8801 a month ago to update The Freeks List, and it hasn't been closed yet. What should I do? Do I need to provide second?

[Ruben Van de Velde]

Perhaps @Johan Commelin hasn't seen your response

[Hunter Monroe]

To include work by @Palalansoukî on Gödel's first incompleteness theorem in mathlib, there does not seem to be any movement with PRs #8887 (Gödel's beta function) and #8619 (order type omega). @Mario Carneiro , @Eric Wieser, @Floris van Doorn What is needed to move these forward? Many thanks.

[Hunter Monroe]

Mario Carneiro said:

#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 PR #9449 has a TM definition based on quintets (the one used most widely based on my research) and chainable step functions for each TM type. This PR is again definition heavy and lacking theorems. My thought was to focus on either (1) showing that the definition of polynomial time computation coincides across the TM definitions, ie. the emulations are poly time (and show the TM0 and TM quintet definition emulate each other); or (2) show that TM computations under the quintet definition can be composed, and the composition of two polynomial time computations is also poly time. Any thoughts?

[Anne Baanen]

Palalansoukî said:

This is off-topic, but I've opened PR #8801 a month ago to update The Freeks List, and it hasn't been closed yet. What should I do? Do I need to provide second?

We have discussed this among the maintainers: the consensus is that we also want the second incompleteness theorems before we consider the goal to be achieved. I am very happy to see these theorems being formalized in Lean, so I hope that this encourages you to make a completer formalization.

[Palalansoukî]

@Anne Baanen Thank you. I am currently working on the full-proof of the second incompleteness theorem at Arithmetization and will request it again when completed.

[Hunter Monroe]

@Aaron Anderson how might a mathlib proof of Godel's First Incompleteness Theorem (G1) mesh well with your Model Theory code? A natural next step toward G1 may be the Arith file from lean4logic, arithmetizing partial recursive functions. There are pending PRs for Godel's Beta Function #8887 (which Arith needs) and omega types #8619 (both seem stuck).

[Palalansoukî]

@Aaron Anderson
I would like to work on the computational facts of BoundedFormula. My plan is to prove that the induction on WType is primitive recursive, and then show that induction on formulas is also primitive recursive since formulas are a subtype of a certain WType. However, after reading ModelTheory/Encoding, it seems you have a different approach in mind. Could you share your thoughts?

[Aaron Anderson]

I can't say I had a totally well-defined plan, but I was hoping to avoid talking about primitive recursiveness or omega-consistency. My first guess for which notes to follow would be the Gödel-Rosser incompleteness section of https://math.berkeley.edu/~marks/notes/computability_notes_v1.pdf