Simplicity via provability for universal prefix-free Turing machines

Universality, provability and simplicity are key notions 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 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, Peano arithmetic or Zermelo–Fraenkel set theory. In all cases some, but not all, machines are simple.