Zulip Chat Archive

Stream: new members

Topic: Goodstein function

Patrick Johnson (Nov 24 2021 at 16:58):

As an exercise, I want to prove that Goodstein function is not primitive recursive. It is a function ℕ → ℕ that computes the length of the Goodstein sequence that starts with n for any (n : ℕ). However, it seems very hard to even define the function. Recursive definition requires me to prove that it terminates (that is, the function is well-founded). But the proof of termination requires Goodstein function itself to prove that something decreases in each recursive call.

My question is not how to implement the function (I want to do it myself). I just want to ask whether it is even possible? I mean, is Lean strong enough to reason about such fast-growing function? The wikipedia page says that induction on natural numbers is not strong enough to prove termination of Goodstein function. Since Lean uses nat.rec to reason about natural numbers, does it mean that the termination of Goodstein function is undecidable in Lean?

Mario Carneiro (Nov 24 2021 at 17:00):

You need to prove it by induction on ordinals up to epsilon_0, IIRC, which lean can handle

Mario Carneiro (Nov 24 2021 at 17:01):

but you don't need to go to such effort; you can define it noncomputably without much work, just give a specification of the function that isn't obviously terminating and use choice to make it into a function

Mario Carneiro (Nov 24 2021 at 17:02):

In fact, there is already a computable implementation of the ordinals below epsilon_0 at docs#onote , so you can probably adapt it to define the goodstein function

Reid Barton (Nov 24 2021 at 17:21):

Roughly speaking, Lean can define functions that are defined in ordinary mathematics. Systems like Peano arithmetic are far far weaker than this.

Patrick Johnson (Nov 25 2021 at 08:30):

So I guess Lean is as strong as ZFC, right? Are there any math papers discussing strength and consistency of the Lean's kernel?

Johan Commelin (Nov 25 2021 at 08:34):

Yes and yes. See https://github.com/digama0/lean-type-theory/releases

Mario Carneiro (Nov 25 2021 at 08:35):

(it's actually a bit stronger than ZFC)

Kevin Buzzard (Nov 25 2021 at 09:39):

while we're here, it occurred to me the other day that Lean might be slightly weaker than ZFC+Grothendieck's axiom, which says "every set is in a universe", even though every type is in some Type u. Because Lean only demands countably infinitely many universes, whereas Grothendieck I think forces uncountably many. Am I mistaken?

Mario Carneiro (Nov 25 2021 at 09:43):

Yes, that's correct. TG is strictly stronger than ZFC + omega inaccessibles, it is equivalent to ZFC + a proper class of inaccessibles

Mario Carneiro (Nov 25 2021 at 09:50):

The reason for the distinction despite the apparent truth of "every set is in a universe" in lean is that ZFC, unlike lean, has the language to talk about sets that cross the universe hierarchy. In ZFC + omega inaccessibles you can form the set of all omega inaccessibles, and this set (which is only countable, so "small" in some sense) is not contained in an inaccessible. In lean there is no such counterexample set because all sets are stratified into a universe, so the TG axiom gives you no extra power.

Kevin Buzzard (Nov 25 2021 at 11:18):

I suspect that SGA4 would work fine with just countably infinitely many universes but I am not an expert.

Last updated: Dec 20 2023 at 11:08 UTC