[FOM] 491:Formal Simplicity
Sam Sanders
sasander at cage.ugent.be
Mon Mar 26 03:21:21 EDT 2012
An important aspect of naturalness, at least in theories regarding the observable universe (physics, chemistry,…), is that they are *robust*.
The latter notion means 'stability under (small) variations of parameters'. The idea is that scientific theories are approximations of reality which always incorporate
small errors (often for valid reasons such as workability). Hence, the theory is a reasonable approximation of reality and robustness guarantees that
the small errors in the theory do not cause artifacts/problems/...
In the context of Harvey Friedman's recent results, the question of robustness is (leads to) the following:
If one varies slightly the definitions, basic objects, functions at hand, … can one (in most cases) still obtain
a statement (similar to the ones provided by Harvey Friedman) that is not provable in ZFC?
I suspect that a) the answer is yes, and b) this is another aspect of the inevitability mentioned by Harvey Friedman:
In similar contexts, we can obtain similar unprovable statements, i.e. they can be found everywhere, and their
discovery is also inevitable.
Just so we understand each other: most variations of the unprovable statements provided by Harvey Friedman are probably provable in ZFC.
However, the question of robustness is not whether variations of an unprovable statement are also unprovable, but whether there are
similar unprovable statements in a similar framework.
Sam Sanders
PS: In my opinion, understanding such qualitative aspects (like naturalness, simplicity, robustness, similarity of behaviour,...) of scientific theories
is an important aspect of foundational investigation.
On Mar 25, 2012, at 10:58 PM, Harvey Friedman wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
More information about the FOM
mailing list