Discuss extensions in the right place

[rzach]

0f8bdb6

Previously, the notions of extension and of stipulating an extension
were used in section 27.1, before the notion of extension was
introduced in section 27.2. This change defines an extension before
introducing the notion of an extensional language.

This is a stopgap. Probably a bigger change is ultimately called for
here: the notion of an extension and the sense in which FOL is an
extensional language should be explained before the symbolising
vs. translating discussion, not within that section.