[FOM] 279:Subcubic Graph Numbers/restated

[Harvey Friedman]

In my http://www.cs.nyu.edu/pipermail/fom/2006-April/010305.html I worked
with finite simple subcubic graphs.

There was no good reason for imposing "simple" on the subcubic graphs. (If
we were considering graphs with unbounded valence, then we could not allow
multiple edges for finite statements).

So we restate the results without the word "simple". The proofs that I gave
do NOT have to be modified.

*******************************

We now discuss numbers associated with the graph minor theorem applied to
subcubic graphs.

A subcubic graph is a graph where every vertex has valence at most 3. Loops
and multiple edges are allowed.

Robertson and Seymour remarked in paper [1] that they could use subcubic
graphs in their derivation of my EKT, and even require that the graphs be
planar and trivalent (every vertex has valence exactly 3).

THEOREM 1. "The finite subcubic graphs are wqo under homeomorphic
embeddability" cannot be proved in Pi11-CA0. This is true even if we require
that the graphs be planar.

[1] H. Friedman, N. Robertson and P. Seymour, The Metamathematics of the
Graph Minor Theorem, Logic and Combinatorics, ed. S. Simpson,
AMS Contemporary Mathematics Series, vol. 65, 1987, 229-261.

In this reference, see page 231, the paragraph beginning with "Robertson and
Seymour...".

We now want to extract a gigantic number out of this situation, as we have
previously with Kruskal's theorem with our TREE[3].
http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html

Accordingly, let SCG(k) be the longest sequence of subcubic graphs
G1,...,Gn such that each Gi has at most i+k vertices and for no i < j is Gi
homeomorphically embeddable into Gj. (Here SCG stands for subcubic graphs).

THEOREM 2. SCG(13) is larger than the halting time of any Turing machine at
the blank tape, that can be proved to halt in at most 2^[2000] symbols in
Pi11-CA0. In particular, every proof of "SSCG(13) exists" in Pi11-CA0 has
more than 2^[1000] symbols.

It is easily seen that TREE[3] is completely UNNOTICEABLE in comparison to
SCG(13). 

**********************************

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 278th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM
255. Controlling Pi01  11/12  5:10PM
256. NAME:finite inclusion theory  11/21/05  2:34AM
257. FIT/more  11/22/05  5:34AM
258. Pi01/Simplification/Restatement  11/27/05  2:12AM
259. Pi01 pointer  11/30/05  10:36AM
260. Pi01/simplification  12/3/05  3:11PM
261. Pi01/nicer  12/5/05  2:26AM
262. Correction/Restatement  12/9/05  10:13AM
263. Pi01/digraphs 1  1/13/06  1:11AM
264. Pi01/digraphs 2  1/27/06  11:34AM
265. Pi01/digraphs 2/more  1/28/06  2:46PM
266. Pi01/digraphs/unifying 2/4/06  5:27AM
267. Pi01/digraphs/progress  2/8/06  2:44AM
268. Finite to Infinite 1  2/22/06  9:01AM
269. Pi01,Pi00/digraphs  2/25/06  3:09AM
270. Finite to Infinite/Restatement  2/25/06  8:25PM
271. Clarification of Smith Article  3/22/06  5:58PM
272. Sigma01/optimal  3/24/06  1:45PM
273: Sigma01/optimal/size  3/28/06  12:57PM
274: Subcubic Graph Numbers  4/1/06  11:23AM
275: Kruskal Theorem/Impredicativity  4/2/06  12:16PM
276: Higman/Kruskal/impredicativity  4/4/06  6:31AM
277: Strict Predicativity  4/5/06  1:58PM
278: Ultra/Strict/Predicativity/Higman  4/8/06  1:33AM

Harvey Friedman