Recursion theorem (set theory)

[Jerbearrrrrr]

There are probably a million theorems called "the recursion theorem" and I'm not sure if this is actually one of them, but there's a remark saying that it defines recursion.
It's proven by piecing together 'attempts' (functions defined on subsets of a domain) and states:

For X a well-ordered set, Y any set:
For any G:P(XxY)->Y,
there exists f:X->Y
such that f(x)=G(f|Ix), for all x in X.

where:
Ix is the initial subset {y in X iff y<x}
f|A = {(x,f(x) : x in A} - the restriction of f to A.
P denotes power set.

I just have no idea what it's saying.

Googling suggests that it's "Cantor's theorem, originally stated for ordinals, which extends inductive proof to recursive construction." but I can't find anything on it, possibly because the lecturer has mixed a few proofs together so it's a weaker form of a better-known theorem, but much easier to prove.

Thanks :\

[edit]
Wait...is this just saying that, for any G:{functions}->{numbers}, there's a function, f, that satisfies f(5)=G[f(4)]? And so on.

 

[Hurkyl]

If X is natural numbers, then f(5) = G(f(0), f(1), f(2), f(3), f(4)).

I've taken the liberty of writing the set {(0, f(0)), (1, f(1)), (2, f(2)), (3, f(3)), (4, f(4))} -- the graph of f restricted to {0,1,2,3,4} -- as an ordered sequence

 

[JSuarez]

Wait...is this just saying that, for any G:{functions}->{numbers}, there's a function, f, that satisfies f(5)=G[f(4)]? And so on.

Not exactly: as Hurkyl already said, f(5) is more complicated; what it states precisely is that, given G as you defined it above (where the "functions" are the ones from the well-ordered set X to any set Y) you can define an unique function [itex]f:X\rightarrow Y[/itex], given by f(x)=G(f|Ix), where Ix is the initial x-segment of X. For example, if [itex]X=Y= N[/itex], this means that:

[tex]
f\left(0\right)=G\left( \emptyset \right)
[/tex]
[tex]
f\left(n\right)=G\left(In\right)=G\left( f \left( 0 \right),f \left( 1 \right),\cdots,f \left( n-1 \right) \right)
[/tex]

This form is usually called course-of-values recursion and it's equivalent to the recursive definition that you are familiar with.