Definition of the notion of a model in first-order logic occurs too late

[beastaugh]

The definition of a model of a set of sentences is given in the section on expressing properties of structures (§8.2 in the sample project). A least in the standard ordering, this occurs after the definition of entailment in the section on semantic notions (§7.7 in the sample project). This is problematic because notion of a model of a set of sentences is already used, albeit only symbolically without mention of the term 'model', in the definition of entailment (as well as in the subsequent definition of satisfiability).

If we don't want to define the term 'model' until the section on expressing properties of structures, I think we should at least define the notion of satisfaction of a set of sentences by a structure earlier, because the overloading of the double-turnstile symbol can be confusing to students, especially if they haven't covered the material on propositional logic before getting into first-order logic. The most natural place would seem to be immediately after the definition of satisfaction for individual sentences, in the section on variable assignments (§7.5 in the sample project). The definitions of entailment and satisfiability, which occur in the subsequent section on semantic notions, would then be comprehensible in terms of this definition.

(If this makes sense, I'm happy to make the change and submit a pull request.)