5
$\begingroup$

I was reading something which contained the following statement:

It is a well-established mathematical result that theories consisting only of recursive definitions... are inherently consistent.

Does this result have a name? Could anyone point me to literature about this?

  • 0
    @Niels Diepeveen: For example, take the powerset lattice of $\{0,1\}$ and let $\phi$ be a (nonmonotone) operator such that $1 \in x$ if and only if $1 \not \in \phi(x)$. This operator cannot have a fixed point, and in that sense it represents a self-contradictory definition.2011-03-12

1 Answers 1

8

It is not true in the most general sense but it is true in a certain sense.

One way that it is true in the sense of the Knaster–Tarski theorem:

If $L$ is a complete lattice and $\phi\colon L \to L$ is an order-preserving function, then the set of fixed points of $\phi$ is a complete sublattice of $L$, and in particular the set of fixed points in nonempty.

Many recursive constructions correspond to order-preserving maps on a complete lattice, and so by this theorem the constructions do have fixed points. Those fixed points correspond to the thing that the recursive definition is trying to construct.

For example, to construct the Borel sets on a topological space $X$, consider the lattice of all sets of subsets of $X$. This is a powerset lattice and so it is complete. Let $\phi$ be the following operator: given a family $F$, $\phi(F)$ contains every set that can be obtained as a countable union of sets from $F \cup F^c \cup O$ where $F^c$ is the set of complements of sets in $F$ and $O$ is the set of open sets in $X$. Then $\phi$ is a order-preserving operator, and its least fixed point is the family of Borel sets of $X$.

Now here is a sense in which recursive definitions do not always define something. It's related to the field of "general recursive functions" which was an early way that people studied computability. Suppose that we we write down a set of recursive definitions for a function: $ f(0) = 5 \qquad f(x+1) = 2f(x)+x $ That particular definition does define a total function $\mathbb{N} \to \mathbb{N}$. But in general there is no reason to expect an arbitrary set of rules will work. For example, $ f(0) = 1 \qquad f(3x) = x + 2 \qquad f(x+1) = 2 $ does not define a function. The point here is we are considering arbitrary definitions, not just definitions in the form of the first example.

Here is an example based on the Collatz conjecture; does it give a total function? $ f(0) = 0 \qquad f(1) = 1 \qquad f(2x) = f(x) \qquad f(2x+1) = f(6x+4)$

As you can see, the problem of telling which sets of rules actually define a total function is far from simple, and it only gets worse if you have a system of several mutually recursively defined functions.

There is a third aspect of the problem, relating to the foundational importance of inductive definitions. For example, in unformalized mathematics, the natural numbers are the smallest set of objects which contains 0 and is closed under successor. This sort of concrete inductive definition is one reason that people often feel that the natural numbers are more directly accessible to intuition than, say, arbitrary uncountable sets.

  • 0
    The idea is that the elements of the lattice are "approximations", of some sort, to the object you're trying to define. The operator takes one approximation and gives you back another, better approximation ("better" in the sense that it's closer to being the object you're trying to construct). A fixed point under this operator is an approximation that the operator can't improve, and that will be an actual example of what you're trying to construct. But not every recursive definition falls into that framework. And not every operator has to have a fixed point; the order preserving ones do.2011-03-12