FOM: 78:Quadratic Axioms/Literature Conjectures
Harvey Friedman
friedman at math.ohio-state.edu
Fri Jan 7 11:51:00 EST 2000
In posting #77, I gave two axiomatizations of ISigma_0(exp) = EFA where all
axioms are strictly mathematical in the strong sense that they can be found
in the standard published literature in number theory - subject to some
quibbles. However, in order to accomplish this, I needed to go beyond the
language of ordered rings by using variables over finite sets of integers.
The question arises as to whether this can be accomplished just in the
language of ordered rings.
I have looked at some elementary number theory books such as Hardy and
Wright, Niven and Zuckerman, etcetera.
In these references, I could not find a single theorem or quoted fact, phi,
in the language of ordered rings such that
*ISigma_0 + phi is equivalent to ISigma_0(exp)*
in the sense that they prove the same sentences in the language of ordered
rings. This is equivalent to saying that
*ISigma_0 + phi is literally equivalent to ISigma_0 + exp*
where exp is the awkward coded version of "for all n >= 0, 2^n exists"
appropriate for ISigma_0.
However, lurking in the background, there is the following obvious
consequence of statements made in these books which sits in the language of
ordered rings:
1) for all n > 0 there exists x > 0 such that for all 1 <= i <= n, i divides x.
This is a consequence of various trivial properties of the factorial (!)
that are always used whenever factorial is used. I.e., set x = n!.
And then we have
**ISigma_0 + 1) is equivalent to ISigma_0(exp)**
It seems reasonable to take 1) as a given axiom, together with the axioms
for commutative rings with unit. So this leads to the first question:
QUESTION 1. Is there a set of theorems and quoted facts in the standard
published number theory literature in the language of ordered rings which,
when added to the axioms for commutative rings with unit and 1) above,
become equivalent to ISigma_0(exp) = EFA?
In the brief abstract below, we give two axioms about quadratics in two and
four variables that do the trick. Are they an answer to this question?
Close, but not quite. But they certainly suggest a positive answer.
Let's come back to the question of what exactly is the logical status of
the standard published number theory literature restricted to sentences in
the language of ordered rings - under a very strict interpretation
disallowing 1).
QUESTION 2. Under this strict interpretation, are all theorems and quoted
facts in the standard published number theory literature in the language of
ordered rings provable in ISigma_0(exp) = EFA? Provable in ISigma_0?
Provable in ISigma_0(n^log(n))?
Some crucial cases are:
a. For all n there exists m > n such that m is prime. (Euclid's theorem).
b. For all n > 1 there exists a prime p such that n < p <= 2n. (Bertrand's
postulate).
c. For all relatively prime a,b, and integers n, there exists x such that
ax + b > n and ax + b is prime.
These are strongly believed not to be provable in ISigma_0, but this is not
known. Statement a) is a trivial consequence of the other two, and was
proved in ISigma_0(n^log(n)) in
Paris, Wilkie, Woods, Provability of the Pigeonhole Principle and the
existence of infinitely many primes, JSL, Vol. 53, No. 4, Dec. 1988, pp.
1235 - 1244.
CONJECTURE 3. All theorems and quoted facts in the standard published
number theory literature in the language of ordered rings are provable in
ISigma_0(exp) = EFA.
We now consider the analogous questions about the standard published number
theory literature when we exapnd the language. We now make a very strong
conjecture about ISigma_0(exp) = EFA.
CONJECTURE 4. All theorems and quoted facts in the standard published
number theory literature that are naturally formalized in finite set theory
are provable in the finite set theory that is a conservative extension of
ISigma_0(exp) = EFA given in section 3 of posting #76. In particular, all
sentences in the language of ordered rings that follow logically from those
theorems or quoted facts in the standard published number theory literature
that are naturally formalized in finite set theory are provable in
ISigma_0(exp) = EFA.
Conjecture 4 is an upper bound. But we also conjecture that it is exact in
various ways:
CONJECTURE 5. Let T be the formalizations in finite set theory of all
theorems and quoted facts in the standard published number theory
literature that are naturally formalized in finite set theory. Then T
proves ISigma_0(exp) = EFA, and T is provable in the conservative extension
of ISigma_0(exp) = EFA given in section 3 of posting #76. In particular, T
and ISigma_0(exp) = EFA prove the same sentences in the language of ordered
rings.
Conjecture 5 is solved by the systems of posting #77, subject to quibbles.
Can the quibbles be entirely removed? Probably.
Here is a special case of conjecture 4:
CONJECTURE 4a. Fermat's Last Theorem in each particular exponent (a
sentence in the language of rings) is provable in ISigma_0(exp) = EFA.
QUESTION 4b. Is Fermat's Last Theorem in each particular exponent provable
in ISigma_0?
Another special case of Conjecture 4:
CONJECTURE 4c. Fermat's Last Theorem is provable in ISigma_0(exp) = EFA.
Of course, corresponding versions of 4a - 4c can be stated for many other
important theorems of number theory such as Falting's Mordell stuff.
CONJECTURE 6. Let T be the set of all theorems and quoted facts in the
standard published number theory literature that are in the language of
ordered rings with finite sets of integers. Then T is logically equivalent
to the system FCA of #75, section 2.
The lower bound half of Conjecture 6 is solved by the systems of posting
#77, subject to quibbles. Can the quibbles be entirely removed? Probably.
CONJECTURE 7. Let T be the set of all theorems and quoted facts in the
standard published number theory literature that are in the language of
ordered rings with exponentiation. Then T is logically equivalent to
ISigma_0(exp) = EFA.
Note that Conjecture 7 is stronger than simply stating that T and EFA prove
the same ordered ring sentences. We have to actually prove in T, each
instance of induction with respect to a bounded formula in the extended
language. The conjecture can be stated with various new symbols beyond
ordered rings such as:
i) exponentiation;
ii) factorial;
iii) finite sets of integers (see conjecture 6);
iv) summation notation;
v) product notation;
vi) various combinations of these.
**********
QUADRATIC AXIOMS
1/6/00
We axiomatize EFA in strictly mathematical terms, involving only the ring
operations, without extending the language by either exponentiation, finite
sets of integers, or polynomials.
The two axioms beyond commutative rings with unit, are essentially the
least element and least common multiple principles for certain quadratics
in, respectively, two and four variables.
Strictly speaking, one cannot point to a specific place in the literature
where these statements are made, even though they are very elemental and
implicit in the literature. So in this sense they are impeachable.
In contrast, our axiomatizations that use finite sets of integers are
almost entirely immune to this objection; see posting #77.
We conjecture that an axiomatization can be given entirely within the ring
axioms which consists of a finite set of theorems and quoted facts from the
standard published number theory literature. To do this, one might well
want to use
*) for all n > 0 there exists m > 0 such that for all 1 <= i <= n, i divides m,
although it is subject to quibbles. It certainly follows from such theorems
and facts that use factorial.
Let PQV (positive quadratic values) be the system
1. Axioms for commutative ring with unit.
2. For every a,b,c,d,e, the values of axy + bx + cy + d, |x| <= e, have a
least positive upper bound.
3. For every a,b,c,d,e,f,g,h, the values of axy + bzw + cx + dy + ez + fw +
g, with |x|,|y|,|z|,|w| <= h, have a least positive common multiple.
In 2, we use the most common definition of least upper bound. In
partciular, if there are positive values, then the least positive upper
bound is the max. If there are no positive values, then the least positive
upper bound is 1.
In 3, we use the most common definition of common multiple. In particular,
if there are no such values then the least positive common multiple is 1.
THEOREM. The theorems of PQV are exactly the theorems of ISigma_0(exp) in
the language of ordered rings.
(manuscript with proof available upon request).
**********
This is the 78th in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones are:
1:Foundational Completeness 11/3/97, 10:13AM, 10:26AM.
2:Axioms 11/6/97.
3:Simplicity 11/14/97 10:10AM.
4:Simplicity 11/14/97 4:25PM
5:Constructions 11/15/97 5:24PM
6:Undefinability/Nonstandard Models 11/16/97 12:04AM
7.Undefinability/Nonstandard Models 11/17/97 12:31AM
8.Schemes 11/17/97 12:30AM
9:Nonstandard Arithmetic 11/18/97 11:53AM
10:Pathology 12/8/97 12:37AM
11:F.O.M. & Math Logic 12/14/97 5:47AM
12:Finite trees/large cardinals 3/11/98 11:36AM
13:Min recursion/Provably recursive functions 3/20/98 4:45AM
14:New characterizations of the provable ordinals 4/8/98 2:09AM
14':Errata 4/8/98 9:48AM
15:Structural Independence results and provable ordinals 4/16/98
10:53PM
16:Logical Equations, etc. 4/17/98 1:25PM
16':Errata 4/28/98 10:28AM
17:Very Strong Borel statements 4/26/98 8:06PM
18:Binary Functions and Large Cardinals 4/30/98 12:03PM
19:Long Sequences 7/31/98 9:42AM
20:Proof Theoretic Degrees 8/2/98 9:37PM
21:Long Sequences/Update 10/13/98 3:18AM
22:Finite Trees/Impredicativity 10/20/98 10:13AM
23:Q-Systems and Proof Theoretic Ordinals 11/6/98 3:01AM
24:Predicatively Unfeasible Integers 11/10/98 10:44PM
25:Long Walks 11/16/98 7:05AM
26:Optimized functions/Large Cardinals 1/13/99 12:53PM
27:Finite Trees/Impredicativity:Sketches 1/13/99 12:54PM
28:Optimized Functions/Large Cardinals:more 1/27/99 4:37AM
28':Restatement 1/28/99 5:49AM
29:Large Cardinals/where are we? I 2/22/99 6:11AM
30:Large Cardinals/where are we? II 2/23/99 6:15AM
31:First Free Sets/Large Cardinals 2/27/99 1:43AM
32:Greedy Constructions/Large Cardinals 3/2/99 11:21PM
33:A Variant 3/4/99 1:52PM
34:Walks in N^k 3/7/99 1:43PM
35:Special AE Sentences 3/18/99 4:56AM
35':Restatement 3/21/99 2:20PM
36:Adjacent Ramsey Theory 3/23/99 1:00AM
37:Adjacent Ramsey Theory/more 5:45AM 3/25/99
38:Existential Properties of Numerical Functions 3/26/99 2:21PM
39:Large Cardinals/synthesis 4/7/99 11:43AM
40:Enormous Integers in Algebraic Geometry 5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees 5/25/99 5:11PM
43:More Enormous Integers/AlgGeom 5/25/99 6:00PM
44:Indiscernible Primes 5/27/99 12:53 PM
45:Result #1/Program A 7/14/99 11:07AM
46:Tamism 7/14/99 11:25AM
47:Subalgebras/Reverse Math 7/14/99 11:36AM
48:Continuous Embeddings/Reverse Mathematics 7/15/99 12:24PM
49:Ulm Theory/Reverse Mathematics 7/17/99 3:21PM
50:Enormous Integers/Number Theory 7/17/99 11:39PN
51:Enormous Integers/Plane Geometry 7/18/99 3:16PM
52:Cardinals and Cones 7/18/99 3:33PM
53:Free Sets/Reverse Math 7/19/99 2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry 8/27/99 3:01PM
57:Fixpoints/Summation/Large Cardinals 9/10/99 3:47AM
57':Restatement 9/11/99 7:06AM
58:Program A/Conjectures 9/12/99 1:03AM
59:Restricted summation:Pi-0-1 sentences 9/17/99 10:41AM
60:Program A/Results 9/17/99 1:32PM
61:Finitist proofs of conservation 9/29/99 11:52AM
62:Approximate fixed points revisited 10/11/99 1:35AM
63:Disjoint Covers/Large Cardinals 10/11/99 1:36AM
64:Finite Posets/Large Cardinals 10/11/99 1:37AM
65:Simplicity of Axioms/Conjectures 10/19/99 9:54AM
66:PA/an approach 10/21/99 8:02PM
67:Nested Min Recursion/Large Cardinals 10/25/99 8:00AM
68:Bad to Worse/Conjectures 10/28/99 10:00PM
69:Baby Real Analysis 11/1/99 6:59AM
70:Efficient Formulas and Schemes 11/1/99 1:46PM
71:Ackerman/Algebraic Geometry/1 12/10/99 1:52PM
72:New finite forms/large cardinals 12/12/99 6:11AM
73:Hilbert's program wide open? 12/20/99 8:28PM
74:Reverse arithmetic beginnings 12/22/99 8:33AM
75:Finite Reverse Mathematics 12/28/99 1:21PM
76: Finite set theories 12/28/99 1:28PM
77:Missing axiom/atonement 1/4/00 3:51PM
More information about the FOM
mailing list