[FOM] 277:Strict Predicativity

[Harvey Friedman]

We give a straightforward analysis of one of many flavors of what is
generally called "predicativity". The one we present is called

strict predicativity

in order to distinguish it from other flavors of "predicativity".

Our proposed analysis of "strict predicativity" is substantially weaker than
the Feferman/Schutte analysis of "predicativity".

However, strict predicativity is sufficiently liberal so as to allow all of
the obviously natural mathematics that I am aware of for which
mathematicians do not easily sense that something logically exotic is going
on connected with, broadly speaking, "predicativity".

Strict predicativity seems to have the advantage of perhaps lending itself
particularly well to formal analysis.

The issue centers around the construction

{n: phi(n)}

where phi may have variables over nonnegative integers in addition to n, and
also phi may have variables over sets of nonnegative integers.

Below, by set we will always mean: set of nonnegative integers.

Now prima facie, phi(n) does not have a definite meaning, as the range of
the set (of natural number) quantifiers in phi(n) are not fixed. They are
not fixed, because the sets do not form a completed totality.

So we will accept 

{n: phi(n)} exists

if we can PROVE that it doesn't make any difference what completed totality
the set variables in phi range over, as long as that completed totality
approximates what we already know about the incompleted totality of all
sets.  

Formally, in order to get things going in a completely nonproblematic way,
let us start off with the system ACA_0. (This is not really necessary, but
fine for this first posting).

To this, we add the following rule of proof:

COMPREHENSION RULE. Let phi, psi be formulas of the language of second order
arithmetic, and n be a variable over the nonnegative integers. Suppose we
have proved psi. Also suppose that we have proved that for all enumerated
families A,B of sets of nonnegative integers that include the set parameters
of phi, if psi holds in A,B, then phi holds in A iff phi holds in B. Then we
can conclude that {n: phi} exists.

Because we have started with ACA_0, there is no problem making sense of the
above talk of "sufficiently inclusive enumerated families" appropriately as
a single set of nonnegative integers.

We also add the following rule of proof:

INDUCTION RULE. Let phi be a formula of the language of second order
arithmetic, and n be a variable over the nonnegative integers. Suppose we
can prove the formulas phi[n/0], and phi implies phi[n/n+1]. Then we can
conclude phi. 

There are variants of the Comprehension Rule that don't feature enumerated
families. We expect to take this up in the future.

Now, what can we say about the above formal system, SP = strict
predicativity? 

It appears that SP is measured by omega^omega Turing jumps. This is of
course far less than Gamma_0 Turing jumps. But I don't know of any Theorem
in nature that is strictly in between.

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 277th 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

Harvey Friedman