Where was this first published? (Sorry - don't have access to the CW)

I understand that the theorem is due to Spector (1956) On degrees of recursive unsolvability, Annals of Mathematics 64:581-592. It's a very nice theorem: Shore stresses its use in eliminating second-order quantification.

@Joel: You are quite right about the error in my, now deleted, answer.

How are functions specified? Will your logic include the lambda-calculus (e.g., is a Henken-like calculus)? Do you want to have, say, all linear transformations?