[FOM] 247:Inevitability of Logical Strength

[Harvey Friedman]

THE INEVITABILITY OF LOGICAL STRENGTH
by
Harvey M. Friedman
Department of Mathematics
The Ohio State University
http://www.math.ohio-state.edu/%7Efriedman/
April 24, 2005

An extreme form of logic skeptic claims that "the present formal systems
used for the foundations of mathematics are artificially strong, thereby
causing headaches such as the Godel incompleteness phenomena". The skeptic
continues by claiming that "logician's systems always contain overly general
assertions, and/or assertions about overly general notions, that are not
used in any significant way in normal mathematics. For example, induction
for all statements, or even all statements of certain restricted forms, is
far too general - mathematicians only use induction for natural statements
that actually arise. If logicians would tailor their formal systems to
conform to the naturalness of normal mathematics, then various logical
difficulties would disappear, and the story of the foundations of
mathematics would look radically different than it does today". This talk
presents some specific results that sharply refute aspects of this
viewpoint. 

###1. EFA = ISigma0(exp) and logical strength.###

For our purposes, we say that a theory in many sorted free logic has logical
strength if and only if the system EFA = ISigma0(exp) is interpretable in
it. I will elaborate after EFA is presented.

We introduced EFA = exponential function arithmetic, in [Fr80]. It was also
used in the exposition of my work on Translatability and Relative
Consistency, in [Sm82].

Since then, this system has often been referred to as ISigma0(exp). See,
e.g., [HP98], p. 62. Also see [HP98], p. 405, second paragraph, referring to
our presentation. We will use the terminology EFA here.

First we present PFA = I(0. Here PFA stands for "polynomial function
arithmetic".

The language of PFA is based on 0,S,+,dot,<=,=. The variables are intended
to range over nonnegative integers.

The Sigma0 formulas are the formulas of PFA defined as follows.

i) every atomic formula of PFA is Sigma0;
ii) if phi,psi are Sigma0 then so are notphi, phi and psi, phi or psi, phi
implies psi, phi iff psi;
iii) if phi is Sigma0 and x is a variable not in the term t of PFA, then
(therexists x <= t)(phi) and (forall x <= t)(phi) are Sigma0.

In iii), the expressions are treated as abbreviations.

The nonlogical axioms of PFA are as follows.

1. The axioms of Q.
2. (phi[x/0] and (forall x)(phi implies phi([x/Sx])) implies phi, where phi
is Sigma0.

The nonlogical axioms of Q are

Q1. notSx = 0.
Q2. Sx = Sy implies x = y.
Q3. x not= 0 implies (therexists y)(x = Sy).
Q4. x + 0 = x.
Q5. x + Sy = S(x + y).
Q6. x dot 0 = 0.
Q7. x dot Sy = (x dot y) + x.
Q8. x <= y iff (therexists z)(z + x = y).

This presentation is slightly different than that given in [HP98]. There <=
is not taken as a primitive, but instead is defined by Q8. Also there the
terms t in bounded quantification are required to be variables.

We now present EFA. The language of EFA is 0,S,+,dot,*,<=,=. The new symbol
* is a binary function symbol standing for exponentiation.

The Sigma0(exp) formulas are the formulas of EFA defined as follows.

i) every atomic formula of ISigma0 is Sigma0(exp);

ii) if phi,psi are ISigma0(exp) then so are notphi, phi and psi, phi or psi,
phi implies psi, phi iff psi;

iii) if phi is Sigma0(exp) and x is an variable not in the term t of EFA,
then (therexists x <= t)(phi) and (forall x <= t)(phi) are Sigma0(exp).

The nonlogical axioms of EFA are as follows.

1. The axioms of Q.
2. x * 0 = S0, x * y+S0 = x*y dot x.

3. (phi[x/0] and (forall x)(phi implies phi[x/Sx])) implies phi, where phi
is Sigma0(exp).

There is a closely related system PFA + EXP whose language is the same as
PFA (i.e., no *). The sentence EXP is horribly ugly. EXP really refers to a
family of sentences, all of which are provably equivalent over PFA.

EXP is based on the following.

THEOREM 1.1. There is a Sigma0 formula Exp(x,y,z) with only the distinct
free variables shown such that the following is provable in PFA.

i) Exp(x,0,z) iff z = 1;

ii) Exp(x,Sy,z) iff (therexists v)(Exp(x,y,v) and z = v dot x).

Proof: See [HP98], p. 299. QED

EXP is taken to be 

(forall x,y)(therexists z)(Exp(x,y,z))

where Exp is any formula satisfying the conditions of Theorem 1.1.

The following two Theorems are well known.

THEOREM 1.2. If Exp(x,y,z) and Exp'(x,y,z) satisfy conditions in Theorem
1.1, then PFA proves their equivalence. PFA proves the equivalence of any
version of EXP.

There is a particularly convenient and natural equivalent of EXP which we
call CM = common multiples.

CM. For all n >= 1, the integers 1,2,...,n have a positive common multiple.

The following is well known.

THEOREM 1.3. PFA proves the equivalence of any version of EXP with CM.

For this reason, we will always use PFA + CM instead of PFA + EXP. The
following is well known.

THEOREM 1.3. EFA and PFA + CM prove the same sentences in the language of
PFA. PFA + CM, and EFA are finitely axiomatizable. EFA is interpretable in
PFA + CM. 

It is not known whether PFA is finitely axiomatizable. This question is
related to notorious issues in complexity theory surrounding P = NP.

EFA is the minimum system of arithmetic where standard coding mechanisms in
arithmetic can be done naturally without worry. In particular, standard
identifications between finite sequences of natural numbers and natural
numbers are fully available.

It appears that EFA is very strong from some points of view. We conjectured
that EFA was sufficient to prove any normal theorem of number theory that is
adequately formalizable in its language. We can be liberal about
"formalizable" here, using the various natural codings available in EFA.

For example, Fermat's Last Theorem ought to be provable in EFA. This has
never been established.

This conjecture captured the imagination of Jeremy Avigad who wrote
extensively about it in [Av03].

Our official definition of logical strength is as follows. T has logical
strength if and only if EFA is interpretable in T.

There are two stronger notions that are particularly convenient.

a. EFA is a subsystem of T. I.e., all axioms of EFA are provable in T.
b. PFA + CM is a subsystem of T. I.e., all axioms of PFA + CM are provable
in T.

Obviously a) is appropriate if the language of T includes that of EFA, and
b) is appropriate if the language of T includes that of PFA. Clearly a)
implies b), but clearly criterion a) is worth stating.

Two minor difficulties arise when using these two criteria.

i. Our strictly mathematical systems do have 0,1,+,dot,<=,=, and sometimes
*, but not S.

ii. Our strictly mathematical systems have a sort for Z, and not for N.
Consequently (forall x)(x >= 0) will be refutable in our strictly
mathematical systems, whereas (forall x)(x >= 0) is provable in PFA.

The most convenient way to get around these difficulties is to modify
criteria a,b as follows.

a'. The universal closure of every axiom of EFA, when quantifiers (forall
x),(therexists y) are replaced by (forall x >= 0),(therexists y >= 0), and
all maximal terms SS...S(t) are replaced by 1+1+...+1+t, associated to the
right, is a theorem of T.

b'. The universal closure of every axiom of PFA + CM, when quantifiers
(forall x),(therexists y) are replaced by (forall x >= 0),(therexists y >=
0), and all maximal terms SS...S(t) are replaced by 1+1+...+1+t, associated
to the right, is a theorem of T.

Obviously a') implies b') implies T has logical strength.

In the next section, we will present strictly mathematical systems meeting
both of these criteria.

###2. Some strictly mathematical statements.###

We now present the strictly mathematical statements that we use to interpret
EFA, and in fact meet criteria a'),b'). All of these statements are used
and/or taught by all mathematicians.

The language in which we make almost all of these strictly mathematical
statements is two sorted. We have a sort Z for integers, and a sort Z* for
finite sequences of integers.

We use 0,1,+,-,dot,<= on Z, where - is unary. We use equality only for Z. We
use lth(x) for the length of the sequence x, which is of sort Z. Here x must
be of sort Z*. We use val(x,n) for the n-th term of the sequence x, which is
of sort Z. Here x must be of soft Z* and n must be of sort Z. Lengths of
sequences are nonnegative, and the terms of sequences are indexed starting
with 1. 

Note that we use equality only for Z and not for Z*. It is convenient to
define equality for Z* as "having the same values in the same positions".
Obviously any two equal sequences must have the same length.

We now give the axioms for FSZ informally. FSZ stands for "finite sequences
of integers". 

1. Discrete linearly ordered ring axioms for Z.
2. lth(x) >= 0.

3. val(x,n) is defined if and only if 1 <= n <= lth(x).

4. The finite sequence (0,...,n) exists.

5. lth(x) = lth(y) implies -x, x+y, x dot y exist.

6. The concatenation of x,y exists.

7. For n >= 1, the concatenation of x, n times, exists.

8. There is a finite sequence enumerating the terms of x that are not terms
of y, in strictly increasing order.

We make some remarks about 1-8.

a. The underlying logic is a well known variant of many sorted predicate
calculus with equality, known as free logic. It has a corresponding complete
axiomatization.

b. Axiom 4 is presented in terms of the length and values of (0,...,n).
I.e., lth(x) = n+1 and val(x,i) = i-1 for 1 ( i ( n+1.

c. Axiom 5 is also presented in terms of the length and values of the finite
sequences -x,x+y,x dot y.

d. Axiom 6 is presented in terms of the length and values of the
concatentation of x,y. This uses addition and subtraction on indices.

e. Axiom 7 is again presented in terms of the length and values of the n
fold concatentation so described. What amounts to modular arithmetic is used
for this presentation. Of course, the axioms of FSZ do not directly address
modular arithmetic.

f. An alternative is to divide axiom 8 into two parts. First that there is a
finite sequence whose terms consist of the terms of x that are not terms of
y. Second that there is a strictly increasing sequence whose terms are the
same as any given z. It is obvious that axiom 8 follows logically from the
conjunction of these two parts. The first part immediately follows from
axiom 8. For the second part, first deduce from axiom 8 that there is an
empty sequence. Then apply axiom 8 to x and the empty sequence.

g. Our results hold for the following weaker system. Replace 8 by the
following two immediate consequences of 8.

8a. There is a finite sequence whose terms are exactly those of x that are
not terms of y. 
8b. Every nonempty finite sequence has a least term.

FSZE is FSZ together with CM, as presented in section 1.

THEOREM 2.1. FSZ + CM meets criteria b').

The language of FSZEXP is L(FSZ) together with the binary operation symbol *
on Z. FSZEXP extends FSZ by

11. m >= 0 implies (n * 0 = 1 and n * m+1 = n dot (n * m)).

12. m < 0 implies (n * m) undefined.

13. (n*1,n*2,...,n*m) exists.

THEOREM 2.2. FSZEXP meets criteria a').

We had an earlier version of mathematical statements that combine to form a
system of logical strength. However, it was considerably less convincing,
and used finite sets of integers instead of finite sequences of integers as
we do here. See [Fr01].

3. FSZ and T0.

T0 of [Fr01] is in the two sorted language with variables over integers and
variables over finite sets of integers. For the integer sort, we use the
language 0,1,+,-,dot,<,= of linearly ordered rings, as we do for FSZ. We use
( between integers and sets. Equality is used only between integers. The
nonlogical axioms of T0 are as follows.

1. Linearly ordered ring axioms.
2. Finite interval. (therexists A)(forall x)(x in A iff (y < x and x < z)).
3. Boolean difference. (therexists C)(forall x)(x in C iff (x in A and not x
in B))).
4. Set addition. (therexists C)(forall x)(x in C iff (therexists
y)(therexists z)(y in A and z in B and x = y+z)).
5. Set multiplication. (therexists C)(forall x)(x in C iff (therexists
y)(therexists z)(y in A and z in B and x = y dot z)).
6. Least element. (therexists x)(x in A) implies (therexists x)(x in A and
(not therexists y)(y in A and y < x)).

THEOREM 3.1. The universal closure of every axiom of PFA, when quantifiers
(forall x),(therexists y) are replaced by (forall x >= 0),(therexists y >=
0), and all terms S(t) are replaced by 1+1+...+1+t, associated to the right,
is a theorem of T0.

Proof: See [Fr01]. QED

Since PFA is not known to be finitely axiomatizable, we cannot witness
Theorem 3.1 by a finite amount of data. So we remark that Theorem 3.1 is
very effectively true. In fact, there is a polynomial time algorithm which,
provably in EFA, converts any axiom of PFA to a proof in T0 of the
replacement of that axiom given in the statement of Theorem 3.1.

We can prove that Theorem 3.1 holds for FSZ. For this, we give an
interpretation of T0 in FSZ which is the identity on the Z sort.

This interpretation of T0 in FSZ is the obvious one. The interpretation of
the integer part is the identity. The interpretation of the sets of integers
in T0 are the sequences of integers in FSZ. The epsilon relation is
interpreted as 

n epsilon x if and only if n is a term of x.

THEOREM 3.1. FSZ + CM meets criterion b'.

###4. Further developments.###

The plan is to generate much greater logical strength from strictly
mathematical statements. This project is of course greatly facilitated now
that we have the essential and fundamental infrastructure of EFA or PFA + CM
at hand. 

Initial developments along the lines of greater logical strength are
discussed in [Fr05].

REFERENCES

[Av03] J. Avigad, Number theory and elementary arithmetic
Philosophia Mathematica 11:257-284, 2003.
http://www.andrew.cmu.edu/user/avigad/

[Fr80] H. Friedman, A Strong Conservative Extension of Peano Arithmetic,
Proceedings  of the 1978 Kleene Symposium, North Holland, (1980), pp.
113-122. 

[Fr01] H. Friedman, Finite reverse mathematics, October 19, 2001, 28 pages,
draft. 

http://www.math.ohio-state.edu/%7Efriedman/

[Fr05] H. Friedman, Strict reverse mathematics, January 31, 2005, 24 pages,
draft.

http://www.math.ohio-state.edu/%7Efriedman/

[HP98] P. Hajek, P. Pudlak, Metamathematics of First-Order Arithmetic,
Perspectives in Mathematical logic, Springer, 1998. ISBN 0-387-50632-2, ISBN
3-540-50632-2.

[Si99] S. Simpson, Subsystems of Second Order Arithmetic, Springer Verlag,
1999.

[Sm82] C. Smorynski, Nonstandard models and related developments. In: Harvey
Friedman's Research on the Foundations of Mathematics, North Holland:
Amsterdam, 1985, pp. 179-229.


*************************************

I use www.math.ohio-state.edu/~friedman/ for downloadable manuscripts.
This is the 247th 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-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms 4/22/03  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM
194:PL Statement/clarification  11/2/03  8:10PM
195:The axiom of choice  11/3/03  1:11PM
196:Quantifier complexity in set theory  11/6/03  3:18AM
197:PL and primes 11/12/03  7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM
203:Proof(?) of Church's Thesis - Restatement 1/13/04 12:23AM
204:Finite Extrapolation 1/18/04 8:18AM
205:First Order Extremal Clauses 1/18/04 2:25PM
206:On foundations of special relativistic kinematics 1 1/21/04 5:50PM
207:On foundations of special relativistic kinematics 2  1/26/04  12:18AM
208:On foundations of special relativistic kinematics 3  1/26/04  12:19AAM
209:Faithful Representation in Set Theory with Atoms 1/31/04 7:18AM
210:Coding in Reverse Mathematics 1  2/2/04  12:47AM
211:Coding in Reverse Mathematics 2  2/4/04  10:52AM
212:On foundations of special relativistic kinematics 4  2/7/04  6:28PM
213:On foundations of special relativistic kinematics 5  2/8/04  9:33PM
214:On foundations of special relativistic kinematics 6  2/14/04 9:43AM
215:Special Relativity Corrections  2/24/04 8:13PM
216:New Pi01 statements  6/6/04  6:33PM
217:New new Pi01 statements  6/13/04  9:59PM
218:Unexpected Pi01 statements  6/13/04  9:40PM
219:Typos in Unexpected Pi01 statements  6/15/04  1:38AM
220:Brand New Corrected Pi01 Statements  9/18/04  4:32AM
221:Pi01 Statements/getting it right  10/7/04  5:56PM
222:Statements/getting it right again  10/9/04  1:32AM
223:Better Pi01 Independence  11/2/04  11:15AM
224:Prettier Pi01 Independence  11/7/04  8:11PM
225:Better Pi01 Independence  11/9/04  10:47AM
226:Nicer Pi01 Independence  11/10/04  10:43AM
227:Progress in Pi01 Independence  11/11/04  11:22PM
228:Further Progress in Pi01 Independence  11/12/04  2:49AM
229:More Progress in Pi01 Independence  11/13/04  10:41PM
230:Piecewise Linear Pi01 Independence  11/14/04  9:38PM
231:More Piecewise Linear Pi01 Independence  11/15/04  11:18PM
232:More Piecewise Linear Pi01 Independence/correction  11/16/04  8:57AM
233:Neatening Piecewise Linear Pi01 Independence  11/17/04  12:22AM
234:Affine Pi01 Independence  11/20/04  9:54PM
235:Neatening Affine Pi01 Independence  11/28/04  6:08PM
236:Pi01 Independence/Huge Cardinals  12/2/04  3:49PM
237:More Neatening Pi01 Affine Independence  12/6/04  12:56AM
238:Pi01 Independence/Large Large Cardinals/Correction  12/7/04  10:31PM
239:Pi01 Update  12/11/04  1:12PM
240:2nd Pi01 Update  12/13/04  2:49AM
241:3rd Pi01 Update  12/13/04  4:08AM
242:4th Pi01 Update  12/18/04  9:47PM
243:Inexplicit Pi01/Ordinals of Set Theories  12/19/04  11:48PM
244:LUB Systems  2/26/05  8PM
245:Relational System Theory 1
246:Relational System Theory 2

Harvey Friedman