[FOM] 297: Order Calculus/restatement

Harvey Friedman friedman at math.ohio-state.edu
Tue Jul 11 12:16:53 EDT 2006


We give a self contained restatement of #296, Order Calculus, 7/7/06,
12:13PM, http://www.cs.nyu.edu/pipermail/fom/2006-July/010636.html

REASON: We have discovered a new order theoretic relation,

B,C are lower equivalent over a_1 < ... < a_p

that is related to those in #296, which significantly simplifies Order
Calculus. 

We then subject the above crucial relation, to TEMPLATING.

###############################

ORDER CALCULUS 
by
Harvey M. Friedman
Ohio State University
July 7 - 11, 2006

1. NEW Pi01 STATEMENTS.

All intervals are discrete. If A is a set of k tuples then A x A is a set of
2k tuples and A^m is a set of km tuples.

For x in [1,n]^k, we write min(x) for the minimum coordinate of x. More
generally, for tuples x_1,...,x_p from [1,n], of various lengths, we write
min(x_1,...,x_p) for the minimum coordinate of the concatenation
(x_1,...,x_p). 

Let A containedin [1,n]^k. We write A' for the complement of A relative to
[1,n]^k. 

Let R containedin [1,n]^k x [1,n]^k. We say that R is strictly dominating if
and only if R(x,y) implies max(x) < max(y). For A containedin [1,n]^k, we
write RA = {y: (therexists x in A)(R(x,y))}.

We say that x,y in [1,n]^k are order equivalent if and only if for all 1 <=
i,j <= k, x_i < x_j iff y_i < y_j.

We say that B containedin [1,n]^k is order invariant if and only if for all
order equivalent x,y in [1,n]^k, x in B iff y in B.

Let B,C containedin [1,n]^r. Let p >= 0 and 1 <= a_1,...,a_p <= n. We write

B,C are lower equivalent over a_1 < ... < a_p

if and only if for all subsequences u,v of a_1,...,a_p of the same nonzero
length,

i. for all x in B, there exists y in B intersect C, such that (x,u), (y,v)
are order equivalent and min(y,u,v) <= min(x,u,v); and

ii. for all y in C, there exists x in C intersect B, such that (y,v), (x,u)
are order equivalent and min(x,v,u) <= min(y,v,u).

We begin with our usual starting point. We call this the Complementation
Theorem (finite relations).
  
THEOREM 1.1. For all n,k >= 1 and strictly dominating R containedin [1,n]^k
x [1,n]^k, there exists A containedin [1,n]^k such that RA = A'.
Furthermore, A is unique.

We now come to something new.

PROPOSITION 1.2. For all n >> k,m >= 1 and strictly dominating order
invariant R containedin [1,3n]^k x [1,3n]^k, there exists A containedin
[1,3n]^k such that (RA)^m and A'^m are lower equivalent over n,2n.

PROPOSITION 1.3. For all n >> k,m >= 1 and strictly dominating order
invariant R containedin [1,4n]^k x [1,4n]^k, there exists A containedin
[1,4n]^k such that (RA)^m and A'^m are lower equivalent over n,2n,3n.

PROPOSITION 1.4. For all n >> k,m,p >= 1 and strictly dominating order
invariant R containedin [1,pn]^k x [1,pn]^k, there exists A containedin
[1,pn]^k such that (RA)^m and A'm are lower equivalent over n,2n,...,pn-n.

THEOREM 1.5. The following is provable in EFA. Proposition 1.2 implies
Con(ZFC + "there exists a totally indescribable cardinal") and is implied by
Con(ZFC + "there exists a subtle cardinal"). Proposition 1.3 implies Con(ZFC
+ "there exists a subtle cardinal") and is implied by Con(ZFC + "there
exists a 2 subtle cardinal"). Proposition 1.4 is equivalent to Con(ZFC +
"there exists an n subtle cardinal")_n.

Note that Propositions 1.2-1.4 are not explicitly Pi01. They are explicitly
Pi03. They can be put into an equivalent explicitly Pi01 form by eliminating
n in favor of an expression in k,m (and k,m,p) as follows.

PROPOSITION 1.6. For all n >= (8km)! >= 1 and strictly dominating order
invariant R containedin [1,3n]^k x [1,3n]^k, there exists A containedin
[1,3n]^k such that (RA)^m and A'^m are lower equivalent over n,2n.

PROPOSITION 1.7. For all n >= (8km)! >= 1 and strictly dominating order
invariant R containedin [1,4n]^k x [1,4n]^k, there exists A containedin
[1,4n]^k such that (RA)^m and A'^m are lower equivalent over n,2n,3n.

PROPOSITION 1.8. For all n >= (8kmp)!, p >= 1 and strictly dominating order
invariant R containedin [1,pn]^k x [1,pn]^k, there exists A containedin
[1,pn]^k such that (RA)^m and A^m are lower equivalent over n,2n,...,pn-n.

THEOREM 1.9. The following is provable in EFA. Proposition 1.2 is
equivalent to Proposition 1.6. Proposition 1.3 is equivalent to Proposition
1.7. Proposition 1.4 is equivalent to Proposition 1.8.

2. NEW Pi01 TEMPLATES.

Note that the relation

B and C are lower equivalent over a_1,...,a_p

can be viewed as a conjunction of

B and C are lower equivalent relative to u,v

over all pairs u,v that are nonempty subsequences of a_1,...,a_p of the same
length. This means 

i. for all x in B, there exists y in B intersect C, such that (x,u), (y,v)
are order equivalent and min(y,u,v) <= min(x,u,v); and

ii. for all y in C, there exists x in C intersect B, such that (y,v), (x,u)
are order equivalent and min(x,v,u) <= min(y,v,u).

Accordingly, we consider all statements of the form

*) (forall x in X_1 intersect X_2)(there exists y in X_3 intersect X_4)
((Y_1) == (Y_1') and ... and (Y_p) == (Y_p) and min(Z_1) <= min(Z_1') and
... and min(Z_q) <= min(Z_q'))

where 

a. The X_i are among the two letters B,C.
b. The Y_i are tuples among the terms x,y,n,2n,3n,... .
c. The Z_i are tuples among the terms x,y,n,2n,3n,... .
d. == means "order equivalent to".

Here is the Template associated with Proposition 2:

TEMPLATE (RA,A',n,2n). For all n >> k,m >= 1 and strictly dominating order
invariant R containedin [1,3n]^k x [1,3n]^k, there exists A containedin
[1,3n]^k such that a given set of *) statements in (RA)^m,A'^m,n,2n hold.

I.e., B is replaced by (RA)^m, C is replaced by A'^m, and at most n,2n are
used.

It is of course natural to extend the Template in the following way.

TEMPLATE (RA,A',A,n,2n). For all n >> k,m >= 1 and strictly dominating order
invariant R containedin [1,3n]^k x [1,3n]^k, there exists A containedin
[1,3n]^k such that a given set of *) statements in (RA)^m,A'^m,A,n,2n hold.

We should be able to determine the truth value of all instances of these
Templates using a subtle cardinal. Of course, we must use at least a totally
indescribable cardinal in light of Theorem 1.5.

More ambitious would be to analyze Template (RA,A',A,n,2n,3n) and so forth.
 
These can be made into Pi01 Templates by placing the same bounds used in
Propositions 1.6 - 1.8. These bounds should not affect the truth values of
the instances of the Templates.

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

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

Harvey Friedman 




 



More information about the FOM mailing list