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.
https://github.com/rzach/forallx-yyc/pull/7/commits/0f8bdb6240cea7cd20eafc59cd10e6d3af68fb99
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.