  There is a useful characterization of the relation ≤ that applies when it is restricted to the type of theories that we will be considering. To describe this we need a few more notions. A theory T is reflexive provided it proves the consistency of each of its finite fragments, it is Σ01-complete provided it proves each true Σ01-statement, and it is Σ01-sound provided it does not prove a false Σ01-statement. Let ‘T1 ⊆Π01 T2’ be shorthand for the statement that all Π01-sentences provable in T1 are provable in T2. The following characterization of interpretability is central to the theory of interpretability: If T1 is reflexive and Σ01-complete, then 