If a pure type system has a terminating proof language, can we have
Type : Type at the logic level without causing paradoxes (i.e., without causing
∀ (x : *) -> x to be inhabited)?
Suppose we take a pure type theory such as the Calculus of Constructions, restrict functions to be affine (at most 1 variable uses) and add constructs for stratified duplications - see here for details. That language - which we could call EACC (Elementary Affine Calculus of Constructions) has a normalizing untyped fragment. That is, the reduction of any term - even ill-typed ones - is guaranteed to terminate due to the reduction rules (and, in particular, the restriction that duplicated terms can not change their levels).