 Moving now to stronger theories beyond PA, one can mention, for example, Kruskal’s Theorem. This is a theorem which concerns certain orderings of finite trees (Kruskal 1960). Harvey Friedman showed that this theorem is unprovable even in subsystems of second-order arithmetic much stronger than PA (see Simpson 1985). In particular, it is not provable in any theory which is predicatively justified (under a widely accepted explication of “predicative”, cf. the section on predicativism in the entry on the  philosophy of mathematics).