FOM: 8:Schemes

[Harvey Friedman]

This is the eighth in a series of positive 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:22AM

Let me remind you that a complete archiving of fom, message by message, is
available at http://www.math.psu.edu/simpson/fom/index.html

I made a conjecture in 4:Simplicity   about Peano Arithmetic (PA) which
asserts that it is complete for schemes (and formulas) of low complexity in
4:Simplicity. There are some awkward things about it, and despite my first
impressions, some currently intractable Diophantine theory is involved. I
think this sort of thing can be made to go through in a reasonable way. But
in this posting, I want to take a different approach.

We can view this as an attempt to answer the question: what is a logical
principle? Rather than directly attack this head on, the program is to
uncover general construction principles for forming the formal systems we
normally work with in f.o.m. in terms of familiar semantic concepts and/or
simplicity (complexity) measures, up to provable equivalence, or at least
up to bi-interpretability or synonymy. We again emphasize the healthy
experimental nature of f.o.m.

The general setup we choose to discuss here is as follows. We start with a
familiar relational structure in a finite relational type, M, with domain
D, with a familiar set S of mathematical axioms commonly associated with
it. We also distinguish a subset C of the constants, relations, and
functions used in M. We then add variables over subsets of D, and consider
all formulas with variables over M, signs from C, quantification over D,
variables over subsets of D, but with no quantification over subsets of D.
This is the so called universal monadic language (restricted to C). It is
important for this particular approach that the set T of all universally
true formulas of this form be known to be decidable. We then form what we
call the first order approximation of M relative to S,C. This is the result
of interpreting the formulas in T as schemes, where the free variables over
subsets of D are replaced by formulas in the full language of M.

More precisely, a variable x is designated not appearing in the scheme, and
each set variable E is assigned a formula in the full language of M, all of
whose  variables other than x do not appear in the scheme. Then each s in E
is replaced by A[x/s], where A is the formula so assigned to the set
variable E. (Here s is a term).

Let us see what happens when we start with the axioms for discrete ordered
commutative ring with unit, DOCRU, and the special DOCRU Z. The language of
DOCRU's is <,=,0,1,+,-. It is well known that the universal monadic theory
over Z,< is decidable. We then form the first order approximation of the
DOCRU Z relative to the DOCRU axioms and <. This is a recursive object.

THEOREM 1. PA, adapted to <,=,0,1,+,-, is logically equivalent to the first
order approximation of the DOCRU Z relative to the DOCRU axioms and <.

We now consider the ordered field of reals with the integers Z as a
distinguished predicate. The language for this will be <,=,0,1,+,-,x,Z,
where Z is a unary predicate. The mathematical axioms for this structure
will be that of ordered field with integers - OFI - which uses the axioms
that Z is a subring with nothing between 0 and 1. We know that the
universal monadic theory of the reals R with < is decidable. So we can
reasonably form the corresponding first order approximation.

Recall the well known first order theory called second order arithmetic,
Z2, an icon of f.o.m. It has variables over natural numbers, variables over
sets of natural numbers, induction with respect to all formulas, and
comprehension with respect to all formulas.

THOEREM 2. The first order approximation of the OFI (R,<,=,0,1,-,x,Z)
relative to the OFI axioms and < is synonymous with Z2.

Now for an additional aspect of the discussion. Many fragments of PA have
been studied in f.o.m. The most well known are simply obtained by
restricting the induction scheme to induction with respect to formulas of
restricted complexity - i.e., sigma-n, n >= 1. There are other important
systems, including wekaer ones such as primitive recursive arithemetic,
exponential function arithmetic, and even lower. Can these be recovered in
terms of first order approximations?

Specifically, consider the first order approximation T* of the DOCRU Z
relative to the DOCRU axioms and <. What are the finite fragments of T* on
top of the DOCRU axioms? Are these logically equivalent to standard
fragments of PA? Could they be linearly (or well) ordered under logical
strength? Is the logical implication relation or the interpretability
relation decidable among such fragments (always on top of the DOCRU
axioms)? Can we get the most commonly studied fragments of PA in f.o.m. in
this way?

The same questions can be asked of the finite fragments of the first order
approximation of the OFI (R,<,=,0,1,-,x,Z) relative to the OFI axioms and
<.

The plan is to see if the usual axioms for set theory, including large
cardinals, can be recovered according to first order approximations. Also,
maybe all of their natural fragments can be recovered too!! If things go
very well, then we can make a bold thesis that "a logical principle is a
scheme that is an element of some first order approximation," and get lots
of structure on the space of such logical principles. It's bold, and
perhaps you don't give it much chance, but, hey.....

NOTE: If all goes well, this is an illustration that in f.o.m., for every
good idea there is a better one. And this can be iterated. Also, try a lot
of bold things, and expect to fail and enjoy it. But once in a while ...