Editing First-order logic (section)

===Expressiveness===
The [[Löwenheim–Skolem theorem]] shows that if a first-order theory has any infinite model, then it has infinite models of every cardinality. In particular, no first-order theory with an infinite model can be [[Morley's categoricity theorem|categorical]]. Thus, there is no first-order theory whose only model has the set of natural numbers as its domain, or whose only model has the set of real numbers as its domain.  Many extensions of first-order logic, including infinitary logics and higher-order logics, are more expressive in the sense that they do permit categorical axiomatizations of the natural numbers or real numbers{{clarification needed|date=January 2023|reason=Article should clarify syntactic-semantic distinction here, e.g. second-order logic can be interpreted as a many-sorted first-order logic, so syntactically it could be argued that it's not more expressive, and it admits categorical axiomatizations only using full semantics, but using Henkin semantics it is a conservative extension of the typical semantics for first-order logic. So really the article needs to clarify whether it is discussing FOL exclusively as a syntactic system, or as a syntactic and semantic system, and in either case clarify in which senses "extensions" of first-order logic are being assumed to extend it (i.e. syntactically only or also semantically).}}. This expressiveness comes at a metalogical cost, however: by [[Lindström's theorem]], the compactness theorem and the downward Löwenheim–Skolem theorem cannot hold in any logic stronger than first-order.