Question about recursion theorem
I'm having difficulties understanding some material in a book I'm reading. (Hrbacek, K., Jech T., Introduction to set theory, 3rd Edt.). In the book there is a presentation of three variants of Recursion Theorem. The first variant states:
For any set
, any
and any function
there exists unique infinite sequence
such that
a/ 
b/ )
I understand that theorem is meant to prove existence of functions, described recursively, like n! And I think I understand the proof. It introduces the term "n-step computation" which is finite sequence. The first element is the initial value and every next element is calculated from the previous, using g. Each separate computation is a function on some
, hence it's a set of ordered pairs. Therefore each n-step computation is element of the power set of
. Then the set of all computations may be defined:
 | \text{t is an n-step computation for some n}\})
The proof procedes to show that all n-step computations for certain g are compatible functions, hence their union is a function. The proofs completes with establishing that the function has the desired properties.
So far so good, but then comes the second version - more general construct for functions like Fibonacci sequences in which each member of the sequence is calculated from several of the preceding ones:
For any set
and any function
there exists unique sequence
such that:
for all 
(
means all finite sequences of elements of S, < and > are used to denote sequences and <> is used to denote the empty sequence).
The proof relies on the first version of recursion theorem. We set
,
and
, defined as:
if t is a sequence of length n
otherwise
Here I'm loosing the idea behind the notation and any clue how the proof stated further on works. g must stand for any function that calculates value from a given sequence. It seems that application of the first version of the recursion theorem yields a sequence that can be described this way:

>\})
This is actually in the book. Then the book states by now it's easy to prove that every
is actually member of the set of all functions on n into S
. But it's not obvious to me how it is so.

(
is some element of S)
>\}\cup\{<1,g(F_{1})>\})

The resulting sets of the type
do not look like function at all, if one takes a function to be set of ordered pairs. Am I reading the notation wrong here?
I am interested in other sources, where this theorem is proven this or other way, preferably more understandable for a newbie.
Re: Question about recursion theorem
Quote:
Originally Posted by
mrproper
The resulting sets of the type
>,<1,g(F_{1})>,\cdots\})
do not look like function at all, if one takes a function to be set of ordered pairs.
Maybe, I'm missing something, but it looks like a set of ordered pairs to me. It has as members such ordered pairs as
<0 g(F_0)>
<1 g(F_1)>
etc.
and no other members.
All ordered pairs.
I don't see any difficulty with that.
Re: Question about recursion theorem
You mean that I should consider that other definition of ordered pair which uses sequences? So the set becomes ), (1,g(F_{1})) ...})
Re: Question about recursion theorem
Definitions:
<j k> = {{j} {j k}}
x is an ordered pair <-> Ejk x=<j k>
f is a relation <-> Ax(x in f -> x is an ordered pair)
f is a function <-> (f is a relation & Axyz((<x y> in f & <x z> in f) -> y=z))
f is a sequence <-> (f is a function & dom(f) is an ordinal)
Perhaps what you're asking about is whether we use tuples or whether we use functions in certain contexts.
Let's define 'tuple' this way.
h is a tuple construction sequence
<->
h is a finite sequence &
An(n+1 in dom(h) -> Ej h(n+1)=<h(n) j>)
t is a tuple
<->
Eh(h is a tuple construction sequence & t in range(h))
I.e., a tuple is the result of using the ordered pairing operation n number of times for some natural number n.
Then, for any tuple there is the corresponding sequence, and vice versa:
The n-tuple <x y ... z> corresponds to the sequence {<0 x> <1 y> .... <n z>} and vice versa.
So, in most instances, it doesn't matter which we use, tuples or sequences.
In any case, the set you mentioned is clearly a function.
Re: Question about recursion theorem
That's right. So I'm reading the proof correctly. But something worries me here... The recursion theorem is given early in the book as a tool for constructing isomorphisms. To the moment of introduction of the theorem the ordered pairs are defined only the way Kuratovski did. (a,b)={{a}, {a,b}}. And the author seems quite precise in such details. Why then he hasn't written
instead of =t\cup\{<n,g(F_{n})>\})
Anyway, I'm trying to read this book from quite some time and sometimes I just "crash" when I try to understand what's encoded in the notation. Is there any source that can help me understand notation better?
Re: Question about recursion theorem
I don't have the book. I'd have to see how the author specifies the usage of "( )", but is there any indication that "( )" is meant differently from "< >"? Sometimes authors use both "( )" and "< >" for the same thing:
(x y ... z) = <x y ... z> = <<<x y> ... > z>
And sometimes authors slip back and forth with the word 'sequence' where it may mean a tuple or it may the corresponding function on a natural number. In most contexts, you can see how it doesn't matter which of the very similar things is used, tuples or functions.
Re: Question about recursion theorem
In this case it seems that it doesn't matter. The author states the same thing 10 or so pages further on.
I'm interested if the Recursion theorem in this book actually related to some of Kleene's recursion theorems. Kleene's recursion theorems are described and proved in Wikipedia, but it's formulation is not as newbie-firendly...
Re: Question about recursion theorem
By the way, one difference is that the axiom schema of replacement is needed to prove:
EbAn((n is a natural number & t is an n-tuple of members of x) -> teb)
But the axiom schema of replacement is not needed to prove:
EbAn((n is a natural number & f is a sequence of length n of members of x) -> feb)
In other words, we need the axiom schema of replacement to prove there is the set of all tuples of members of x. But we don't need the axiom schema of replacement to prove there is the set of all finite sequences of members of x.
Re: Question about recursion theorem
I have the book, and I'll have to check if I'm recalling the correct one, but I believe they made a difference between ordered pairs and n-tuples (2-tuples). The difference, however, is slight and inconsequential to the results (more syntactical than semantical). That might explain the difference between the two uses. However, I could be thinking of another book.
Re: Question about recursion theorem
mrproper, you might want to have a look at section "5. Operations and Structures" in Chapter 3 (pp 56-7). Below is a snippet from that section.
_________________________________________________
We now proceed to give a general definition of a structure. In Chapter 2, we introduced a unary (1-ary), binary (2-ary),and ternary (3-ary) relations. The reason we did not talk about n-ary relations for arbitrary n is simply that we could not then handle arbitrary natural numbers. This obstacle is now removed, and the present section gives precise definitions of n-tuples, n-ary relations and operations, and n-fold cartesian products, for all natural numbers n.
We start with the definition of an ordered n-tuple. Recall that ordered pairs
has been defined in Section 1 of Chapter 2 as a set that uniquely determines its two coordinates ... In analogy, an n-tuple should be a set that uniquely determines its n coordinates ...; that is, we want
 \ (a_0, ..., a_{n-1}) = (b_0, ..., b_{n-1}) \text{ if and only if } a_i = b_i, \text{ for all } i = 0, ..., n-1)
But we already introduced a notion that satisfies (*): it is the sequence of length n ... [it] is just a reformulation of equality of functions, as in Lemma 3.2 in Chapter 2 (see page 24: Functions F and G are equal iff their domains are equal and for all points x in the domain F(x) = G(x))
_________________________________________________
Now, recall that under Section 3 "The Recursion Theorem" of Chapter 3, page 46, they define a sequence as "a function whose domain is either a natural number or N," (i.e., either the elements less than a given natural number or the set of all natural numbers itself). Thus, a sequence is defined as a function of a certain domain. It is obviously clear that if two sequences S and S' were both sequences of length n, then their domains would both be the natural number n, itself, and if they agreed at each coordinate (i.e., for every x in n, S(x) = S'(x)), then this satisfies Lemma 3.2 for equality of functions.
As you read through the Recursion Theorem here, do not think of them as merely functions that are themselves a set of ordered pairs. Think of them as members from
. (Recall definition 3.13 on page 26:
is the set of all functions on A into B.)
Re: Question about recursion theorem
I was reviewing Theorem 3.5 (p. 50), which states.
For any set S and any function
there exists a unique sequence
such that
 = g(\langle f_0, ..., f_{n-1}\rangle), \text{ for all } n\in N.)
I think it is important to break this down so we're clear on what is being stated. First off, the Seq(S) is nothing but the union of all functions from n into S (p. 46):
 = \bigcup_{n\in N} S^n)
This is a complicated statement because the theorem is saying for any set S and for any function g that maps into S from, basically, the set of functions from n into S, then we can define another function f that maps from N into S (obviously, based on g). In particular, this is done by defining
(f evaluated at n, see definition 3.1 on page 23). But what is
? It is nothing but a function defined at n, for all
where at each n it is equal to g evaluated at f restricted to n. But as the equality in the above statement goes, this is just g evaluated at a sequence of f for each numbered index before n.
The proof begins by defining the sequence (function):
, with

 \rangle\}, \text{ for all } n\in N)
For clarity on the solution, notice that
consists of a sequence of the points into g as defined for
in the theorem statement, and g maps into S. The proof will conclude by letting
, which is clearly a function from N into S.
Before we get there, however, we need to establish the existence of the defined sequence above. This follows from the Recursion Theorem, as pointed at on page 50. They show you the substitutions to make into the Theorem, which we could line up side-by-side, but I'll just state substituted below.
Recursion Theorem (substituted for this problem):
For any set Seq(S), any
, and any function
, there exists a unique infinite sequence
such that
(a) 
(b)
, where
 = t \cup \{\langle n, g(t)\rangle\}, \text{ if t is a sequence of length n}, \langle \rangle, \text{ otherwise.})
You should be able to see the clear correspondence with G(t, n) and <F>. Therefore, <F> is well defined and exists by the recursion theorem. The authors go on to state that it is easy to prove by induction that each
belongs to
and that
for all
. By previous results, this establishes that
is a compatible system of functions. Note, this is saying that the range of
is a compatible system, and a compatible system just is (Definition 3.10 page 26) a set of functions for which any two functions in it are compatible; furthermore, any two functions are compatible if their points evaluated are equal for every point that belongs to the intersection of those function domains.
The domain of <F> is the natural numbers and its range is based on
which maps to S. Thus, this establishes the concluding statement mentioned earlier:
Let
; then clearly
and
. Therefore, this concludes what was needed since,
 = g(F_n) = g(f\ |\ n))
I think if you look at this final statement it should make things appear clearer because it tells you precisely what is going on. It is easy to get confused about the n's that are being thrown around. When F_i is being defined, you have to remember that it is a function of numbers, and as the statement above points out, any
just is g evaluated at
. Remember, further, why this follows:
. So what do we get by the definition of
? Remember, it was defined as a union.
Re: Question about recursion theorem
Thank you very much for the replies! I was on holiday at a place with almost no Internet (I would never go if I knew beforehand (Happy)), so I was unable let You know that thanks to this discussion I finally understood the proof. It doesn't look that complex now.