[FOM] 319: Pi01 Incompleteness/Digraphs/#3

Tue Feb 12 10:36:45 EST 2008

We make an improvement on #315.

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

1. INFINITE FORM.

Here digraphs will not have multiple edges, but can have loops.

Let G be a digraph. We write V(G) for the set of vertices of G, and  
E(G) for
the set of edges of G. Edges of G are ordered pairs of vertices of G.

We say that G is a digraph on V(G).

Let S containedin V(G). We say that S is independent if and only if  
there is
no edge with vertices from S. We write S' = V(G)\S.

We write GS for {y: (therexists x in S)((x,y) in E(G))}.

We use interval notation. All intervals are discrete. We use [1,inf)  
for the
set of all positive integers.

Let G be a digraph on [1,inf)^k. We say that G is upwards if and only if

(x,y) in E(G) implies max(x) < max(y).

The following is an immediate consequence of a well known theorem from  
graph
theory.

THEOREM 1.1. Every upwards digraph G on [1,inf)^k has an independent  
set S,
where GS = S'. Furthermore, S is unique.

Let x,y in [1,inf)^k. We say that x,y are order equivalent if and only  
if
for all 1 <= i,j <= k,

x_i < x_j iff y_i < y_j.

Let G be a digraph with V(G) = [1,inf)^k. We say that G is order  
invariant
if and only if for all vertices x,y,z,w, if (x,y) and (z,w) are order
equivalent (as elements of [1,inf)^2k), then

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

For n >= 1, the powers of n are the vectors whose coordinates lie in
{1,n,n^2,...}.

The successor of V containedin [1,inf)^k is the set resulting from  
raising all coordinates by 1.

PROPOSITION 1.2. Every upwards order invariant digraph G on [1,inf)^k  
has an
independent set S such that the following holds. Every k element  
independent subset of S'
has the same powers of (8k)! as some k element independent subset of  
GS whose successor
has none.

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

THEOREM 1.3. Theorem 1.1 is provable in RCA_0. Proposition 1.2 is  
provable
in MAH+ but not in MAH, assuming that MAH is consistent. Proposition 1  
is
provably equivalent, over ACA, to CON(MAH). Proposition 1 is not  
provable in
any consistent subsystem of MAH. In particular, Proposition 1 is not
provable in ZFC, assuming ZFC is consistent. If we delete "whose  
successor has none",
then Proposition 1.2 is an immediate consequence of Theorem 1.1.

Here (8k)! is just a convenient expression.

2. FINITE FORM.

The finite forms are obtained trivially by replacing [1,inf) with  
[1,n]. All
of the definitions are restated in the obvious way with [1,inf) replaced
throughout by [1,n]. Specifically,

PROPOSTION 2.2. Every upwards order invariant graph G on [1,n]^k has an
independent set S such that the following holds. Every k element  
independent subset of S'
has the same powers of (8k)! as some k element independent subset of  
GS whose successor
has none.

Proposition 2.2 is explicitly Pi01.

All of the results read the same.

**********************************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 319th 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
279: Subcubic graph numbers/restated  4/8/06  3:14AN
280: Generating large caridnals/self embedding axioms  5/2/06  4:55AM
281: Linear Self Embedding Axioms  5/5/06  2:32AM
282: Adventures in Pi01 Independence  5/7/06
283: A theory of indiscernibles  5/7/06  6:42PM
284: Godel's Second  5/9/06  10:02AM
285: Godel's Second/more  5/10/06  5:55PM
286: Godel's Second/still more  5/11/06  2:05PM
287: More Pi01 adventures  5/18/06  9:19AM
288: Discrete ordered rings and large cardinals  6/1/06  11:28AM
289: Integer Thresholds in FFF  6/6/06  10:23PM
290: Independently Free Minds/Collectively Random Agents  6/12/06   
11:01AM
291: Independently Free Minds/Collectively Random Agents (more)  6/13/06
5:01PM
292: Concept Calculus 1  6/17/06  5:26PM
293: Concept Calculus 2  6/20/06  6:27PM
294: Concept Calculus 3  6/25/06  5:15PM
295: Concept Calculus 4  7/3/06  2:34AM
296: Order Calculus  7/7/06  12:13PM
297: Order Calculus/restatement  7/11/06  12:16PM
298: Concept Calculus 5  7/14/06  5:40AM
299: Order Calculus/simplification  7/23/06  7:38PM
300: Exotic Prefix Theory   9/14/06   7:11AM
301: Exotic Prefix Theory (correction)  9/14/06  6:09PM
302: PA Completeness  10/29/06  2:38AM
303: PA Completeness (restatement)  10/30/06  11:53AM
304: PA Completeness/strategy 11/4/06  10:57AM
305: Proofs of Godel's Second  12/21/06  11:31AM
306: Godel's Second/more  12/23/06  7:39PM
307: Formalized Consistency Problem Solved  1/14/07  6:24PM
308: Large Large Cardinals  7/05/07  5:01AM
309: Thematic PA Incompleteness  10/22/07  10:56AM
310: Thematic PA Incompleteness 2  11/6/07  5:31AM
311: Thematic PA Incompleteness 3  11/8/07  8:35AM
312: Pi01 Incompleteness  11/13/07  3:11PM
313: Pi01 Incompleteness  12/19/07  8:00AM
314: Pi01 Incompleteness/Digraphs  12/22/07  4:12AM
315: Pi01 Incompleteness/Digraphs/#2  1/16/08  7:32AM
316: Shift Theorems  1/24/08  12:36PM
317: Polynomials and PA  1/29/08  10:29PM
318: Polynomials and PA #2  2/4/08  12:07AM

Harvey Friedman