FOM: 66:PA/an approach
Harvey Friedman
friedman at math.ohio-state.edu
Thu Oct 21 20:02:32 EDT 1999
This is the 65th 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
In posting #65, we made a number of general and specific conjectures about
the completeness and special status of various formal systems, especially
PA = Peano Arithmetic. One of the conjectures is:
*Let phi be a scheme in the language of PA with
=,not,and,or,implies,0,S,+,x,forall,therexists, variables x_1,x_2,..., and
schematic letters A_1,A_2,..., with at most 14 occurrences of symbols. Then
each instance of phi is provable in PA, or the universal closure of some
instance of phi is refutable in EFA.*
The number 14 is used because the usual axiomatization of PA has all axioms
with at most 14 symbols, where induction is viewed as a scheme. This
conjecture and related stronger conjectures would give preferred status to
PA, as indicated in posting #65.
The conjecture is already interesting and difficult without schemes and EFA:
*Let phi be a formula in the language of PA with
=,not,and,or,implies,0,S,+,x,forall,therexists, variables x_1,x_2,..., with
at most 14 occurrences of symbols. Then the universal closure of phi is
provable or refutable in PA.*
It is also interesting and difficult in this weakened form:
*Let phi be a quantifier free formula in the language of PA with
=,not,and,or,implies,0,S,+,x, and variables x_1,x_2,..., with at most 14
occurrences of symbols. Then the universal closure of phi is provable or
refutable in PA.*
This is the form that we address in this posting. Let phi = A(x_1,...,x_k)
be the given quantifier free formula.
The conjecture is obviously true if all equations in A are linear, using
the decision procedure for Presburger Arithmetic.
I believe that this conjecture can be established with a great deal of
human/machine interaction as well as some serious number theory. The
relevant number theory is of course Diophantine theory, where some of it is
looked at in novel ways that would not be particularly natural without this
conjecture in mind.
Basically, there are too many cases to handle, although the computer can
cut them down considerably. But to cut things down to really manageable
size, one should find the right theorems.
One theoretical idea that seems really relevant is to extend work of Carl
Ludwig Seigel in certain ways that may or may not have been done.
LEMMA 1. (Seigel) There is a decision procedure for determining whether a
given multivariate quadratic with integer coefficients has an integral
solution.
LEMMA 2. (???) There is a decision procedure for determining whether a
given multivariate quadratic with integer coefficients has an integral
solution which additionally satisfies a given finite set of linear
inequalities.
Proof: I don't know a reference, and I am not sure that this is known,
although I suspect that it is known. I talked to Barry Mazur and John
Conway, who did not know off the top of their head, and were certainly
interested in this question. Let's assume this is known. QED???
LEMMA 3. Lemma 2 is provable in PA. So each problem instance is provable or
refutable in PA.
Proof: Expected from the proof of Lemma 2. Certainly is the case for the
proof of Lemma 1. QED???
LEMMA 4. Let K be the set of all sentences of the following form: (forall
x_1,...,x_k in Z)(A(x_1,...,x_k)), where A is a Boolean combination of
linear and quadratic inequalities with integer coefficients, and there is
precisely one inequality appearing in A that is not linear, perhaps with
multiple occurrences in A. Then every element of K is provable or refutable
in PA.
Proof: It suffices to decide all sentences of the form (therexists
x_1,...,x_k in Z)(B), where B is a Boolean combination of inequalities of
the form P(x_1,...,x_k) >= 0, where P is linear or quadratic, with integer
coefficients, and exactly one of the P's is quadratic. Let P be the
quadratic, and P_1,...,P_r be the linears.
We can put the sentence in the form (therexists x_1,...,x_k in
Z)(P(x_1,...,x_k) >= 0 and B') or (therexists x_1,...,x_k)(P(x_1,...,x_k) <
0 and B''), where B',B'' use only the P_i's. This disjunct can be put in
the form (therexists x_1,...,x_k,a,b,c,d in Z)(P(x_1,...,x_k) = a^2 + b^2 +
c^2 + d^2 and B') or (therexists x_1,...,x_k,a,b,c,d)(P(x_1,...,x_k) =
-(a^2 + b^2 + c^2 + d^2 + 1) and B''). Now apply Lemma 3. QED???
Now assume that A is a quantaifier free formula in the language of PA with
at most 14 symbols as in the Conjecture we are addressing. Lemma 4 will
come in below. Note that Lemma 4 is more than what we can directly use,
since it goes beyond the language of PA.
Below, we consider the equations in A counting repetitions. REMINDER: Since
we are using PA, variables range over N = nonnegative integers.
I. A HAS EXACTLY ONE EQUATION.
Without loss of generality, we assume that A is the negation of the equation.
Ia. Degree seven and higher.
Impossible. A term of degree seven or higher has at least 13 symbols.
Therefore the equation has at least 15 symbols.
Ib. Degree six.
We can assume that the left side is of degree six, and so has at least
eleven symbols. The right side must be a variable or 0. Trivial.
Ic. Degree five.
Let A = not(u = v), where u is of degree five. Let us first assume that u
has nine symbols, and so is a product of five variables. Then v has at most
3 symbols. We can assume v is of the form 0, y, S0, Sy, y*z, y+z, SSy,
where y is a variable. These are easily handled.
Now assume u has ten symbols. Since it is of degree five, a single S must
have been inserted. Now v has at most 2 symbols. So v is either 0,S0,y,Sy.
These cases are easily handled.
Now assume u has 11 symbols. Then v is either 0 or y. The structure of u is
extremely limited, and so this is easily handled.
Id. Degree four.
Let us first assume that u has seven symbols, and so is a product of four
variables. Then v has at most five symbols. If v has at most three symbols
then we can argue as above. If v has four symbols then we can assume v is
of the form y + Sz, y * Sz, SSSy. These cases are trivially handled.
Now assume that u has eight symbols, and so is the result of inserting a
single S in a product of four variables. Then v has at most four symbols.
If v has at most 2 symbols we can argue as above. If v has three symbols
then we can assume v is y*z, y+z, SSy. These are easily handled. If v has
four symbols then we can assume v is y + Sz, y * Sz, SSSy. These are also
easily handled.
Now assume that u has nine symbols. Then v has at most 3 symbols, and so we
can assume v is of the form 0, y, S0, Sy, y*z, y+z, SSy. One has to catalog
the possible forms for u, but I do not expect any difficulties here.
Ie. Degree three.
This is the most dicey, and interesting case under I. E.g., x*x*x = y*y +
SS0, with 13 symbols, so when negated as required, it has exactly 14
symbols, the limit. Of course, we know that this has a solution. But I
think that an exhaustive analysis will only come up with cubics which are
known to have or not have a solution in N.
II. A HAS FOUR OR MORE EQUATIONS
If they are all linear, then we are done. If at least one is nonlinear,
then it takes up at least five symbols, in addition to the other three, for
a total of 14 symbols. But we still need connectives, and so this is
impossible.
So there are at most three equations.
III. CUBIC, ANYTHING, ANYTHING
The cubic must contain 7 symbols and the others at least 3 symbols each for
a total of 13 symbols. But two connectives are needed, and so this is
impossible.
IV. QUADRATIC, ANYTHING, ANYTHING, OR QUADRATIC, LINEAR
The second case is taken care of by Lemma 4. The first case is taken care
of by Lemma 4 unless it is Quadratic, Quadratic, Anything. In this case,
quadratics take up 5 symbols, and so this accounts for 13 symbols, with no
room for connectives.
V. QUADRATIC, QUADRATIC
Write this as u = v, w = z, where u,w are quadratic. We can assume that we
either have the two equations or their negations connected by a conjunction
- four possibilities - or the disjunction of the two, or one implies the
other, or one implies the negation of the other. The four conjunction cases
can be split into single quadratic cases.
The disjunction case is trivial. This leaves the implication cases. These
may have to be examined carefully. This amounts to very very special cases
of deciding whether every integral solution to one quadratic equation with
integer coefficients is a solution to another quadratic equation with
integer coefficients, and also whether two quadratic equations with integer
coefficients have a common integral solution. Bear in mind, that we are
talking about extremely special quadratic equations. There probably is a
relevant theory. I have been asking around.
VI. QUADRATIC, CUBIC
The quadratic takes at least five symbols, and the cubic at least seven
symbols, with two remaining symbols possible. If they take exactly five and
seven symbols, then the problem is trivial. If the quadratic takes five
symbols and the cubic takes eight symbols, then there is only one
connective symbol, and we have a very constrained situation that is easy to
handle. Same if the quadratic takes six symbols and the cubic takes seven
symbols.
VII. QUADRATIC, QUARTIC OR HIGHER
Impossible.
VIII. CUBIC, LINEAR
First take care of the case that the linear has only 3 symbols. In this
case, there are a few more propositional combinations to consider, but this
won't be a problem.
IX. CUBIC, CUBIC OR HIGHER
Impossible.
X. QUARTIC, LINEAR
The quartic B has at least 9 symbols and the linear C has at least 3
symbols. B & C, B or C, notB & C, B & notC can be easily taken care of,
using I. B implies C, B implies notC, C implies B, C implies notB should
also be easy using a little theory. First look at the 9,3 split. This
constrains the quartic a lot. Then look at the 9,4 split. Then there must
be only one connective. Finally, look at the 10,3 split, again only one
connective.
XI. QUARTIC, NONLINEAR
Impossible.
XII. QUINTIC AND HIGHER, ANYTHING
Impossible.
COPY OF LETTER TO SOME FAMOUS CORE MATHEMATICIANS
Hi! Good to hear some of your voices again.
1. As I asked some of you: can you tell whether a quadratic equation with
integer coefficients and several variables has an integral solution which
also satisfies a given finite set of linear inequalities?
2. Can you tell whether two quadratic equations with integer coefficients
and several variables have a simultaneous integral solution? Of course, if
you ask for more and more quadratics, then you can simulate Hilbert's tenth
problem, which is algorithmically undecidable.
3. Can you tell whether every integral solution to one quadratic equation
with integer coefficients and several variables is a solution to another
such quadratic equation?
Even partial results like you can do it if the number of variables is small
(not large!) and/or the coefficients are really small, would be very
useful.
Is there anybody especially knowledgeable about such things, or its
literature, in addition to you guys?
Thanks very much for your time.
Harvey
More information about the FOM
mailing list