How does second-order logic relate to lambda calculus?

Question

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.

Answer 1

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.

Answer 2

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.