[FOM] 300: Exotic Prefix Theory
Harvey Friedman
friedman at math.ohio-state.edu
Thu Sep 14 07:11:29 EDT 2006
The state of the art on Order Calculus and the variants of the Pi01
independent statements that are associated with the subtle cardinal
hierarchy (not the Mahlo cardinal hierarchy), is now contained in
Search for Consequences, under downloadable manuscripts, Lecture Notes,
http://www.math.ohio-state.edu/%7Efriedman/
Note that the independent statements in Search for Consequences go forward
and backward. The ones in posting #299 only go forward, and we are no
longer confident that we can get away with this in #299.
############################
The Order Calculus development now appears as key Lemmas in Exotic Prefix
Theory.
Exotic Prefix Theory is the study of basic prefix classes, comprising
finitely many sentences, at least one of which is independent of ZFC. Such a
prefix class is said to be "exotic".
The goal is to show that various exotic prefix classes can be "tamed by
large cardinals". I.e., every statement in the class is either provable or
refutable using large cardinals. Some of these exotic prefix classes consist
entirely of explicitly Pi01 sentences.
At the moment, this goal is out of reach for any basic exotic prefix class.
However, we expect a long series of partial results, that various subclasses
can be tamed by large cardinals.
In both Search for Consequences, and Forty Years on his Shoulders, under
downloadable manuscripts, http://www.math.ohio-state.edu/%7Efriedman/ we
made the following conjecture:
EXOTIC CONJECTURE
Every interesting mathematical theorem can be recast as one among a
natural finite set of statements, all of which can be decided using well
studied extensions of ZFC, but not within ZFC itself.
######################
We now present some prefix classes that comprise finitely many statements,
at least one of which is independent of ZFC (exotic prefix classes). Some of
the prefix classes consist entirely of explicitly Pi01 sentences.
This suggests the following:
EXOTIC PREFIX CONJECTURE
Every interesting mathematical theorem is an element of a natural exotic
prefix class. In other words, every interesting mathematical theorem can be
recast as an element of a natural prefix class, with finitely many elements,
all of which can be decided using well studied extensions of ZFC, but not
within ZFC itself.
######################
As we have done many times before, we start with what we call the
complementation theorem for relations.
Lower case letters stand for positive integers, unless otherwise
indicated. We write [inf] for the set of all positive integers, and [n] for
{1,...,n}.
For A containedin [n]^k, we write A' = [n]^k\A.
Let R containedin [n]^k x [n]^k = [n]^2k. We write RD = {b: (therexists a in
D)(R(a,b))}.
We say that R is strictly dominating iff for all a,b, if
R(a,b) then max(a) < max(b).
COMPLEMENTATION THEOREM (finite relations). For all n,k >= 1 and strictly
dominating R containedin [n]^2k, there exists D containedin [n]^k such that
RD = D'. In fact, A is unique.
Here we will also consider the obvious infinite form. Let [inf] =
{1,2,...}.
COMPLEMENTATION THEOREM (infinite relations). For all k >= 1 and strictly
dominating R containedin [inf]^2k, there exists D containedin [inf]^k such
that RD = D'. In fact, D is unique.
The above is a special case of a well known and well studied theorem in
digraph theory - for any dag G, there is a (unique) D containedin V(G) such
that GD = V(G)\D. (Here GD is the set of heads coming out from D).
We can put the complementation theorem in the following successive logical
forms.
If R is strictly dominating then there exists D such that RD = D'.
For all R there exists D such that if R is strictly dominating then RD = D'.
For all R there exists D such that if (forall a,b)(R(a,b) implies a < b)
then RD contianedin D' and D' containedin RD.
For all R there exists D such that if (forall a,b)(R(a,b) implies a < b)
then (forall a,b in D)(not(R(a,b)) and (forall a in D')(therexists b in D)
(R(b,a)).
For all R there exists D such that EE or (AA and AE).
For all R there exists D such that AAEE.
In the above, we have used < for
a < b iff max(a) < max(b).
Thus we have put the Complementation Theorem (relations), without
uniqueness, into the following prefix forms:
Let k >= 1. (forall R containedin [inf]^2k)(therexists D containedin
[inf]^k)(forall a,b in [inf]^k)(therexists c,d in [inf]^k)
(phi(R,D,a,b,c,d)).
Let k,n >= 1. (forall R containedin [n]^2k)(therexists D containedin
[n]^k)(forall a,b in [n]^k)(therexists c,d in [n]^k)(phi(R,D,a,b,c,d)).
where phi is a propositional combination of atomic formulas
v < w.
v in A.
R(v,w).
where v,w are among the variables a,b,c,d.
However, we can give obviously equivalent forms of the Complementation
Theorem (relations) which need one less quantifier to state:
COMPLEMENTATION THEOREM (infinite relations). For all k >= 1 and R
containedin [inf]^2k, there exists D containedin [inf]^k such that R<D = D'.
In fact, D is unique.
COMPLEMENTATION THEOREM (finite relations). For all n,k >= 1 and R
containedin [n]^2k, there exists D containedin [n]^k such that R<D = D'. In
fact, D is unique.
Here R<D is taken to be {b: (therexists a in D)(a < b and R(a,b)}.
If R is strictly dominating then there exists D such that R<D = D'.
For all R there exists D such that R<D = D'.
For all R there exists D such that if R<D contianedin D' and D' containedin
R<D.
For all R there exists D such that (forall a,b in D)(not(R(a,b)) and
a < b) and (forall a in D')(therexists b in D)(R(b,a) and b < a).
For all R there exists D such that AA and AE.
For all R there exists D such that AAE.
Thus we have put the Complementation Theorem (relations), without
uniqueness, into the following form:
Let k >= 1. (forall R containedin [inf]^2k)(therexists D containedin
[inf]^k)(forall a,b in [inf]^k)(therexists c in [inf]^k)(phi(R,D,a,b,c)).
Let k,n >= 1. (forall R containedin [n]^2k)(therexists D containedin
[n]^k)(forall a,b in [n]^k)(therexists c in [n]^k)(phi(R,D,a,b,c)).
where phi is a propositional combination of atomic formulas of the forms
v < w.
v in D.
R(v,w).
Here v,w are among the variables a,b,c.
We can now ask for a determination of the truth values of all instances of
Let k >= 1. (forall R containedin [inf]^2k)(therexists D containedin
[inf]^k)(forall a,b in [inf]^k)(therexists c in [inf]^k)(phi(R,D,a,b,c)).
Let k,n >= 1. (forall R containedin [n]^2k)(therexists D containedin
[n]^k)(forall a,b in [n]^k)(therexists c in [n]^k)(phi(R,D,a,b,c)).
where phi is as given above.
We strongly believe that these classification problems are manageable,
with some real effort, and also that these particular prefix classes are not
exotic. I.e., these sets of statements are not comprehensive enough to force
us out of ZFC.
We have been able to extend these Templates above that incorporate
the Order Calculus development. In particular, consider the following four
Templates:
Let k >= 1. (forall R containedin [inf]^2k)(therexists S containedin
[inf]^2k)(forall a,b,c,d in [inf]^k)(therexists e,f,g,h in [inf]^k)
(phi(R,S,a,b,c,d,e,f,g,h)).
Let n >> k. (forall R containedin [n]^2k)(therexists S containedin
[n]^2k)(forall a,b,c,d in [n]^k)(therexists e,f,g,h in [n]^k)
(phi(R,S,a,b,c,d,e,f,g,h)).
For all k there exists n such that the following holds. (forall R
containedin [n]^2k)(therexists S containedin [n]^2k)(forall a,b,c,d in
[n]^k)(therexists e,f,g,h in [n]^k) (phi(R,S,a,b,c,d,e,f,g,h)).
Let k >= 1. (forall R containedin [(8k)!]^2k)(therexists S containedin
[(8k)!]^2k)(forall a,b,c,d in [(8k)!]^k)(therexists e,f,g,h in [(8k)!]^k)
(phi(A,B,a,b,c,d,e,f,g,h)).
where phi is a propositional combination of formulas of the form
v < w.
v ~ w.
R(v,w).
S(v,w).
Here v,w are among the variables a,b,c,d,e,f,g,h. Also, ~ denotes order
equivalence.
Using the Order Calculus development, we can show that all four of these
prefix classes are exotic. In fact, we find a single
phi(R,S,a,b,c,d,e,f,g,h) using only the atomic formulas above, such that all
four of the above Templates are provable in ZFC + "there exists a 2-subtle
cardinal", but not in ZFC, or even in ZFC + "there exists a subtle cardinal
kappa such that there are kappa many subtle cardinals below kappa".
Note that these Templates are, explicitly, in
Pi12, Pi03, Pi02, Pi01
form, respectively.
We conjecture that these four exotic prefix can all be tamed by large
cardinals. In fact, that all instances of these four Templates can be
decided in ZFC + {there exists an n-subtle cardinal}_n.
We can refer to these prefix forms as
(AE;A^4E^4).
Using (AE;A^5E^5), we can get past 2-subtle cardinals, (AE;A^6E^6) past
3-subtle cardinals, etcetera. Of course, at some point, we probably run into
the real possibility of coding, so that the prefix class becomes "completely
wild" - whatever that means. But we are convinced that (2,2;4,4) is far
below the "completely wild" level, whatever that means.
Some partial results will probably involve restrictions on the atomic
formulas that appear in the instances.
Coming back to the Exotic Prefix Conjecture, we can obviously view the
Complementation Theorem (relations) as an instance of the exotic classes
presented above. Of course, the challenge that awaits us is to eventually
show that these exotic classes can be tamed by large cardinals.
**********************************
I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 300th 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
Harvey Friedman
More information about the FOM
mailing list