[FOM] 299: Order Calculus/simplification
Harvey Friedman
friedman at math.ohio-state.edu
Sun Jul 23 19:38:25 EDT 2006
In #297, Order Calculus/restatement, 7/11/06 12:16PM,
http://www.cs.nyu.edu/pipermail/fom/2006-July/010640.html
we defined the following crucial notion:
Let B,C containedin [1,n]^r. Let p >= 0 and 1 <= a_1,...,a_p <= n.
We have reworked this definition so that it is much simpler. We will give a
new self contained version of Order Calculus.
################################
ORDER CALCULUS
by
Harvey M. Friedman
Ohio State University
July 7 - 23, 2006
1. NEW Pi01 STATEMENTS.
All intervals are discrete. We use a,b,c,d,e,k,n,m,p,q,r,s,t for positive
integers.
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 finite sequences x of positive integers, we write min(x) for the minimum
coordinate of x. More generally, for finite sequences x_1,...,x_p of
positive integers, we write min(x_1,...,x_p) for the minimum coordinate of
the concatenation (x_1,...,x_p). By convention, min of the empty tuple is 0.
Let A containedin [1,n]^k. We write A' for the complement of A relative to
[1,n]^k, which is [1,n]^k\A.
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))}.
Let x,y be finite sequences of positive integers. We say that x,y are order
equivalent if and only if lth(x) = lth(y), and for all 1 <= i,j <= lth(x),
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 and u,v be finite sequences of positive
integers. We say that B,C are lower equivalent from u to v if and only if
(forall x in B union C)(therexists y in B intersect C)((x,u),(y,v) are order
equivalent and min(x,u) >= min(y,u)).
Note that for u = v, the above holds if B = C. However, if u not= v, then B
= C may not be sufficient.
We begin with our usual starting point. We call this the Complementation
Theorem (finite relations).
THEOREM 1.1. For all n,k 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 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 from n to 2n.
PROPOSITION 1.3. For all n >> k,m 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 from n,2n to 2n,3n.
PROPOSITION 1.4. For all n >> k,m,p 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 from n,2n,...,pn-2n to
2n,3n,...,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)! 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 from n to 2n.
PROPOSITION 1.7. For all n >= (8km)! 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 from n,2n to 2n,3n.
PROPOSITION 1.8. For all n >= (8kmp)! 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 from n,2n,...,pn-2n
to 2n,3n,...,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.
There are a number of natural Templates associated with the Propositions of
section 1. i.e., collections of statements obtained by allowing various
components to vary over natural spaces.
An obvious Template allows the multiples of n used to vary, and also allows
multiple clauses.
TEMPLATE 2.1. For all n >> k,m 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 from alpha_1 to beta_1, from
alpha_2 to beta_2, ..., and from alpha_s to beta_s. Here p is a specific
positive integer, and the alpha's and beta's are specific tuples of the
multiples n,2n,...,pn.
Note that Propositions 2-4 are instances of Template 2.1, but Proposition
1.8 is not.
Using the subtle cardinal hierarchy, it can be shown that the instances of
Template 2.1 that hold are exactly those where for all 1 <= i <= s, alpha_i
and beta_i are order equivalent, and if pn appears in beta_i then pn appears
in alpha_i.
Note as a Corollary that an instance of Template 2.1 holds if and only if
each of its s component instances hold.
So the remaining issue is the computation of the logical strength of each
instance. This should be fully analyzable. We will take this up at a later
time.
We can use various Boolean combinations of A and RA.
TEMPLATE 2.2. For all n >> k,m and strictly dominating order invariant R
containedin [1,pn]^k x [1,pn]^k, there exists A containedin [1,pn]^k such
that B_1(A,RA)^m and B_2(A,RA)^m are lower equivalent from alpha_1 to
beta_1, from alpha_2 to beta_2, ..., and from alpha_s to beta_s. Here p is a
specific positive integer, B_1(A,RA), B_2(A,RA) are specific Boolean
combinations of A,RA, and the alpha's and beta's are specific tuples of the
multiples n,2n,...,pn.
This should be fully analyzable.
Considerably more ambitious would be to allow the following wider class of
compound Boolean expressions in A,R. These are defined inductively by
i. A is an expression.
ii. Boolean combinations of expressions are expressions.
iii. R(X) is an expression if X is an expression.
Thus we arrive at the following.
TEMPLATE 2.3. For all n >> k,m and strictly dominating order invariant R
containedin [1,pn]^k x [1,pn]^k, there exists A containedin [1,pn]^k such
that CB_1(A,R)^m and CB_2(A,R)^m are lower equivalent from alpha_1 to
beta_1, from alpha_2 to beta_2, ..., and from alpha_s to beta_s. Here p is a
specific positive integer, CB_1(A,R), CB_2(A,R) are specific compound
Boolean expressions in A,R, and the alpha's and beta's are specific tuples
of the multiples n,2n,...,pn.
We can obviously extend the above further by allowing various pairs of
compound Boolean expressions in A,R, simultaneously.
Much more ambitious Templates arise by asking for more than one set A. We
can ask for sets A_1,...,A_t such that some set of lower equivalences holds
between a pair (or even various pairs) of Boolean combinations of
A_1,...,A_t,R(A_1),...,R(A_t) from various tuples to various tuples.
We can even ask for sets A_1,...,A_t such that some set of lower
equivalences holds between various compound Boolean expressions in
A_1,...,A_t,R from various tuples to various tuples.
We can even go much much further by considering more than one strictly
dominating order invariant R.
A whole new dimension of difficulty arises when we wish to template the
definition of
B is lower equivalent to C from u to v.
Recall that this takes the forall/exist form
(forall x in B union C)(therexists y in B intersect C)((x,u),(y,v) are order
equivalent and min(x,u) >= min(y,u)).
We can replace B union C, and B intersect C, by various Boolean combinations
of B,C. We can replace >= by >,<,=, and use various patterns of the letters
x,y,u,v, and allow multiple clauses inside the quantifier free part. We can
also allow multiple forall/therexist sentences of this form, taken
conjunctively.
Furthermore, we can combine the previous paragraph with the earlier
paragraphs after Template 2.3.
Additional moves can be made if we fix dimension k, keeping m as a
quantified variable. We know that we still have the same independence
results for the original Propositions if we fix k to be quite small. But if
we fix k then we can template the notion "order invariant". This opens up a
whole new major dimension of templating.
As in section 1, these Templates are all, technically speaking, Pi03
Templates. However, We can appropriately replace n >> k,m with n >= (8kmt)!
and obtain Pi01 Templates. I.e., each instance is a Pi01 sentence. (Here t
represents the size of the conclusion statement).
**********************************
I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 299th 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
Harvey Friedman
More information about the FOM
mailing list