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.
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:
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:
System T is the simply typed calculus enriched with booleans, natural numbers and primitive recursion on them.
All this is described in detail in Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor.
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.