My favorite examples involve the Robinson-Seymour theorem about graph minors. For any particular class of graphs closed under graph minors (eg planar) can be c

My favorite examples involve the Robinson-Seymour theorem about graph minors. For any particular class of graphs closed under graph minors (eg planar) can be completely characterized by a finite list of minimal graphs that are not in the list (for planar graphs that list is K5 and K3,3). BUT we have no way to find the list. We have no way to bound how many things are on the list. Plus even if you were given the list, you have no way to verify it. Stronger than that, for your favorite set of axioms there are classes of graphs where, any verification that the minimal list IS the minimal list would lead to a contradiction! So..in what sense does this list exist? And in what sense is it finite?