Finite form of the graph minor theorem

Statement

Friedman, Robertson & Seymour (1987) showed that the following theorem exhibits the independence phenomenon by being unprovable in various formal systems that are much stronger than Peano arithmetic, yet being provable in systems much weaker than ZFC:

(Here, the size of a graph is the total number of its vertices and edges, and ≤ denotes the minor ordering.)

Friedman uses this result on simple subcubic graphs to construct the fast-growing function, SSCG.