[FOM] 491:Formal Simplicity

Sun Mar 25 16:58:42 EDT 2012

THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION

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

THIS POSTING IS ENTIRELY SELF CONTAINED

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

Arana's posting http://www.cs.nyu.edu/pipermail/fom/2012-March/016353.html 
  led me to http://www.cs.nyu.edu/pipermail/fom/2012-March/016356.html  
and to getting focused (refocused) on Formal Simplicity. I hope Arana  
continues making interesting postings.

Suppose we want to claim that some particular mathematical statement  
is "natural"? Obviously if it fits well into the existing mathematical  
literature, then that can be used.

But, otherwise, this is generally difficult to argue. Easy to argue  
this with people who are struck for some reason by its naturalness,  
and very difficult to argue this with people who are not so struck.

So what can be done?

The best approach we have seems to be to argue for "simplicity".  
Obviously "simplicity" is not the same as "naturalness", but they are  
obviously related in some way, and also "simplicity" is a nice  
positive adjective just like "natural".

The best handle we have on "simplicity" is in terms of length of  
expressions in a "natural" formal language.

Now it looks like we have a vicious circle, with "natural" appearing  
again!

But the formal languages we have in mind for this purpose are the  
standard sugared set theoretic language for general purpose  
mathematics, restricted to a handful of "natural" primitives.

We once again have descended into a vicious circle, with "natural"  
appearing yet again!

But NOW we apply a SEVERE test for "naturalness" of a primitive here.

We require that the primitive notions being used are massively used in  
existing mathematics.

This criteria for the primitives in the formal languages is of course  
not the same "natural", but is almost certain to imply "natural".

And this criteria can usually be quickly verified using current  
technology. GOOGLE searches under the quote signs is the natural way  
to verify this (this last use of "natural" is a deliberate joke-in- 
truth).

I have already done some work on sugared set theoretic foundations -  
as have other people. E.g., you might look at

H. Friedman, S. Kieffer, J. Avigad), A language for mathematical  
knowledge management, in: Computer Reconstruction of the Body of  
Mathematics, ed. A. Grabowski, A. Naumowicz, Studies in Logic, Grammar  
and Rhetoric, p. 51-66, 2009.

In this posting, I want to largely take Sugared Set Theoretic  
Foundations for granted, and get right away to Formal Simplicity. I  
will take up Sugared Set Theoretic Foundations, or SSTF, in later  
postings, as it probably needs some streamlining to work well with  
theory and experiments in Formal Simplicity.

INVARIANT MAXIMALITY STATEMENT

Let us focus on the seemingly best single Invariant Maximality  
statement. Recall that it is provably equivalent to consistency of  
large cardinals over ACA' - actually, Con(SRP).

PROPOSITION 1. Every order invariant subset of Q[0,n]^2k has a  
completely Z+up invariant maximal square.

In this first version of Formal Simplicity, we will not follow the  
convention that is implicitly used whereby subsets of a space carry  
along the space. For this reason, we need to adjust the statement.

PROPOSITION 2. S is an order invariant subset of Q[0,n]^2k implies  
(therexists U)(U is a maximal square in S and U is completely Z+up,n, 
2k invariant).

Proposition 2 thus has the following logical form:

alpha(S,n,k) implies (therexists U)(beta(U,S) and gamma(U,n,k))

where alpha,beta,gamma are ternary, binary, and ternary predicates.

We now list the Google friendly primitives that we use in order to  
express Proposition 2.

1. Z+. Set of all positive integers.
2. Q. Set of all rationals. We take Z+ to be a subset of Q.
3. variables k,n,m,r,i,j over Z+.
4. variables p,q over Q.
5. 0. Zero.
6. in, containedin. Membership, contained in.
7. <=. Usual <= on real numbers.
8. 2k. Doubling a rational.
9. x. Cartesian product.
10. S^k. Set of all k-tuples from S.
11. [a,b]. The usual closed interval of reals, for reals a,b.
12. x_i. The i-th coordinate of the tuple x.
13. int. Pairwise intersection.

The above have very high number of uses in the existing mathematical  
literature. Evidence for this can be obtained through Google searches.

Here is the natural definitional lead up to Propositional 2.

1. Q[0,n] = Q int [0,n].
2. x ~ y for x,y in Q[0,n]^k. Order equivalence.
3. S is an order invariant subset of Q[0,n]^2k.
4. Z+up,n,k: Q[0,n)^2k into Q[0,n]^2k. Sugared set theory allows this  
expression Z+up,n,m to be introduced in this way and explicitly  
defined and used as a function (a function for each n,k). Here Z+up is  
just a primitive combination of symbols, and n,k are the primitive  
variables over Z+. This adds 1 to all coordinates that are greater  
than all coordinates not in Z+.
5. U is completely f invariant. This means x in U iff f(x) in U.
6. U is a maximal square in S.

QUESTION. How does this natural formal development of Proposition 2  
compare to various normal theorems in the existing mathematical  
literature? Of course, the continuum hypothesis is particularly simple  
in this sense. But what about continuous, discrete, or finite  
mathematics?

QUESTION. Is there any way to get a provable equivalence with  
consistency of large cardinals which is remotely this simple, over  
primitives with high Google searches?

The development above is not only relatively short, but it is "locally  
natural" in some definite sense. E.g., the moves made in the  
development are each individually made all through existing math.

QUESTION. How do we be more precise about this kind of "local  
naturalness"?

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

I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 491st 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-449 can be found
in the FOM archives at http://www.cs.nyu.edu/pipermail/fom/2010-December/015186.html

450: Maximal Sets and Large Cardinals II  12/6/10  12:48PM
451: Rational Graphs and Large Cardinals I  12/18/10  10:56PM
452: Rational Graphs and Large Cardinals II  1/9/11  1:36AM
453: Rational Graphs and Large Cardinals III  1/20/11  2:33AM
454: Three Milestones in Incompleteness  2/7/11  12:05AM
455: The Quantifier "most"  2/22/11  4:47PM
456: The Quantifiers "majority/minority"  2/23/11  9:51AM
457: Maximal Cliques and Large Cardinals  5/3/11  3:40AM
458: Sequential Constructions for Large Cardinals  5/5/11  10:37AM
459: Greedy CLique Constructions in the Integers  5/8/11  1:18PM
460: Greedy Clique Constructions Simplified  5/8/11  7:39PM
461: Reflections on Vienna Meeting  5/12/11  10:41AM
462: Improvements/Pi01 Independence  5/14/11  11:53AM
463: Pi01 independence/comprehensive  5/21/11  11:31PM
464: Order Invariant Split Theorem  5/30/11  11:43AM
465: Patterns in Order Invariant Graphs  6/4/11  5:51PM
466: RETURN TO 463/Dominators  6/13/11  12:15AM
467: Comment on Minimal Dominators  6/14/11  11:58AM
468: Maximal Cliques/Incompleteness  7/26/11  4:11PM
469: Invariant Maximality/Incompleteness  11/13/11  11:47AM
470: Invariant Maximal Square Theorem  11/17/11  6:58PM
471: Shift Invariant Maximal Squares/Incompleteness  11/23/11  11:37PM
472. Shift Invariant Maximal Squares/Incompleteness  11/29/11  9:15PM
473: Invariant Maximal Powers/Incompleteness 1  12/7/11  5:13AMs
474: Invariant Maximal Squares  01/12/12  9:46AM
475: Invariant Functions and Incompleteness  1/16/12  5:57PM
476: Maximality, CHoice, and Incompleteness  1/23/12  11:52AM
477: TYPO  1/23/12  4:36PM
478: Maximality, Choice, and Incompleteness  2/2/12  5:45AM
479: Explicitly Pi01 Incompleteness  2/12/12  9:16AM
480: Order Equivalence and Incompleteness
481: Complementation and Incompleteness  2/15/12  8:40AM
482: Maximality, Choice, and Incompleteness 2  2/19/12 7:43AM
483: Invariance in Q[0,n]^k  2/19/12  7:34AM
484: Finite Choice and Incompleteness  2/20/12  6:37AM__
485: Large Large Cardinals  2/26/12  5:55AM
486: Naturalness Issues  3/14/12  2:07PM
487: Invariant Maximality/Naturalness  3/21/12  1:43AM
488: Invariant Maximality Program  3/24/12  12:28AM
489: Invariant Maximality Programs  3/24/12  2:31PM
490: Invariant Maximality Program 2  3/24/12  3:19PM

Harvey Friedman