Goodstein function

Stream: new members

[Patrick Johnson]

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]

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

[Mario Carneiro]

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]

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]

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

[Patrick Johnson]

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]

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

[Mario Carneiro]

(it's actually a bit stronger than ZFC)

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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