[FOM] 270: Finite to Infinite/restatement

[Harvey Friedman]

In the previous 
http://www.cs.nyu.edu/pipermail/fom/2006-February/009997.html

for some reason, I just didn't notice that quantifier free comprehension
does in fact prove extensionality. This is obviously a significant
improvement (although very easy).

Thus from the quantifier free comprehension scheme in epsilon,inclusion,=
with one unary schematic letter, studied there, we derive all of Z (not ZC)
except union and infinity.

It follows that QFCS + infinity is equiconsistent and mutually interpretable
with Z.  

FINITE TO INFINITE 1
by
Harvey M. Friedman
February 25, 2006

One credible view of set theory is that it is an extrapolation from finite
set theory to infinite set theory. In fact, this view is probably what is
behind the adherence of ZFC as the underlying Gold Standard for valid
mathematics by the mathematics community for about 80 years with very little
controversy. 

Obviously it is not true that any sentence in finite set theory can be
transferred to infinite set theory. So a major challenge is to uncover
natural criteria for transferring statements from finite set theory to
infinite set theory.

In this abstract, we discuss such criteria for transfer that supports the
level of Zermelo set theory. The key statements being transferred are

*the quantifier free comprehension schemes*

in the language epsilon,=,inclusion. The same results hold if we instead use
any of the languages

epilson,=,pairwise union.
epsilon,=,pairwise intersection.
epsilon,=,set difference.
epsilon,=,pairwise union, pairwise intersection, set difference, inclusion.

>From now on, we will refer to "infinite set theory" as simply "set theory".

Earlier work of ours on transfer principles appears on my website, and
assumes a substantial set theoretic infrastructure from the start. It also
involves the transfer of certain second order properties from V(omega) to V.
This is a more basic investigation.

1. FINITE SET THEORY.

The standard model of finite set theory is the class HF of all hereditarily
finite sets. This is the same as V(omega), as in the cumulative hierarchy of
sets. 

The most common formalization of finite set theory consists of the usual
axioms of ZFC stated in the usual way, with the axiom of infinity deleted
and replaced by its negation. Let us write this system as ZFC\INF +
not(INF).

There is a very powerful unifying reaxiomatization that shows how one can
actually derive all of ZFC\INF + not(INF) from the most fundamental
inductive description of HF = V(omega).

Specifically, V(omega) is the least class containing the emptyset, and
closed under the operation of adjunction: x,y go to x union {y}.

Let the language of FST be epsilon,=, with axioms

i. Extensionality.
ii. Emptyset. 
iii. Adjunction. (therexists z)(forall w)(w in z iff (w in x or w = y)).
iv. Induction. If a formula holds of emptyset, and whenever it holds of x,y,
it holds of x adjoined with y, then it holds of everything.

THEOREM 1.1. FST and ZFC\INF + not(INF) have the same theorems.

THEOREM 1.2. FST, ZF\INF, ZFC\INF + not(INF), PA are equiconsistent and
mutually interpretable.

It would be very satisfactory if such a reaxiomatization of ZFC were
possible in such fundamental terms. Attempts at reaxiomatization in terms of
fundamental principles of reflection partially succeed (see my website).

Here we take a different approach. We wish to support the following idea:
the axioms of set theory are simply transfers of fundamental facts about the
standard model of finite set theory, HF = V(omega), together with the axiom
of infinity. 

The sense is that the fundamental facts about HF = V(omega) should have
nothing to do with finiteness, and that the infiniteness of sets should not
matter. 

In fact, we go further. We wish to support the idea that the axioms of set
theory are simply transfers of fundamental facts about HF = V(omega) that
are derivable in FST, together with the axiom of infinity.

2. SCHEMES.

Let L be a language in first order predicate calculus with equality. By
this, we mean a countable set of constant, relation, and function symbols,
together with the special binary relation symbol =.

A schematic language (in first order predicate calculus with equality) is a
system L* = (L;L'), where L and L' are two disjoint countable sets of
constant, relation, and function symbols. To avoid some trivialities, we
will assume that L' contains no constant symbols.

The essential point is that the elements of L' serve as schematic letters.
Thus the usual axiomatization of ZC is based on the schematic language
(epsilon,=;R), where R is unary. The usual axiomatization of ZFC is based on
the schematic language (epsilon,=;R,S), where R is unary and S is binary.

A scheme in L* is simply a formula in the language L union L'.

Each scheme in L* gives rise to *instances*, which are formulas in L. To
define these, we use the notion of an L* substitution.

An L* substitution is a partial function alpha from L' into tuples of the
form (phi,v1,...,vk), where phi is a formula of L and v1,...,vk are distinct
variables. If R is a k-ary relation symbol in L' lying in the domain of
alpha, then the number of v's in alpha(R) is k. If F is a k-ary function
symbol in L' lying in the domain of alpha, then the number of v's in
alpha(R) is k+1. 

Let psi be a scheme in L*. We say that alpha is an L* substitution for psi
if and only if 

i. alpha is an L* substitution.
ii. the domain of alpha consists of all symbols of L' appearing in psi.
iii. no variables appearing in the values of L' (either in the formula or
among the v's) appears in psi.

We now perform the substitution, creating the formula psi[alpha]. Each
atomic subformula of psi is replaced by a formula of L' as follows.

In this first abstract, we will only have relation symbols in L*, and this
simplifies the situation considerably. We will postpone treatment of the
general case, with constants and functions in L, and functions in L' until
it is time to make use of it.

Let R(x1,...,xk) be a subformula of psi, and let alpha(R) = (phi,v1,...,vk).
Replace R(x1,...,xk) by the formula phi[v1/x1,...,vk/xk] of L.

3. QUANTIFIER FREE COMPREHENSION FORMULAS.

A comprehension formula in L is a formula of the form

1) (therexists x)(forall y)(y in x iff phi)

where x,y are distinct variables, and phi is a formula in L in which x is
not free. 

A comprehension scheme in L* is a scheme of the form

2) (therexists x)(forall y)(y in x iff psi)

where x,y are distinct variables, and psi is a scheme in L* in which x is
not free. We often abuse terminology and identify a scheme with its
instances.

In this section, we will adhere to the language epsilon,containedin,=. We
write this language as L(ep,co,=).

Inclusion is obviously a completely fundamental notion in set theory, in the
same category as membership and equality.

In a later abstract, we will address the following issue: are the results
artificially biased by the choice of inclusion? We will at a later time
consider what happens if we use other primitives. Obviously inclusion is not
some random binary relation on sets, and we will later develop criteria for
the "simple" relations.

So let us consider all comprehension formulas in epsilon,containedin,=,
where the phi is QUANTIFIER FREE. We call these

*quantifier free comprehension formulas*

which is an abuse of notation since the formula itself is obviously not
quantifier free - only the phi inside.

THEOREM 3.1. The universal closure of any given quantifier free
comprehension formula in L(ep,co,=) is provable or refutable in FST.

THEOREM 3.2. There is an elementary recursive decision procedure for
determining whether a given quantifier free comprehension formula in
L(ep,co,=) holds in V(omega).

THEOREM 3.3. Let phi be a quantifier free comprehension formula in
L(ep,co,=). The following are equivalent.
i. phi holds in V(omega).
ii. phi is provable in FST.
iii. FST + phi is consistent.
iv. phi holds in V(lambda), for some limit ordinal lambda.
v. phi holds in V(lambda), for all limit ordinals lambda.
vi. phi holds in V.

Let QFC be the following theory in L(ep,co,=).

i. Definition of inclusion. x containedin y iff (forall z)(z in x implies z
in y).
ii. all quantifier free comprehension formulas that hold in V(omega).

QFC is a very interesting theory, with lots of consequences. However, it
does not appear to have much logical strength. In particular, it is
interpretable in EFA (exponential function arithmetic).

THEOREM 3.4. QFC is a proper fragment of FST that has the following
consequences.
i. Definition of inclusion.
ii. Extensionality.
iii. Pairing.
iv. Pairwise union.
v. Pairwise intersection.
vi. Set theoretic difference.
vii. Power set.
viii. No epsilon chains.
QFC is provable from the above if we add separation.

Also it appears that QFC + Infinity does not have significant logical
strength. Here we can take Infinity to be the usual formulation in terms of
emptyset and x union {x}, or the stronger version with x union {y}.

4. QUANTIFIER FREE COMPREHENSION SCHEMES.

Here we investigate quantifier free comprehension schemes in the schematic
language (epsilon,containedin,=;R), where R is unary. We write this language
as L(ep,co,=;R). I.e.,

(therexists x)(forall y)(y in x iff psi)

where psi is a quantifier free scheme in L(ep,co,=;R).

Of particular importance is the quantifier free comprehension scheme

(therexists x)(forall y)(y in x iff (y in a and R(y)))

called the separation scheme.

THEOREM 4.1. Let S be a quantifier free comprehension scheme in L(ep,co,=).
Then either every instance of S is provable in FST, or there is an instance
of S whose universal closure is refutable in FST. Furthermore, if the former
holds then S is true as a universal monadic second order statement over HF =
V(omega).

THEOREM 4.2. There is an elementary recursive decision procedure for
determining whether a given quantifier free comprehension scheme in
L(ep,co,=) holds in V(omega) in either of the two equivalent senses used in
Theorem 4.1.

THEOREM 4.3. Let phi be a quantifier free comprehension scheme in
L(ep,co,=). The following are equivalent.
i. phi holds in V(omega).
ii. phi is provable in FST.
iii. FST + phi is consistent.
iv. phi holds in V(lambda), for some limit ordinal lambda.
v. phi holds in V(lambda), for all limit ordinals lambda.
vi. phi holds in V.

Let QFCS be the following theory in L(ep,co,=).

i. Definition of inclusion. x containedin y iff (forall z)(z in x implies z
in y).
ii. all instances of all quantifier free comprehension schemes, where all
instances of the quantifier free comprehension scheme hold in V(omega).

We can obviously modify ii according to the last claim of Theorem 4.1, and
get the same theory.

THEOREM 4.4. QFCS is a fragment of FST (and in fact of ZF without
replacement and infinity) that proves the following.
i. Definition of inclusion.
ii. Extensionality.
iii. Pairing.
iv. Separation.
v. Power set. 
vi. Pairwise union.
vii. No epsilon chains.
QFCS does not prove union or foundation or replacement or transitive closure
or not(infinity) or the axiom of choice. QFCS is equiconsistent with and
mutually interpretable in FST.

We now come to the main point: QFCS + Infinity. Here Z is Zermelo set
theory, which we take to be ZFC without choice, foundation, replacement.
I.e., extensionality, pairing, union, power set, separation, infinity.

THEOREM 4.5. QFCS + infinity is a fragment of Z, that is equiconsistent with
and mutually interpretable in Z and ZFC\Replacement.

We can take any reasonable formulation of Infinity for Theorem 4.5. The most
relevant one to our general theme is b below. There are several ones that
are in common use. E.g.,

a. There is a set that contains the empty set and is closed under the
operation x union {x}. This is the one most commonly used in renditions of
ZF(C).
b. There is a set that contains the empty set and is closed under the
operation x union {y}. This is the one most commonly used in renditions of
ZF(C). This has the advantage that it gives rise to V(omega). The previous
version does not over ZC.
c. There is a set that contains the empty set and is closed under the
operation {x}. This is the version in Zermelo's 1908 paper.
d. There is a nonempty set with no epsilon maximal element.
e. There is a one-one function from a nonempty set into a proper subset.
f. There is a function from a proper subset of a set onto the set.
g. There is a linear ordering with no greatest element.
h. There is a nonempty set of subsets of some set, with no maximal element
under inclusion. 

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

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

Harvey Friedman