In Types and Programming Languages by Pierce,
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)?
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.
Which programming language system correspond to the first order logic?
λ→, a term varies in a type, so doesn't
λ→more correspond to the first order logic than to the propositional logic?
Which logic system does the untyped lambda calculus correspond to?
Does Curry-Howard Correspondence only care about typed systems, not untyped systems?
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?
Do the order in logical system and the order in the hierarchy of kinds in Section 30.4 not match?
λ→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
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.