# What order logic does a system correspond to under Curry–Howard correspondence?

In Types and Programming Languages by Pierce,

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

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 quantiﬁcation over types, corresponds precisely to a second-order constructive logic, which permits quantiﬁcation 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.

Thanks.

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