🚀 go-pugleaf

A "recursive definition" of a name X is a sentence of the form

  X := E

where E is an expression that contains X as a free variable.  Naively we
might associate with such definitions the axiom

  X := E => X = E

To express what a definition means.  (We also need some syntactic rules
to allow the introduction of definitions so that the same name is not
used for different purposes.)

Here are some examples of recursive definitions:

(1) x := x + 1
(2) x := x * 2
(3) x := 1/x
(4) x := x * 1

Definition (1) fails to define x because there is no x that satisfies
the equation.  (3) and (4) both fail to define x because there are more
than one object that satisfy the equation.  (2) defines x = 0 because
that is the unique solution to the equation.  When a recursive
definition is based on an equation that has a unique solution, then it
is called a well-founded recursion.  If the equation has no solution or
more than one solution, the recursion is said to be ill-founded.

Using (1) and the naive axiom of definition you can prove

  x := x + 1
  x = x + 1
  x - x = 1
  0 = 1

which is a contradiction.  The lesson is that before you can use a
recursive definition in a proof, you must show that it is well-founded.

A recursive set definition might look like this:

  S := {x : (x = {} or x = S) and ~(x E x)}                (5)

It should be clear that (5) is a recursive definition.  It should also
be clear that there is no S satisfying the equation implied by the
definition, therefore it is an ill-founded recursive definition.
Furthermore, there is no need to look further for an ``explanation'' of
the inconsistency that arises when you assume that the definition
actually defines something.  When you have said that the definition is
an ill-founded recursive definition you have said all that needs to be
said.

What I have written up to now is well-known and should be
uncontroversial.  So now lets apply the notions to the theory ZF (or Z,
for that matter) by adding definitions with the proper syntactic
restrictions and adding the naive axiom of definition:

  X := E -> X = E

to get the theory ZF+ND.  (This theory is inconsistent, but let's ignore
that for now).  In ZF+ND you can form the following paradoxical set:

  S := {x E {{},S} : ~(x E x)}                            (6)

Clearly, this is logically equivalent to (5) and so is also a definition
based on an ill-founded recursion.  This is a simplified version of the
paradox of the library catalogue that lists all catalogues that do not
list themselves.  Curry, in _Foundations of Logic_ dismisses this
paradox rather sanguinely as a ``pseudo-paradox'', saying that the
catalog just cannot be constructed.  But it is obvious (to me, anyway)
that this is merely a finite version of Russel's paradox, less artfully
concealed because the recursion is explicit.

But consider the paradoxical definitions

  S := {{},R}
  R := {x E S : ~(x E x)}                                (8)

where the definition of R has exactly the same form as the definition of
Russell's paradoxical set (replacing S with the universal set).  But
here, S is a set with only two elements!  Given such a clear example of
Russell's paradox by quantifying over a finite set, I don't see how
anyone can still claim that Russell's paradox is somehow caused by a
universal set that is "too big".  Size has nothing to do with it, the
only consideration is how it is defined.  Clearly in this example the
problem is an ill-founded mutual recursion between the two set
definitions.

Now let us take one more step and consider the theory ZF+ND+U of ZF+ND
with a universal set axiom:

  Forall y. y E U

People knowledgeable in set theory will immediately recognize this as an
inconsistent theory, because ZF |- ~U.  However, the theory ZF+ND is
already inconsistent, so I haven't done any damage.  If the reader will
bear with me I will solve both of these inconsistencies in one swell
foop at the end (trust me :-).

Consider

  S := {x in U : ~(x E S)}

which is an ill-founded recursive definition.  If you replaced the
second S with another set (that is not defined recursively with S), then
this definition would not lead to inconsistency, so I hope that everyone
will agree with me that the "cause" of the inconsistency in the above is
the ill-founded recursion.

Now consider Russell's paradoxical set

  R := {x E U : ~(x E x)}

which is clearly not recursive in the sense I gave above.  In other
words, the name being defined does not occur (syntactically) in the
expression.  Just as clearly though, this R is closely related to the
one in (8).  I claim then, that there is an ill-founded mutual recursion
going on between this definition and the definition of U.  Basically, U
is defined by quantifying over all y, where R is one of the y.
Similarly, R is defined as an element of U.  Recursion-by-quantifier is
not included my original definition of recursion, so I will have to
broaden the definition.

Before I give my new definition of recursion, let me discuss
impredicativity and explain why I did not use that term to begin with.
Impredicativity, as I understand it, is the use of a quantifier over a
domain that is incomplete in some sense.  One might say that {x E U :
~(x E x)} is impredicative because x quantifies over a set U that
contains x, and that U is not complete until x is defined.  I don't like
this notion because it seems vague.  After all, there is no time for
mathematical objects, so the phrase "when" must be an analogy for
something _like_ a period of time, but I have no idea what this
analogous thing is.  (Whatever it is, it is _not_ a stage in the
iterative hierarchy, because assuming that is equivalent to assuming
that all sets are defined by the iterative hierarchy --a position that I
deny.)

Now I could have used the term "impredicative" instead of "recursion"
since I am forced to generalize either term to make it work.  I chose
recursion in order to avoid giving the impression that I was making
arguments similar to the various arguments about impredicativity that
have been made before.  But I have not agreed with any of those
arguments, and I wanted to avoid this confusion.  Unfortunately, the
confusion arose anyway.  I hope these comments are enough to straighten
things out.

Going back to recursion, I want a redefinition of the concept that will
bring out the similarity in all the inconsistent definitions I have
proposed.  Clearly, S := {x E U : ~(x E x)} does contain a sort of
circularity in that the variable x quantifies over a set that contains
S.  We can expand the above notation into something like

  S := (if x1 E x1 then {} else {x1}) union
         (if x2 E x2 then {} else {x2}) union
	   (if x3 E x3 then {} else {x3}) union ...

with one term for each set in U.  If we do so (and the sets are
enumerable) we will find one expression at some finite position i where
xi = S.  There is the recursion.  The recursion is not syntactic, but
there is certainly a circularity in the definition.

So I propose to redefine the notion of a recursive definition to be
something like  "X := E is recursive if E contains a free occurence of
X or if E contains a bound variable that quantifies over a class that
include the value that X would denote if it denotes anything".  "Would
denote" obviously requires formalization.  Furthermore, this definition
does not include the possibility of a term F(y) where y quantifies over
such a range that F(y) = X for some y.  So I propose

  Definition: a definition X := E is _recursive_ iff there is a proper
  subterm F of E such that X=E => X=F for some legal substitution of the
  bound variables in E.

This does not entirely solve the problem of Russell's paradox because
that paradox exists without the axiom of definition.  So I propose the
following definition of a recursive term:

  Definition: a term E is _recursive_ iff there is a proper subterm F of
  E such that E=F for some legal substitution of the bound variables in E.

Then we can talk about ill-founded recursive terms as well as about
recursive definitions.  The distinction, I think, is not essential.

Notice that I am not claiming that all recursion causes paradox.  On the
contrary, I believe that set theories should allow recursion, and ZF's
lack of it is one of the reasons I think the theory is inadequate.  I
claim that the problem is caused specifically by _ill-founded_ recursion
in my sense, namely that the equation implied by the definition does not
have a unique solution.

And I don't think that there is any mysterous problem about ``defining
something in terms of itself'' or ``quantifying over something that does
not yet exist''.  There is simply the problem that some equations don't
have unique solutions.  And this problem only tells us that we have to
be careful what we take to be definitions, it does not tell us that some
sets are too big to be sets, that self-reference is illegitimate, or
that recursion is illegitimate.

I propose for discussion the

  Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E

where "Exist! x" means "there exists a unique x such that".  What if you
altered ZF to contain this axiom (and introduction of definitions)?  In
the first place, you could immediately prove the existence of all sets
that are already there.  And by adding some of the well-known machinery
from recursion theory to prove Exist!... you could also talk about a lot
of self-containing sets.  Wouldn't this theory be much more powerful
than ZF?
-- 
					David Gudeman
gudeman@cs.arizona.edu