[FOM] Impredicativity of Kruskal's Theorem

[hendrik@topoi.pooq.com]

On Tue, Apr 04, 2006 at 08:20:57PM -0400, Harvey Friedman wrote:
> On 4/4/06 12:25 AM, "Nik Weaver" <nweaver at math.wustl.edu> wrote:
> 
> "Hao Wang considered the question of which ordinals are
> predicatively acceptable, and tentatively proposed an answer:
> the predicative ordinals are precisely the recursive ordinals.

When Friedman quotes Weaver here, the quote becomes quite 
intriguing.

Could it be that:
* there	is a coherent concept of "predicative", in the sense of being 
built up from below,
* that the recursive ordinals are predicative, because they are, after 
all, just recursive functions,
* but that any predicative formal system (i.e., one that formalises 
predicative concepts) will leave out some of these recursive ordinals, 
in the sense that it cannot prove them to be well-orders?

It's not clear whether this would work constructively.  Would the 
witness for the well-orderedness of those left-out ordinals be 
unobtainable?

-- hendrik