Harvey M. Friedman Internal finite tree embeddings
Wilfried Sieg, Richard Sommer, Carolyn Talcott · 2002
Introduction. The present author demonstrated the first example of a predicatively meaningful but predicatively unprovable theorem from the standard mathematical literature. The example was J. B. Kruskal’s tree embedding the orem concerning infinite sequences of finite trees. See [Kr60] and [NW65] for proofs of this theorem, and [Si85] for the independence result (based on [Fr81], [Fr82]).