From Hofstadter's book GEB: In this case, we have an excellent prototype for the concept of isomorphism. There is a “lower level” of our isomorphism—t-that is, a mapping between the parts of the two structures: P <==> plus Q <==> equals - <==> one - - <==> two - - - <==> three etc. This symbol-word correspondence has a name: interpretation. Secondly, on a higher level, there is the correspondence between true statements and theorems. But—note carefully—this higher-level correspondence could not be perceived without the prior choice of an interpretation for the symbols. Thus it would be more accurate to describe it as a correspondence between true statements and interpreted theorems. In any case we have displayed a two-tiered correspondence, which is typical of all isomorphisms.