[FOM] 278:Ultra/Strict/Predicativity/Higman

Sat Apr 8 01:33:04 EDT 2006

First, a correction.

In connection with Higman's theorem, I wrote
http://www.cs.nyu.edu/pipermail/fom/2006-April/010337.html :

"People often forget that Graham Higman proved what really amounts to
labeled Kruskal's Theorem (bounded valence) EARLIER than Kruskal!

G. Higman, Ordering by divisibility in abstract algebras, Proc. London Math.
Soc. (3), 2:326--336, 1952.

Since this Higman Theorem corresponds to LKT (bounded valence), we know that
it cannot be predicatively proved under any proposed interpretation of
predicativity."

CORRECTION: 

People often forget that Graham Higman proved what really amounts to
Kruskal's Theorem (bounded valence) EARLIER than Kruskal!

G. Higman, Ordering by divisibility in abstract algebras, Proc. London Math.
Soc. (3), 2:326--336, 1952.

Higman also proves a stronger version there, that corresponds to LKT
(bounded valence), which we know cannot be predicatively proved under any
proposed interpretation of predicativity.

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

Here I want to proceed at a more fundamental level concerning predicativity
than I did in 277, 
http://www.cs.nyu.edu/pipermail/fom/2006-April/010343.html

All systems are in the usual language of second order arithmetic.

1. ULTRA PREDICATIVITY.

Here we start with the idea that quantification over all sets of nonnegative
integers is to be absolutely rejected as meaningless. However, assertions
can be made with free variables over sets of nonnegative integers.

Well orderings, transfinite induction, and transfinite recursion have no
special status of any kind, and are to be dealt with only according to prior
principles. 

We are allowed to use the only legitimate form of comprehension available,
which is {n: A}, where A has no set quantifiers. However, A may have both
integer and set variables.

We avoid the existential set quantifier normally used here, but considering
{n: A} to be a denoting term, provided A has no set quantifiers.

Induction is in the form

(A[x/0] and (forall x)(A implies A[x/x+1]) implies A

where A has no set quantifiers.

Of course, the usual successor axioms are used.

This system, is of course, just ACA_0.

ACA_0 is sufficient to develop Weyl's analysis, pretty much as Weyl
presented it. 

However, note that nothing short of ACA_0 is sufficient to develop Weyl's
analysis. This can be proved to be the case in various satisfactory ways.

This is because of principles like: every bounded sequence of reals has a
limit point, and every Cauchy sequence (no rate of convergence) converges,
etcetera. 

However, if one is careful to do real analysis in a more explicit
(classical) way, one can do a lot in RCA_0 or RCA_0 + WKL.

Pragmatically, the vast preponderance of mathematics that is not
appropriately formalizable in ACA_0, isn't formalizable in much much
stronger systems. So ACA_0 is a good line of demarcation, serving as a
practical guide to predicativity in a way that avoids having to get into
controversial issues of various unattractive kinds.

However, there is some substantial mathematics that form exceptions, that
lie just outside ACA_0.

In particular, RT = the usual infinite Ramsey theorem, for all k-tuples. For
any fixed k, RT for k-tuples is provable in ACA_0. However, not so for RT.

The proof of RT is so simple and transparent, particularly as a "limit" of
the proofs of the RT(k), that there is a compelling reason to explore
notions of predicativity that go further.

2. STRICT PREDICATIVITY.

In strict predicativity, one still adheres to the fundamental idea that
quantification over all sets of nonnegative integers is to be absolutely
rejected as meaningless. However, assertions can be made with free variables
over sets of nonnegative integers. Also terms are used instead of
existential assertions.

Just as in ultra predicativity, well orderings, transfinite induction, and
transfinite recursion have no special status of any kind, and are to be
dealt with only according to prior principles.

The following formalization for strict predicativity has substantial
analogies with a common formalization of finitism - PRA = primitive
recursive arithmetic.

A common way of motivating PRA is to step back and first discuss the
primitive recursive functions as a mathematical construction, and not as a
formal system. 

Similarly, we introduce what we call

the primitively hyperarithmetical operations

as a mathematical construction.

a. Initial functions. Introduce F(m1,...,mp,x1,...,xq) = {n:
phi(n,m1,...,mp,x1,...,xq)}, where phi has no set quantifiers and the free
variables of phi are among n,m1,...,mp,x1,...,xq.

b. Composition. Introduce F(m1,...,mp,x1,...,xq) =
G(H1(m1,...,mp,x1,...,xq),...,Hr(m1,...,mp,x1,...,xq)).

c. Primitive Recursion. F(0,m1,...,mp,x1,...,xq) = G(m1,...,mp,x1,...,xq),
F(n+1,m1,...,mp,x1,...,xq) =
H(n,m1,...,mp,x1,...,xq,F(n,m1,...,mp,x1,...,xq)).

THEOREM 2.1. The primitively hyperarithmetical operations are given as
follows. F(m1,...,mp,x1,...,xq) = the f(m1,...,mp)-th set r.e. in
J(alpha,<x1,...,xq>), where f is a recursive function, alpha is an ordinal <
omega^omega, and J(alpha,<x1,...,xq>) is the alpha-th Turing jump of
<x1,...,xq>. 

We can make clauses a,b,c into a formal system in the same way that the
standard clauses for primitive recursion turn into the formal system PRA =
primitive recursive arithmetic.

We have the usual successor axioms, the above equations, and induction for
all quantifier free formulas.

THEROEM 2.2. This system is logically equivalent to ACA_0 plus "for all x,
the alpha-th Turing jump of x exists", for every specific alpha <
omega^omega.

This system is easily enough to prove RT = infinite Ramsey Theorem.

3. SOMEWHAT FURTHER.

We can study various natural extensions of the above, that correspond to
various schemes and associated systems of arithmetic. It appears that, e.g.,
omega^(omega^omega) Turing jumps (from multirecursion), and epsilon_0 Turing
jumps (from nested recursion) come up right away.

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 278th 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM
255. Controlling Pi01  11/12  5:10PM
256. NAME:finite inclusion theory  11/21/05  2:34AM
257. FIT/more  11/22/05  5:34AM
258. Pi01/Simplification/Restatement  11/27/05  2:12AM
259. Pi01 pointer  11/30/05  10:36AM
260. Pi01/simplification  12/3/05  3:11PM
261. Pi01/nicer  12/5/05  2:26AM
262. Correction/Restatement  12/9/05  10:13AM
263. Pi01/digraphs 1  1/13/06  1:11AM
264. Pi01/digraphs 2  1/27/06  11:34AM
265. Pi01/digraphs 2/more  1/28/06  2:46PM
266. Pi01/digraphs/unifying 2/4/06  5:27AM
267. Pi01/digraphs/progress  2/8/06  2:44AM
268. Finite to Infinite 1  2/22/06  9:01AM
269. Pi01,Pi00/digraphs  2/25/06  3:09AM
270. Finite to Infinite/Restatement  2/25/06  8:25PM
271. Clarification of Smith Article  3/22/06  5:58PM
272. Sigma01/optimal  3/24/06  1:45PM
273: Sigma01/optimal/size  3/28/06  12:57PM
274: Subcubic Graph Numbers  4/1/06  11:23AM
275: Kruskal Theorem/Impredicativity  4/2/06  12:16PM
276: Higman/Kruskal/impredicativity  4/4/06  6:31AM
277: Strict Predicativity  4/5/06  1:58PM

Harvey Friedman