In article <email@example.com>, Keith Ramsay <firstname.lastname@example.org> wrote:
>I don't think it's so hard to see that the way one ordinarily proves >induction up to Gamma_0 is impredicative. It's not that it's impossible >to define it predicatively. Each computable ordinal can be defined >as an ordering on natural numbers, given by a primitive recursive >relation on them. The existence of this ordering isn't the problem. >The problem is proving induction up to it. The way that one ordinarily >does it makes reference to sets of ordinals. That's the gist of it. To >show that this is not a merely apparent obstacle to a predicative >proof is a longer story.
I'd love to hear a bit more of the story, especially if you can tell it in a charming and not too rigorous manner. In particular, nothing in the paragraph says what's special about Gamma_0. For example, suppose I have an ordinal smaller than Gamma_0. How can I give a "predicative" proof of induction up to that ordinal? What breaks down at Gamma_0?