Why can System F1 a.k.a. λ → have kind `*`, but no quantification `∀`?

Question

In Types and Programming Languages by Pierce, on p461 in Section 30.4 Fragments of Fω

30.4.1 Definition: In System F1 , the only kind is * and no quantification (∀) or abstraction (λ) over types is permitted.

F1 is just our simply typed lambda-calculus, λ → . Its definition is super- ficially more complicated than Figure 9-1 because it includes kinding and type equivalence relations, but these are both trivial: every syntactically well formed type is also well kinded, with kind *, and the only type equivalent to a type T is T itself

Is it correct that quantification ∀ means universal types?

* is the kind of proper types, which are introduced on p442:

The level of types contains two sorts of expressions. First, there are proper types like Nat, Nat→Nat, Pair Nat Bool, and ∀X.X→X, which are inhabited by terms. (Of course, not all terms have a type; for example (λx:Nat.x) true does not.)

So universal types such as ∀X.X→X are proper types, and thus belong to kind *. Why can System F1 have kind *, but no universal types, i.e. quantification ∀?

But if System F1 could have kind * and quantification ∀, then wouldn't it become the same as System F2 a.k.a. System F? Quoted from on p461:

In System F2 , we still have only kind * and no lambda-abstraction at the level of types, but we allow quantification over proper types (of kind *).

F2 is our System F;

Thanks.

Answer 1

Why can System F1 have kind *, but no universal types, i.e. quantification ∀?

Because "System F1 has types of kind *" does not mean "any types which have kind * in some other system (e.g. universal types) are allowed in F1".