# 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.

-
That's a rather fuzzy question. Could you be a bit more specific about which kind of relation you're looking for? Just name-dropping a few basic computability concepts does not help much figuring out which connection to second order logic you want to know about. –  Henning Makholm Feb 18 '13 at 7:39
Edited the question. –  hwe Feb 18 '13 at 9:21

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 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.

-
Edited the question. By "consequence", you mean second-order sentences? –  hwe Feb 18 '13 at 9:22