In Types and Programming Languages by Pierce,

  1. Section 9.4 Curry–Howard correspondence on p109 has a table

    enter image description here

    Does the table mean that the simply typed lambda calculus λ→ corresponds to propositional logic (i.e. the zeroth order logic)?

  2. Does the following quote on p109 mean that System F correspond to the second order logic?

    System F (Chapter 23), whose parametric polymorphism involves quantification over types, corresponds precisely to a second-order constructive logic, which permits quantification over propositions.

  3. Which programming language system correspond to the first order logic?

    In system λ→, a term varies in a type, so doesn't λ→ more correspond to the first order logic than to the propositional logic?

  4. Which logic system does the untyped lambda calculus correspond to?

    Does Curry-Howard Correspondence only care about typed systems, not untyped systems?

  5. p109 continues to say

    System Fω (Chapter 30) corresponds to a higher-order logic.

    Section 30.4 on p461 defines system Fi, where i = 1, ..., in terms of kinds, and calls F2 (the same as System F above) the second order lambda calculus. Is system F1 (the same as System λ→ above) called the first order lambda calculus?

    What order logic does System Fi correspond to?

  6. Do the order in logical system and the order in the hierarchy of kinds in Section 30.4 not match?

    For example, λ→ corresponds to the proposititional logic (my part 1), so its order of logic system is 0, or it might correspond to the first order logic, and its order might be 1 (see my part 3). λ→ is system F1 in the hierarchy by kinds (c.f. Section 30.4), so its order in the hierarchy of kinds is 1. The two orders may or may not match, depends on which logic λ→ corresponds to.

    For another example, System F corresponds to the second order logic (my part 2), and is system F2 in the hierarchy by kinds (c.f. Section 30.4). So the two orders seem to match.



1 Answer 1


I'm not confident enough about the later questions, but I hope I can give a partial answer, since this hasn't been given much love.

  1. Yes
  2. Yes
  3. There is nothing in particular, since first-order logic quantifies over non-logical objects, but a priori there are no non-logical objects we're reasoning about for the lambda calculus. There is a similar-sounding type system (Hindley-Damas-Milner which allows some quantification over types, but this is not related to the non-logical quantification of FOL)
  4. The untyped lambda calculus does not directly correspond to anything, since the Curry-Howard correspondance related Types to Propositions, so in the untyped setting there is no proposition to prove. Also: since the untyped lambda calculus has the Y combintor, so it's very likely any attempt will make it inconsistent. To answer a potential further question, we would also get inconsistency if we added a fixed-point combinator $\mu: (\tau \to \tau) \to \tau$ to most any lambda calculus. This is more or less equivalent to naive set comprehension. The exceptions for losing consistency are some weak linear logics (E.g. EAL or Łukasiewicz) and corresponding lambda calculi.

To the best of what I can tell, you're mostly correct here.

  1. For system $F_i$, $i \geq 2$ should correspond to ith-order logic. The only difference is that first-order logic doesn't quite fit into this hierarchy.
  2. Seems like yes

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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