[FOM] Finite to Infinite: an alternative approach

[Arnon Avron]

In one of his postings on  February 22 Harvey Friedman 
attributed to me "a rejection of the very idea that set theory 
is based on a transfer from finite set theory, right from the start".
Again I simply cannot understand from where did he
take this interpretation of my words. In this case
nothing can be far from the truth. Not only
I don't reject the idea, but already 8 years ago I have described 
on FOM my first attempt at working out the same idea (see 
http://www.cs.nyu.edu/pipermail/fom/1998-January/000955.html). 
Since then I had made some progress, some of which has been published
(details can be found in my homepage, in case somebody is interested). 
My current suggestions are described in two 
prepapers (NOT papers yet) which are available from my homepage:
"A Framework for Formalizing Set Theories" and "A New Approach to
Predicative Set Theory". I believe that unlike Friedman, I am
suggesting and using a natural, well-motivated criterion
for transferring to the infinite comprehension schemes which are
valid for the finite. Below I am providing a short outline.
I leave to the readers of FOM the judgment which approach is more 
natural and convincing: mine, or that described 
by Friedman in his posting from February 22 on "Finite to Infinite".

According to my approach, a predicativist need
*not* exclude the possibility that "arbitrary (undefinable) sets of
integers", or "real numbers", or even "arbitrary sets of reals",
do exist as objects in some sense,  and that propositions about 
them might be meaningful.  However, being a limited human
being, he cannot feel *certain* about the existence and identity of of such 
entities.  Accordingly,  a predicativist (at least of the type I am
speaking about here)  may formulate and use in set theory propositions
that refer to all sets. However,
only those of them which can be proved as true independently of 
the exact extension of "the true universe V of sets" may be 
accepted as *absolute* (certain)  theorems. In particular, the only
instances of the comprehension schema that *certainly* make sense
for him and are safe to use are those that are "universe independent"
(For the purpose of this posting this notion should be understood
intuitively. Platonists may understand it as "having the same
extension in all transitive models of ZF"). I believe that deeply, this is 
what Poincare has in mind when he introduced the concept "predicative" 
(but I am not an historian, and I would not be able to defend this 
belief if attacked by people who, unlike me, are real experts).

 So now come the criterion I suggest for transferring to the 
infinite comprehension principles which are valid for finite sets:
accept those principles that define a set in a "universe independent" way.

  Now it should be apparent that "universe independent" and "absoluteness"
(in the known technical sense used in texts on Set theories) are very 
close relatives. However, what is not less important is that 
a closely related notion, domain-independence (d.i.), is of a crucial 
importance in relational database theory - a theory which almost exclusively 
deals with finite universes and relations. 

In relational databases, a query is d.i. if the answer to it depends only
on the information included in the database, and on the objects which are mentioned
either in the query or in the database. The answer to such query
should not depend on the exact extension of the full intended domain,
which might include other objects as well (a "query" is just
a formula in the corresponding language, and the answer to a query is either
"yes" or "no" in case the query is a sentence, and the list of tuples
which satisfy the query in case it has free variables).
Practical database query languages (like SQL)
are designed so that *only domain-independent queries can be formulated
in them*, and each such query
language is based on some syntactic criteria that ensure this property.

Now both "absoluteness" (in set theory) and d.i. (in database theory)
are properties of formulas (which are obviously related, but not identical).
Predicativity of a formula, in contrast, is a relation between a formula
and one of its free variables. A common generalization of all is
a semantic  safety relation between a formula and subsets of its set free variables.
The intuitive idea is that A(x_1,...,x_n,y_1,...,y_k) is safe with respect
to {x_1,...,x_n} if for every a_1,...,a_k, the collection 
{(x_1,...,x_n)|  A(x_1,...,x_n,a_1,...,a_k)} is the same in
all acceptable domains/universes that includes a_1,...,a_k.
As particular cases we have that a formula A is d.i. if it is safe
w.r.t its set of free variables, absolute if it is safe w.r.t
the empty set (of variables), and predicative w.r.t a variable x
if it is safe w.r.t. {x}.

 The transfer from the principles used in finite database theory to 
infinite set theory (based on the binary relations = and epsilon) 
naturally  leads (see my papers for an explnation) to the following theory RST:

Formulas
=========

1) If t and s are safe terms than t=s and t\in s are atomic formulas
2) If A and B are formulas then so are any complex formulas obtained
   from them using the standard classical connectives and quantifiers.

Safe terms
==========

1) Every variable is a safe term.
2) If x is a variable, and A is a formula which is safe w.r.t x
   then {x|A} is a safe term.

The safety relation
===================

1) Every atomic formula is safe w.r.t. the empty set (of variables)
2) If A is safe w.r.t. the emptyi set then so is its negation.
3) If x is a variable, and t is a safe term in which x does not
   occur free, then x=t, t=x, x\in t and the negation of x=x are
   all safe w.r.t. x.
4) If A and B are both safe w.r.t. X then so is their disjunction
5) If A is safe w.r.t. X, B safe w.r.t. Y, and no element of Y
   is free in A, then the conjunction of A and B is safe w.r.t.
   the union of X and Y.
6) If A is safe w.r.t. X, and y belongs to X, then \exists y.A
   is safe w.r.t. X-{y}.

Axioms
======

1) Extensionality
2) Comprehension: x\in{x|A} iff A (here {x|A} should of course be 
   a safe term, i.e.: A should be safe w.r.t. {x}).

Theorem 1. the collection of hereditarily finite sets is the minimal
           model of RST.
Theorem 2. If A is safe w.r.t its set of free variables than A is d.i.
           in the sense of database theory (Note: it is easy to see
           that intuitively, if A is safe w.r.t. X according to
           the official syntactic definition, then 
           A is also safe w.r.t. X according to the intuitive semantic
           meaning describe above. The converse fails).

Theorem 3. A function F on sets is explicitly definable by some safe
           term of RST iff it is rudimentary in the sense of Jensen
           (if t is a term whose free variables are y_1,...,y_k
           then t defines the function on set \lambda y_1,...,y_k.t)
           A relation is rudimentary iff it is definable by some
           formula of RST which is safe w.r.t. the empty set.

It follows that the union of an arbitrary set is definable in RST
(as well as the cartesian product of any two sets and many other
basic operations on sets). On the other hand the powerset operation 
is *not* available in RST. In order to get it one should explicitly
add to the definition of the safety relation the condition
that x\subset y is safe w.r.t to x - but such an addition has no justification,
since x\subset y is not universe-independent.

This message is already too long. So I'll stop here.
 
Arnon Avron