Löwenheim–Skolem theorem

The theorem says that a first-order theory with an infinite model has models of every infinite cardinality at least the size of its language. In a countable language, it therefore has a countable model.

Downward Löwenheim–Skolem theorem: A theorem giving elementary substructures of bounded cardinality inside sufficiently large structures. It produces small models, including countable ones for structures in countable languages.
Skolem's paradox: The apparent tension between set theory's uncountable models and its countable models containing sets described as uncountable. A countable model of set theory can contain an internal bijection that it cannot recognize externally.
First-order theory: A set of sentences in first-order logic, interpreted as constraints on mathematical structures. The theorem applies to theories whose models satisfy those sentences.
Leopold Löwenheim: A German mathematician whose 1915 result established an early countability theorem for first-order logic. His result supplied the theorem's original downward direction.
Upward Löwenheim–Skolem theorem: A theorem stating that an infinite first-order structure has elementary extensions of every larger infinite cardinality. It accounts for models larger than a given infinite model.
Categorical theory: A theory is categorical in a cardinality when all its models of that size are isomorphic. The theorem rules out categoricity across all infinite cardinalities for theories with infinite models.
Structure (mathematical logic): A domain equipped with interpretations for the symbols of a formal language. Models are structures, and their domains determine their cardinalities.
Thoralf Skolem: A Norwegian mathematician who strengthened and clarified early results on countable models and set theory. His work generalized the countability result and exposed its set-theoretic consequences.
Elementary substructure: A substructure that agrees with its parent structure on every first-order formula with parameters from the substructure. Downward constructions preserve all first-order truths while shrinking the domain.
First-order logic: A formal logic whose quantifiers range over individual objects in a structure. The theorem's model-size flexibility is a characteristic limitation of first-order expression.

Linked from 9 pages