  Universality is one of the most important ideas in computability theory.
There are various criteria of simplicity for universal Turing machines.
Probably the most popular one is to count the number of states/symbols. This
criterion is more complex than it may appear at a first glance. In this note we
review recent results in Algorithmic Information Theory and propose three new
criteria of simplicity for universal prefix-free Turing machines. These
criteria refer to the possibility of proving various natural properties of such
a machine (its universality, for example) in a formal theory, PA or ZFC. In all
cases some, but not all, machines are simple.
