In first-order classical logic, the theorem due to logician Per Lindström (1936–2009) that any extension to first-order classical logic that strengthens its expressivity in a certain way must fail to enjoy either the downward Löwenheim-Skolem property or the compactness property. This type of strengthening can be explained by noting that there are limitations to the types of models that classical logic can distinguish. For example, there is no sentence holding of all and only finite models of a theory , i.e., finiteness is not a first-order property. But one can define generalized quantifiers capable of distinguishing between finite and infinite models and add them to the apparatus of first-order logic. For example, let be defined so that:
Then should hold in precisely those models whose domains are finite. Hence, the logic enriching first-order classical logic with is capable of finer discrimination between classes of models than classical logic alone, i.e., it strengthens classical logic. Lindström’s theorem then states that this deductive system must fail to enjoy natural properties, i.e., downward Löwenheim-Skolem or compactness must fail.