FOM: 56:Consistency of Algebra/Geometry
Harvey Friedman
friedman at math.ohio-state.edu
Fri Aug 27 10:01:43 EDT 1999
This is the 56th 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
The following is an abbreviated version from a rough draft. Such
consistency proofs are known to be very treacherous matters. Even such a
consistency proof within PRA = primitive recursive arithmetic (and related
conservation extension results proved in PRA) does not appear anywhere in
good form as far as I know, although it is discussed in Simpson's book and
there were plans to have my proof of this appear in an old joint paper of
Simpson, Smith, and me (it never made it there). Of course, doing this is
EFA is incomparably more delicate.
The full rough draft is too long for posting on the FOM. It will appear on
my website in the near future. Meanwhile, if anybody wants to see it in its
present condition, they can get it from me by e-mail.
This can be viewed as a strong success for Hilbert's program. Of course,
full success was dashed by Godel.
A CONSISTENCY PROOF FOR ELEMENTARY ALGEBRA AND GEOMETRY
by
Harvey M. Friedman
Department of Mathematics
Ohio State University
August 27, 1999
ABSTRACT
We give a consistency proof within a weak fragment of arithmetic of
elementary algebra and geometry. For this purpose, we use EFA (exponential
function arithmetic), and various first order theories of algebraically
closed fields and real closed fields.
We actually prove in EFA that RCF (real closed fields) is consistent and
complete. The completeness proof is an adaptation of known constructions.
We also obtain a proof in EFA that every quantifier free formula provable
in RCF has a quantifier free proof in the theory of real fields and in the
theory of ordered fields.
As a Corollary, we obtain an interpretation of RCF into EFA in the sense of
model theory, as well as interpretations of finitely axiomatized extensions
of RCF into EFA.
Negative results show that various fragments of EFA based on subexponential
functions do not suffice.
The development can be used to provide fixed length iterated exponential
estimates in connection with Hilbert¹s seventeenth problem.
INTRODUCTION
to be written. discusses Hilbert¹s program briefly. discusses systems of
arithemetic briefly. introduces EFA = exponential function arithmetic.
reference to Hajek/Pudlak. disclaimer that we make no attempt here to
obtain more precise information.
1. PRELIMINARIES ABOUT LOGIC
In the free variable predicate calculus with equality, we start with a
signature sigma consisting of a set of constant, relation, and function
symbols. Formulas are built up in the usual way using the variables
v1,v2,..., connectives not, or, and, implies, iff, =, and the symbols in
sigma. There are no quantifiers.
The variables are literally the vi, i >= 1. We use this to define the
universal closure of a formula phi. This is obtained from phi by
successively universally quantifying by the free variables of phi in
reverse order of their subscripts. If phi is a sentence then the universal
closure of phi is phi.
The logical axioms and rules of inference of free variable predicate
caluclus presented (Hilbert style).
THEOREM 1.1. Let T be a set of quantifier free formulas and phi be a
quantifier free formula based on the signature sigma. The following are
equivalent.
i) Every equality model universally satisfying all elements of X
universally satisfies phi;
ii) phi is free variable provable in T;
iii) some finite set of subsitution instances of elements of T and the
equality axioms tautologically implies phi.
THEOREM 1.2. (EFA) Let T be a finite set of quantifier free formulas and
phi be a quantifier free formula based on the signature sigma. The
following are equivalent.
i) phi is free variable provable in T;
ii) some set of substitution instances of elements of T and the equality
axioms tautologically implies phi.
We use the following terminology in connection with ii) above. An
instantiation of T is a finite set of substitution instances of elements of
X together with a finite set of substitution instances of equality axioms.
All of this is required to take place in the signature sigma.
A special proof in T of a quantifier free formula phi in the language of
sigma is an instantiation of T which tautologically implies phi. Thus
condition ii) above asserts that ³phi has a special proof in T.²
In the predicate calculus with equality, we start with a signature sigma
consisting of a set of constant, relation, and function symbols. Formulas
are built up in the usual way using the variables v1,v2,..., connectives
not, or, and, implies, iff, quantifiers forall, therexists, =, and the
symbols in sigma.
Axioms and rules of inference of predicate calculus with equality presented
(Hilbert style).
THEOREM 1.4. Let T be a set of formulas and phi be a formula based on the
signature sigma. The following are equivalent.
i) Every equality model universally satisfying all elements of T
universally satisfies phi;
ii) phi is provable in T.
THEOREM 1.5. Let T be a set of quantifier free formulas and phi be a
quantifier free formula based on the signature sigma. The following are
equivalent.
i) phi is provable in T;
ii) phi is free variable provable in T;
iii) phi has a special proof in T.
Notice that Theorem 1.5 does not mention infinitary objects. However, we
know that it cannot be proved in EFA. The usual proof of Theorem 1.5 is to
pass through Theorem 1.4, which is infinitary. Theorem 1.5 can also be
proved using the cut elimination theorem for predicate calculus with
equality. However, the cut elimination theorem can only be proved by going
slightly beyond EFA.
Let T be a set of existential formulas in sigma. An iterated instantiation
of T is any finite set of quantifier free formulas obtained in the
following way. First select an element of T and make any term substitution
not mentioning the bound variables in that element of T. Then add variables
witnessing their existential quantifiers. These witness variables must all
be distinct, and distinct from any variables appearing earlier. Then select
another element of T and make any term substitution not mentioning the
bound variables in that element of T. Then add variables witnessing their
existential quantifiers, which must be distinct and distinct from all
variables appearing earlier. Continue in this manner for finitely many
steps.
NOTE: In subsequent sections, all formulas in the T¹s considered will have
at most one existential quantifier, and so at most one witness variable is
introduced at each step.
For each introduction of witness variables, there is the corresponding
witness formula asserting that the substitution instance of the element of
X in question holds at the witness variables.
The iterated instantiation consists of all these witness formulas. It
should be noted that some elements of T may be quantifier free.
Substitution instances of them may appear in the iterated instantiation
without introducing any witness variables.
Let phi be an existential formula in sigma. A special proof of phi in T is
an iterated instantiation X of the union of T and the set of equality
axioms, such that
i) X tautologically implies some instantiation of the existential
quantifiers in phi by terms;
ii) no witness variables in T appear free in phi.
THEOREM 1.6. Let T be a set of existential formulas and phi be an
existential formula. The following are equivalent.
i) phi is provable in T;
ii) phi has a cut free proof from the universal closures of elements of T
and the equality axioms;
iii) phi has a special proof in T.
EFA¹ is EFA with indefinitely iterated exponentiation, and bounded
induction with respect to the larger signature.
THEOREM 1.7. (EFA) Let T be a finite set of existential formulas and phi be
an existential formula. Then phi has a cut free proof from universal
closures of elements of T and the equality axioms if and only if phi has a
special proof in T. Also, Theorem 1.6 for finite T is provable in EFA¹. In
fact, ii) implies i) is provably equivalent to EFA¹ over EFA for finite T.
2. QUANTIFIER ELIMINATION AND CONSISTENCY
Define E0(n) = n, Ec+1(n) = 2^Ec(n).
The special consistency of an existential theory asserts that the formula x
not= x does not have a special proof in the theory. Of course, the
consistency of any theory asserts that the formula x not= x does not have a
proof in the theory. According to Theorem 1.7, it is provable in EFA that
the consistency and the special consistency are equivalent for existential
theories with finitely many axioms.
It is the purpose of this section to prove that if, provably in EFA, an
existential theory has a certain property related to quantifier
elimination, then, provably in EFA, consistency is equivalent to special
consistency. We also obtain some additional results involving conservative
extensions.
An EFA existential theory T consists of a finite signature, an integer
constant c >= 1, and a Turing machine TM, such that EFA proves
i) TM accepts or rejects strings in time bounded by Ec(x);
ii) TM accepts only existential formulas in the signature.
Proofs and special proofs in T refer to proofs and special proofs in the
set of all existential formulas accepted by TM.
THEOREM 2.1. Suppose T is an EFA existential theory. Then EFA¹ proves the
equivalence of consistency and special consistency of T. In fact, EFA¹
proves that every existential formula has a proof in T if and only if it
has a special proof in T.
We make the following definitions in EFA. For formulas phi, write #(phi)
for the size of phi, which is the total number of symbols in phi, assuming
a base 2 representation of all subscripts of variables. The size of a proof
or a special proof is the total number of symbols involved, again with base
2 representation of all subscripts of variables.
We say that T is an EFA qe existential theory if and only if T is an EFA
existential theory with constants c such that the following is provable in
EFA.
Let (therexists x)(phi(x,y1,...,yn)) be a formula in the signature of X,
where phi is quantifier free, x,y1,...,yn are distinct variables, and all
variables in phi are among those shown. There is a quantifier free
psi(y1,...,yn) with all variables among those shown and special proofs of
phi(x,y1,...,yn) arrows psi(y1,...,yn)
and
(therexists x)(psi(y1,...,yn) implies phi(x,y1,...,yn))
in T of size <= 2^[log(#(phi))^Ec(n)].
We say that T is a strong EFA qe existential theory if and only if
i) T is an EFA existential theory with integer constant c;
ii) EFA proves that T is specially consistent in the sense that there is no
special proof in T of any quantifier free formula and its negation;
iii) EFA proves that if phi is a quantifier free sentence in the signature
of T, then there is a special proof of phi or of notphi in T of size <=
Ec(#(phi)) using only the quantifier free elements of T;
iv) the following is provable in EFA:
Let (therexists x)(phi(x,y1,...,yn)) be a formula in the signature of X,
where phi is quantifier free, x,y1,...,yn are distinct variables, and all
variables in phi are among those shown. There is a quantifier free
psi(y1,...,yn) with all variables among those shown and special proofs of
phi(x,y1,...,yn) arrows psi(y1,...,yn)
and
(therexists x)(psi(y1,...,yn) implies phi(x,y1,...,yn))
in T of size <= 2^[log(#(phi))^Ec(n)], where the first special proof uses
only the quantifier free formulas in T.
Until further notice, we fix an EFA qe existential theory T with constant
c. In EFA, let H map each quantifier free phi(x,y1,...,yn) to the first
special proofs given by the definition, where they are ordered first by
size and second by lexicographic order. We also let H¹ map each quantifier
free phi(x,y1,...,yn) to to the quantifier free formula psi(y1,...,yn) used
in the value of H.
Obviously EFA proves the inequalities H(x),H¹(x) <= 2^log(x)^Ec(n)] in
terms of sizes of formulas and special proofs, where n is one less than the
number of variables in the formula x. Obviously if c is, say, at least 4,
then EFA proves the inequalities H(x),H¹(x) <= Ec(x). We assume that c >= 4.
In order to simultaneously handle the case of a strong EFA qe existential
theory, we assume that H gives the first special proofs given by the
definition of strong EFA qe existential theory if this is possible. We can
do this, since we have placed a size bound on the special proofs being
searched for.
For every formula phi we define a quantifier free formula phi* in the
language of fields as follows. If phi is atomic then phi* = phi. (notphi)*
= not(phi*). (phi or psi)* = phi* or psi*. (phi & psi)* = phi* & psi*. (phi
implies psi)* = phi* implies psi*. (therexists x)(phi)* = H¹((therexists
x)(phi*)). (forall x)(phi)* = (not(therexists x)(notphi))*. We have to
argue that this definition can be given in EFA.
LEMMA 2.2. There is a bounded formula rho(x,y) with the free variables
shown, and a constant c¹ such that the following is provable in EFA.
rho(x,y) defines a function obeying the definition of the * function.
(forall x)(therexists y <= Ec¹(x))(rho(x,y)).
LEMMA 2.3. There is an integer c¹ such that the following is provable in
EFA. Let phi be a formula provable in predicate calculus. Then phi* has a
special proof in T of size <= Ec¹(#(phi)).
LEMMA 2.4. There is an integer c¹ such that the following is provable in
EFA. Let phi be quantifier free and have a special proof in T of size <= n.
Then (forall x)(phi)* has a special proof in T of size <= Ec¹(#(phi))+n.
LEMMA 2.5. There is an integer c¹ such that the following is provable in
EFA. Let phi is quantifier free and have a special proof in T of size <= n.
Then the * of the universal closure of phi has a special proof in T of size
<= Ec¹(n).
LEMMA 2.6. There is an integer c¹ such that the following is provable in
EFA. The * of the universal closure of every axiom phi of T has a special
proof in X of size <= Ec¹(#(phi)).
LEMMA 2.7. There is an integer c¹ such that the following is provable in
EFA. Let phi be a formula with a proof in T of size <= n. Then phi* has a
special proof in T of size <= Ec¹(n).
LEMMA 2.8. There is an integer c¹ such that the following is provable in
EFA. Let phi be an existential formula with a proof in T of size <= n. Then
phi has a special proof in T of size <= Ec¹(n).
LEMMA 2.9. There is an integer c¹ such that the following is provable in
EFA. Assume T is a strong EFA qe existential theory. Let phi be a
quantifier free formula with a proof in T of size n. Then phi has a special
proof in the quantifier free part of T of size <= Ec¹(n).
LEMMA 2.10. There is an integer c¹ such that the following is provable in
EFA. Let phi be a formula. There is a proof of phi iff phi* in T of size <=
Ec¹(#(phi)).
THEOREM 2.11. Let T be an EFA qe existential theory. Then EFA proves that
every existential formula provable in T has a special proof in T. And EFA
proves that every formula is provably equivalent, in T, to a quantifier
free formula. Let T be a strong EFA qe existential theory. Then EFA proves
that T is consistent. EFA proves that every quantifier free formula
provable in T has a special proof in the quantifier free part of T. And EFA
proves that every sentence is provable or refutable in T.
THEOREM 2.12. Let T be an EFA qe existential theory. There is an integer
constant c¹ such that the following are provable in EFA. Every existential
formula with a proof in T of size n has a special proof in T of size <=
Ec¹(n). For every formula phi, there is a quantifier free formula psi such
that phi iff psi has a proof in T of size <= Ec¹(#(phi)). Let T be a strong
EFA qe existential theory. There is an integer constant c¹ such that the
following are provable in EFA. Every quantifier free formula with a proof
in T of size n has a special proof in the quantifier free part of T of size
<= Ec¹(n). Every sentence phi is provable or refutable in T by a proof of
size <= Ec¹(#(phi)).
3. CONSISTENCY AND COMPLETENESS OF ALGEBRAICALLY CLOSED FIELDS
We formulate the field axioms FLD in the signature 0,1,dot,-,x,/ with =, as
follows.
1. a+0 = 0, a+b = b+a, a+(b+c) = (a+b)+c, a+(-a) = 0.
2. ax0 = 0, ax1 = a, axb = bxa, ax(bxc) = (axb)xc.
3. ax(b+c) = axb + axc, a/0 = 0, b not= 0 implies bx(a/b) = a.
4. 1 not= 0, axb = 0 implies (a = 0 or b = 0).
FLD(0) consists of FLD together with the axioms
5. 1+1+...+1 not= 0, where there is at least one 1.
Let p be a prime. FLD(p) consists of FLD together with the axioms
6. 1+1+...+1 not= 0, where there are at least one but fewer than p 1¹s.
7. 1+1+...+1 = 0, where there are p 1¹s.
Whenever we write FLD(p), it is understood that p is either a prime or 0.
If p is a prime or 0, then we write ACF(p) for FLD(p) plus the root axioms
(therexists x)(x^n + c1x^n-1 + ... + cn-1x + cn = 0)
where n >= 1 and the c¹s are variables other than x.
LEMMA 3.1. ACF(0) is an EFA qe existential theory with constant 4.
Moreover, clause iv) in the definition of strong EFA qe existential theory
holds, with constant 4.
LEMMA 3.2. (EFA) ACF(0) is specially consistent in the sense that there is
no special proof of any quantifier free formula and its negation.
LEMMA 3.3. (EFA) If phi is a quantifier free sentence in the signature of
fields, then there is a special proof of phi or of notphi of size <=
E4(#(phi)) using only the quantifier free axioms of ACF(0).
LEMMA 3.4. ACF(0) is a strong EFA qe existential theory.
We also want to treat the characteristic p case. We want to prove in EFA
that certain properties of ACF(p) hold for all primes p. This is stonger
than saying that for all primes p, EFA proves certain properties of ACF(p).
In order to get such uniformity, we need to expand the concept of (strong)
EFA (qe) existential theory to that of a (strong) EFA (qe) existential
theory family. This is done in the obvious way.
We can view the ACF(p), p prime, as an EFA existential theory family T* in
the obvious way. Here it is convenient to take T*(n) to be ACF(n) if n is
prime; ACF(0) otherwise. We write this EFA existential theory family as
ACF*.
LEMMA 3.5. ACF* is a strong EFA qe existential theory.
THEOREM 3.8. (EFA) Let p be a prime or 0. ACF(p) is consistent and
complete, and conservative over FLD(p) for quantifier free formulas. Every
existential formula provable in ACF(p) has a special proof in ACF(p). Also,
there exists a positive integer c such that EFA proves the preceding
statements with upper bounds using the function Ec.
4. COMPLETENESS OF REAL CLOSED FIELDS WITH INTERMEDIATE VALUE THEOREM
FLD(<) is the usual theory of ordered fields, whose signature is the
signature of fields together with the binary relation symbol <. The axioms
are as follows.
1. FLD.
2. < is a strict linear ordering of the domain, where 0 < 1.
3. (x > 0 & y > 0) implies x+y > 0 & xdoty > 0.
RCFI is the theory of real closed fields based on the intermediate value
theorem for polynomials. Its signature is the signature of ordered fields.
The axioms are as follows.
1. FLD(<).
2. (therexists y)(x > 0 implies y^2 = x).
3. (therexists x)((b < c & P(b) < u < P(c)) implies b < x < c & P(x) = u),
where P(x) is x^n + a1x^n-1 + ... + an-1x + an, n >= 1.
LEMMA 4.1. RCFI is an EFA qe existential theory with constant 4. Moreover,
clause iv) in the definition of strong EFA qe existential theory holds,
with constant 4.
LEMMA 4.2. EFA proves that if phi is a quantifier free sentence in the
signature of RCFI, then there is a special proof of phi or of notphi in
FLD(<) of size <= Ec(#(phi)).
LEMMA 4.3. Suppose EFA proves the special consistency of RCFI. Then RCFI is
a strong EFA qe existential theory with constant 4.
THEROEM 4.4. (EFA) RCFI is complete. Every existential formula provable in
RCFI has a special proof in RCFI. If RCFI is specially consistent then RCFI
is consistent, and is a conservative extension of FLD(p) for quantifier
free formulas. Also, there exists a positive integer c such that EFA proves
the preceding statements with upper bounds using the function Ec.
5. SPECIAL CONSISTENCY OF REAL CLOSED FIELDS
The weakest commonly considered theory of real closed fields is RCF, whose
signature is the same as that of fields, and whose axioms are as follows.
1. FLD.
2. (therexists y)(y^2 = x or y^2 = -x).
3. x1^2 + ... + xn^2 not= -1, where n >= 1.
4. (therexists x)(xn + a1xn-1 + ... + an-1x + an = 0), where n is odd.
We let RF be the subsystem consisting of axioms 1 and 3. RF is the
quantifier free part of RCF.
Let M be a finite relational structure in a finite relational type, with a
distinguished subset of the domain that we always write as A. We
inductively define M[0] = A, and M[i+1] to be the elements of M[i] together
with all values of the functions of M at arguments from M[i].
Let d >= 0 and phi be a quantifier free formula in the language of M. We
say that phi is d-true in M if and only if phi holds for all assignments
from M[d] to the variables appearing in phi.
We apply these concepts to the language of fields, =,0,1,+,-,dot,/.
Let d >= 0. A d-semifield is a relational structure in the language of
fields in which the the field axioms are d-true.
A d-real semifield is a d-semifield in which the statement
x1^2 + ... + xd^2 not= -1
written left associatively, is d-true.
LEMMA 5.1. (EFA) For all d >= 0, there is a d-real semifield.
LEMMA 5.2. (EFA) Let d >= 16 and M = (D,A,0,1,+,-,dot,/) be a 16d-real
semifield. Let a be an element of M[d] that is not the left associative sum
of d squares of elements of M[6d]. Then there is a d-real semifield M¹ =
(D¹,A¹,0,1,+¹,-¹,dot¹,/¹) extending M and x in A¹ such that x^2 = -a.
LEMMA 5.3. (EFA) Let d >= 16 and M = (D,A,0,1,+,-,dot,/) be a 16d-real
semifield. Let a in M[d]. Then there is a d-real semifield M¹ =
(D¹,A¹,0,1,+¹,-¹,dot¹,/¹) extending M and x in A¹ such that x^2 = a or x^2
= -a.
LEMMA 5.4. (EFA) Let d >= 32 and M = (D,A,0,1,+,-,dot,/) be a 16d^4-real
semifield. Let 1 <= i <= d-2 and P1(x),...,Pd(x),Q(x) be polynomials of
degree <= d with coefficients from M[16d^3(d-1)]. Let Q(x) be of odd
degree. Then P1(x)^2 + ... + Pd(x)^2 + 1 is not divisible by Q(x) by long
division in M.
LEMMA 5.5. (EFA) Let d >= 32 and M = (D,A,0,1,+,-,dot,/) be a 16d^4-real
semifield. Let P(x) be a polynomial in one variable of odd degree <= d with
coefficients from M[d]. Then there is a d-real semifield M¹ =
(D¹,A¹,0,1,+¹,-¹,dot¹,/¹) extending M and x in A¹ such that P(x) = 0.
LEMMA 5.6. (EFA) Let X be an iterated instantiation of axioms 2 and 4 of
RCF, and n >= 1. There is an n-real semifield M = (D,A,0,1,+,-,dot,/) and
an interpretation of X in which the variables are assigned elements of A.
LEMMA 5.7. (EFA) Let X be an iterated instantiation of RCF, and n >= 1.
There is an n-real semifield M = (D,A,0,1,+,-,dot,/) and an interpretation
of X in which the variables are assigned elements of A. There is no special
proof in RCF of 0 not= 0.
LEMMA 5.8. (EFA) Let X be an iterated instantiation of RCF whose first
variables introduced are by term substitution and are x1,...,xr without
repetition, and let n >= 1. Let M0 be any m-real semifield, where m is
sufficiently large relative to X and n. Assume that x1,...,xr have been
assigned elements of A0. Then there exists M0 containedin ... containedin
Mn, where Mn is an n-real semifield, and X has an interpretation extending
the interpretation of x1,...,xr. Furthermore, there is an integer constant
c >= 1 such that, provably in EFA, we can take m = Ec(#(X)+n).
THEOREM 5.9. (EFA) RCF is specially consistent; i.e., there is no special
proof in RCF of 0 not= 0. A quantifier free formula has a special proof in
RCF if and only if it has a special proof in RF. There is an integer
constant c >= 1 such that the following is provable in EFA. Let phi be a
quantifier free formula. If there is a special proof of phi in RCF of size
n then there is a special proof in RF of size <= Ec(n).
THEOREM 5.10. (EFA¹) RCF is consistent and complete, and conservative over
RF for quantifier free formulas. Every existential formula provable in RCF
has a special proof in RCF. Also, there exists a positive integer c such
that EFA¹ proves the preceding statements with upper bounds using the
function Ec.
6. REDUCTION OF REAL CLOSED FIELDS FROM INTERMEDIATE VALUES TO COMPLEX ROOTS
The axioms of RCF(fta) are as follows. [fta = fundamental theorem of algebra]
1. RF.
2. There exists a complex z such that z^n + a1z^n-1 + ... + an-1z + an = 0.
Here n >= 1.
Note that 2 is stated with coefficients from the real field, and not more
generally with coefficients from the complex numbers. However, this can be
formally derived. Thus we take the axioms of RCF(fta¹) to be
1. RF.
2. There exists a complex z such that z^n + a1z^n-1 + ... + an-1z + an,
where the a¹s are complexes. Here n >= 1.
LEMMA 6.1. There is a positive integer c such that the following is
provable in EFA. Let phi be an axiom of RCF(fta¹). Then phi has a special
proof in
RCF(fta) of size <= Ec(#(phi).
We let RCF(fact) be in the signature of fields with the following axioms.
1. RF.
2. (therexists y)(y^2 = x or y^2 = -x).
3. x^n + a1x^n-1 + ... + an-1x + an can be factored into linear and
quadratic factors, the sum of whose degrees is n. Here n >= 1.
LEMMA 6.2. There is a positive integer c such that the following is
provable in EFA. Let phi be an axiom of RCF(fact). Then phi has a special
proof in RCF(fta) of size <= Ec(#(phi)).
Let phi be a formula in the signature of RCFI. The field interpretation of
phi is the result of replacing every atomic subformula s < t in phi by
(therexists x)(x not= 0 & t-s = x^2), where x is the first variable not
appearing in s,t.
LEMMA 6.3. There is a positive integer c such that the following is
provable in EFA. Let phi be an axiom of RCFI. The field interpretation of
phi has a special proof in RCF(fact) of size <= Ec(#(phi)).
THEOREM 6.4. (EFA) If RCF(fta) is specially consistent then RCFI is
specially consistent. There is a positive integer c such that the following
is provable in EFA. Let phi be an axiom of RCFI. The field interpretation
of phi has a special proof in RCF(fta) of size <= Ec(#(phi)).
7. SPECIAL CONSISTENCY OF REAL CLOSED FIELDS WITH INTERMEDIATE VALUE THEOREM
LEMMA 7.1. (EFA) Every axiom of RCF(fta) has a proof in RCF. There is a
positive integer c such that EFA proves the following. Let phi be an axiom
of RCF(fta). Then there is a proof in RCF of phi of size <= Ec(#(phi)).
LEMMA 7.2. (EFA) Every axiom of RCF(fta) has a special proof in RCF. There
is a positive integer c such that EFA proves the following. Let phi be an
axiom of RCF(fta). Then there is a special proof in RCF of phi of size <=
Ec(#(phi)).
LEMMA 7.3. (EFA) The field interpretation of every axiom of RCFI has a
special proof in RCF. There is a positive integer c such that EFA proves
the following. Let phi be an axiom of RCFI. Then there is a special proof
in RCF of the field interpretation of phi of size <= Ec(#(phi)).
THEOREM 7.4. (EFA) If RCF is specially consistent then RCFI is specially
consistent. There is a positive integer c such that the following is
provable in EFA. Let phi be an axiom of RCFI. The field interpretation of
phi has a special proof in RCF(fta) of size <= Ec(#(phi)).
THEOREM 7.5. (EFA) RCF is consistent and complete, and conservative over RF
for quantifier free formulas. Every existential formula provable in RCF has
a special proof in RCF. Also, there exists a positive integer c such that
EFA proves the preceding statements with upper bounds using the function
Ec.
THEROEM 7.6. (EFA) RCFI is consistent and complete, and conservative over
FLD(<) for quantifier free formulas. Every existential formula provable in
RCFI has a special proof in RCFI. Also, there exists a positive integer c
such that EFA proves the preceding statements with upper bounds using the
function Ec.
The axioms of RCF(lub) are as follows.
1. FLD(<).
2. If a formula with parameters holds of no positive elements, then there
is a least x >= 0 such that it holds of no elements greater than x.
We can carry out this development for RCF(lub) as well, just involving
proofs and not special proofs, since it is not an existential theory.
8. APPLICATION TO HILBERT¹S 17TH PROBLEM
We can use the results of this paper to prove in EFA that every polynomial
of several variables with rational coefficients, which is nonnegative at
all rational arguments, can be formally written as the sum of squares of
rational functions with rational coefficients. And there is a positive
integer c such that this statement is provable in EFA with the relevant
estimate using the function Ec.
9. INTERPRETATIONS OF RCF AND FINITELY AXIOMATIZED EXTENSIONS IN EFA
There is an interpretation of the signature of fields into the signature of
EFA such that EFA proves the interpretation of every theorem of RCF is a
theorem of EFA. This can be done with a relatively mild estimate. And there
is an interpretation of the signature of fields with a satisfaction
relation into the signature of EFA such that the interpretation of every
axiom of RCF with a satisfaction predicate (there are only finitely many)
is a theorem of EFA.
10. NEGATIVE RESULTS
The consistency of RCF cannot be proved in various weaker systems than EFA
that are commonly considered. Specifically, systems based on subexponential
functions such as n^log(n).
More information about the FOM
mailing list