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.
