[FOM] 266:Pi01/digraphs/unifying

Sat Feb 4 17:27:28 EST 2006

The previous work with finite graph theory is now on my website at

http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html

article 50 under Preprints, Drafts and Abstracts, entitled

Finite Incompleteness: finite graph theory 1.

I have now found a unifying idea. This allows me to state a very basic Pi01
statement with two parameters.

More specifically, in k dimensions, we ask for a G embedding from every r
element subset of V(G)\A into GA which does not move vectors of kind 1 and
does not fix vectors of kind 2.

In the independent statement, kind 1 and kind 2 are very simply defined.

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

Pi01 INCOMPLETENESS: finite graph theory 2
by
Harvey M. Friedman
February 4, 2006

In this abstract, a digraph is a directed graph with no loops and no
multiple edges. Thus all digraphs will be simple. The results will be the
same if we allow loops.

A dag is a directed graph with no cycles.

Let G be a digraph. We write V(G) for the set of all vertices in G, and E(G)
for the set of all edges in G.

Let A containedin V(G). We write GA for the set of all destinations of edges
in G whose origins lie in A. I.e., GA = {y: (therexists x)((x,y) in E(G))}.

We begin by quoting a well known theorem about directed acyclic graphs, or
so called dags. We call it the complementation theorem, but we have been
told that it is rather ordinary fundamental fare in dag theory.

COMPLEMENTATION THEOREM (finite dags). Let G be a finite dag. There is a
unique set A containedin V(G) such that GA = V(G)\A.

We can look at the Complementation Theorem in terms of a large independent
set. We say that A containedin V(G) is independent in G if and only if there
is no edge connecting any two elements of A.

COMPLEMENTATION THEOREM (finite dags). Every finite dag has a unique
independent set A such that V(G)\A containedin GA.

A digraph on a set E is a digraph G where V(G) = E.

We will focus on digraphs whose vertex set is of the form [1,n]^k. Here
k,n >= 1 and [1,n] = {1,2,...,n}.

An upgraph on [1,n]^k is a digraph on [1,n]^k such that for all (x,y) in
E(G), max(x) < max(y).

The following is an immediate consequence of the Complementation Theorem
(finite dags) since upgraphs are obviously dags.

COMPLEMENTATION THEOREM (finite upgraphs). For all k,n >= 1, every upgraph
on [1,n]^k has a unique independent set A such that V(G)\A containedin GA.

Our development relies on what we call order invariant digraphs on [1,n]^k.
These are the digraphs G on [1,n]^k where only the relative order of
coordinates of pairs of vertices determine if they are connected by an edge.

More formally, let u,v lie in {1,2,3,...}^p. We say that u,v are order
equivalent if and only if for all 1 <= i,j <= p,

u_i < u_j iff v_i < v_j.

Let G be a digraph on [1,n]^k. We say that G is order invariant if and only
if the following holds. For all x,y,z,w in [1,n]^k, if (x,y) and (z,w) are
order equivalent (as 2k tuples), then

(x,y) in E(G) iff (z,w) in E(G).

Note that an order invariant digraph on [1,n]^k is completely determined,
among digraphs on [1,n]^k, by the subdigraph induced by [1,2k]^k -
regardless of how large n is. Thus the number of order invariant digraphs on
[1,n]^k is bounded by (2k)^k.

Let G be a digraph and A,B containedin V(G). We say that h is a G embedding
of A into B if and only if h:A into B is one-one, and for all x,y in A,

(x,y) in E(G) if and only if (fx,fy) in E(G).

We say that h fixes x if and only if h(x) = x, and h moves x if and only if
h(x) not= x. Note that if h fixes or moves x, then h(x) is defined.

Let x be a k-tuple of nonnegative integers. We write 2^x for the vector
(2^x1,...,2^xk).

TEMPLATE. For all n,k,r >= 1, every order invariant upgraph G on
[1,n]^k has an independent set A such that the following holds. Every r
element subset of V(G)\A has a G embedding into GA which does not move any
vector of kind 1, and does not fix any vector of kind 2.

Note that in the Template, if we remove "and does not fix any vector of kind
2", then the statement immediately follows from the Complementation Theorem
(finite upgraphs), since we can use the identity embeddings.

PROPOSITION A. For all n,k,r >= 1, every order invariant upgraph G on
[1,n]^k has an independent set A such that the following holds. Every r
element subset of V(G)\A has a G embedding into GA which does not move any
vector 2^x, max(x) >= 0, and does not fix any vector 2^x -1, max(x) >=
(4kr)^2. 

Proposition A can be proved with large cardinals but not without. Note that
Proposition A is explicitly Pi01.

Here is more detailed information.

Let MAH = ZFC + {there exists a strongly n-Mahlo cardinal}n.

Let MAH+ = ZFC + "for all n there exists a strongly n-Mahlo cardinal".

THEOREM 1. MAH+ proves Propositions A,B. However, Proposition A is not
provable in any consistent fragment of MAH that derives Z = Zermelo set
theory. In particular, Proposition A is not provable in ZFC, provided
ZFC is consistent. These facts are provable in RCA_0.

THEOREM 2. EFA + Con(MAH) proves Proposition A.

THEOREM 3. It is provable in ACA that Propositions A is equivalent to
Con(MAH).

By adjusting the vectors to be "not moved" and the vectors to be "not
fixed", we can reach a variety of logical strengths.

It seems clear that we can turn the Template into a formal template, where
we insist that kind 1 and kind 2 be of a certain simple formal character,
and then endeavor to establish which instances of the Template and true and
which are false. We can also endeavor to determine their logical strength.

The proper setup for this, in order to make it dramatic and feasible, need
some serious research - research that I currently do not have the time to
conduct.

Instead, I am working on another such attractive Template, which can be used
for Pi00 statements. This is more urgent.

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 266th 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.

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

Harvey Friedman