Bit patterns don't have to matter. There are languages like Haskell which have type-theoretic type systems and no bit patterns specified . There are also languages like C, which has non-type-theoretic type systems and lots of things to say about bits, and languages like ANS FORTH, which has no type system at all and could reinterpret bit patterns.
There are also languages which have features generally referred to as type systems, and which fit Pierce's definition, but which are not just not type-theoretic, but don't resemble any kind of system which discriminates values based on membership in a set. For example, Pony and Rust both have syntactic forms for adding memory semantics to values, and their type-checking routines check the memory semantics oblivious to the bits being stored. Pony additionally can check certain causality properties. Monte has auditors, which are syntactically-specified objects which enforce semantic properties of other objects by examining their ASTs .
In summary, "type system" means what Pierce says it means: there is syntax, the syntax describes abstract properties of the program, the properties can be checked by syntax-guided computation, and programs can be rejected as invalid if the check fails.
What do you mean by "type theoretic"? Once you have a formal system where your objects are divided into sorts and your syntactic expressions are constrained by those sorts such that expressions may be ill-formed when the sorts are mismatched (by some definition), then you have a type theory on your hands.
> the properties can be checked by syntax-guided computation
Not all type systems can be checked by computation (some are undecidable).
The reason for the infamous undefinedness of signed integer overflow is precisely that C tries to be agnostic about their encoding (which mostly comes down to two's complement vs sign bit).