Unprovability threshold for the planar graph minor theorem

This note is part of the implementation of a programme in foundations of mathematics to find exact threshold versions of all mathematical unprovability results known so far, a programme initiated by Weiermann. Here we find the exact versions of unprovability of the finite graph minor theorem with growth rate condition restricted to planar graphs, connected planar graphs and graphs embeddable into a given surface, assuming an unproved conjecture (*): ‘there is a number a > 0 such that for all k ≥ 3 , and all n ≥ 1 , the proportion of connected graphs among unlabelled planar graphs of size n omitting the k -element circle as minor is greater than a ’. Let γ be the unlabelled planar growth constant ( 27.2269 ≤ γ < 30.061 ) . Let P ( c ) be the following first-order arithmetical statement with real parameter c : “for every K there is N such that whenever G 1 , G 2 , … , G N are unlabelled planar graphs with | G i | < K + c ⋅ log 2 i then for some i < j ≤ N , G i is isomorphic to a minor of G j ”. Then 1. ery c ≤ 1 log 2 γ , P ( c ) is provable in I Δ 0 + exp ; ery c > 1 log 2 γ , P ( c ) is unprovable in ATR 0 . so give proofs of some upper and lower bounds for unprovability thresholds in the general case of the finite graph minor theorem.