Pure type systems in general need not be, for example System U from Girard's paradox is not.
Τα αμιγή συστήματα τύπων σε γενικές γραμμές δεν χρειάζεται να είναι, όπως για παράδειγμα το U από το παράδοξο του Girard δεν είναι.