Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
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.


All this is described in detail in Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor.

share|cite|improve this answer

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.

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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.