Types are about rigorously constructing mathematical abstractions from primitive types defined up to a unique isomorphism. In fact, types have become the prim

Types are about rigorously constructing mathematical abstractions from primitive types defined up to a unique isomorphism. In fact, types have become the primary foundation of Computer Science. Russell introduced the crucial concept of the order of a proposition to block his famous paradox as follows: Without orders on propositions, the paradoxical predicate I’mNotSelfApplicable (such that I’mNotSelfApplicable[I’mNotSelfApplicable]⇔¬I’mNotSelfApplicable[I’mNotSelfApplicable]) could be constructed using the following recursive definition: I’mNotSelfApplicable:Predicate<i>≡¬I’mNotSelfApplicable[I’mNotSelfApplicable] Since I’mNotSelfApplicable is a predicate variable in the definition, ¬I’mNotSelfApplicable[I’mNotSelfApplicable]:Predicate<i+1>. Consequently, I’mNotSelfApplicable:Predicate<i>⇒I’mNotSelfApplicable:Predicate<i+1> which is a contradiction meaning that I'mNotSelfApplicable does not exist. See video: https://www.youtube.com/watch?v=AJP1VL7shiI https://www.youtube.com/watch?v=AJP1VL7shiI