@article{8767688,
  abstract     = {{A prefixed polynomial equation, or a polynomial expression with a quantifier prefix, is an equation of the form P(x(1), x(2),..., x(n)) = 0, where P is a polynomial with integer coefficients whose variables x(1), x(2),..., x(n) range over natural numbers, that is preceded by some quantifiers over all of its variables x(1), x(2),..., x(n). Here is a typical, seemingly random, example of such an expression, Phi : for all m c there exists N for all a b there exists c d X A X for all x y there exists BCF there exists hijklnpqrst x (y+B-x) center dot (A+m+B-y) center dot((A+h-d)(2) + ((d+1) center dot i + A-c)(2) + (B+n-dx)(2) + (+(()dx+1) center dot j+B-c)(2) + (C+ r-dy)(2) + ((dy+1) center dot k+C-c)(2) + (B + s + 1 - c)(2) + (+)(c+t-N)(2) + (F+p-b(B+C)(2))(2) + (a -lb(B+C-2)-F- l)(2) + (X-F+eq)(2)) = 0 In this note we initiate the study of the collection of all possible such expressions ('the Atlas'), equipped with the equivalence relation of "being EFA-provably equivalent" on its members. The Atlas is partially ordered by EFA-implication. Here is the first abstract picture of the Atlas to have in mind: [GRAPHICS] Notice that the set of all prefixed polynomial equations is arithmetically complete, that is, every first-order arithmetical formula is EFA-equivalent to some prefixed polynomial expression. In this sense, the Atlas is just another way of talking about first-order arithmetical statements. Godel's Incompleteness theorems guarantee existence of many distinct equivalence classes. Our first task is to find examples. We start off with examples of distinct equivalence classes of metamathematical interest: the 1-consistency of I Sigma(1) (the expression phi above), the 1-consistency of I Sigma(2), the 1-consistency of full Peano Arithmetic, the highly unprovable Finite Kruskal's Theorem. [GRAPHICS] Then we give an example of the phase transition phenomenon. We produce a polynomial expression that has two free variables m and n such that whenever m/n is smaller or equal to Weiermann's constant w approximate to 0.63957768999472013311..., the expression is EFA-provable, otherwise it is unprovable in the theory ATR0 (so we witness a phase transition between EFA-provability and predicative unprovability). Then we give a crude example of a polynomial equation with quantifiers that is equivalent to the famous Graph Minor Theorem and, hence, is of the unknown high strength beyond that of Pi(1)(1)-CA(0). A 'seed' is a prefixed polynomial equation that is of minimal length in its EFA-equivalence class. We discuss seeds and notice that the seed of the 1-consistency of I Sigma(1) is smaller than 131. We discuss the role of the Atlas and its possible future partial implementation as a metamathematically-sensitive database of mathematical knowledge. The purpose of this note is to give definitions, to arrange the set-up, give nontrivial examples, introduce the right unprovability-sensitive notions, and ask some first questions about the Atlas. The current note omits all proofs. All proofs can be found in the grand manuscript [4]. Eventually, a bigger article, stemming from [4] will appear. Some of the material from this project became a chapter in the second author's doctoral thesis [6] at the University of Gent, Belgium. The authors genuinely and cordially thank the John Templeton Foundation for its interest and support for Unprovability research. The first author thanks the John Templeton Foundation for its financial support.}},
  author       = {{Bovykin, Andrey and De Smet, Michiel}},
  editor       = {{Baaz, Matthias}},
  issn         = {{2055-3706}},
  journal      = {{JOURNAL OF APPLIED LOGICS-IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS}},
  language     = {{eng}},
  number       = {{10}},
  pages        = {{3239--3261}},
  title        = {{A glimpse at polynomials with quantifiers}},
  url          = {{http://collegepublications.co.uk/ifcolog/?00019}},
  volume       = {{4}},
  year         = {{2017}},
}