A type is uninterpreted when it has not been given any interpretation as a sort known to the underlying logic.

In other words: as far as the logic knows, an individual of that type exists but has no other properties than those the user declares.

Many types in Ivy programs are uninterpreted.

Functions over uninterpreted types are called uninterpreted functions. Satisfiability of uninterpreted functions is decidable.