How does second-order logic relate to lambda calculus? How does second-order arithmetic/logic relate to lambda calculus? By lambda calculus, I mean both typed and untyped. And is there any relationship with recursive and recursively enumerable sets?
Edit: some edits.
 A: The question is rather vague. However, I recall something that you may be interested in:
System F is a typed lambda calculus that has a very interesting property:

An arithmetic function can be represented in System F if and only if it can be proved total in second order Peano arithmetic.

This also means that in System F we can represent basically all total functions we can ever imagine.
There is also a weaker system called Gödel System T, for which there is a similar theorem:

An arithmetic function can be represented in System T if and only if it can be proved total in first order Peano arithmetic.

System T is the simply typed calculus enriched with booleans, natural numbers and primitive recursion on them.
Also:


*

*All functions representable in System F and System T are total.

*This means that those systems (unlike the untyped lambda calculus) are not Turing complete.


All this is described in detail in Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor.
A: The obvious result that comes to mind (which talks both of second-order logic and computability) is that second-order consequence -- when defined using the natural 'full' semantics (so second-order quantifiers run over all subsets of the domain) -- is not recursively axiomatizable. 
Otherwise it is unclear what kind of relation is being enquired about. 
