How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Upward Löwenheim–Skolem, including elementary extensions
Statement
In ZFC, let be an infinite structure for a set signature . For every infinite cardinal , has an elementary extension of size exactly , with literal inclusion after transport. Consequently a countable-language theory with an infinite model has models in every infinite cardinality.
Facts & Assumptions
Given: The infinite structure , the stated cardinal inequality, and AC.
A model of the elementary diagram of induces an elementary embedding of , and this can be transported to literal inclusion. (Models of the elementary diagram yield elementary embeddings)
Under AC, a finitely satisfiable theory in a language of size at most infinite has a model of size at most . (Well-ordered language completeness with a size bound)
An infinite structure in a language of size at most infinite has an elementary substructure of size when . (Downward Löwenheim–Skolem with parameters)
The sum of finitely many sets of size at most infinite has size at most . (Absorption: for cardinals with infinite and , , and when )
AC is assumed, including for the general-language theorem and hulls. (The Axiom of Choice)
Proof
Expand by one diagram name for each element of and by distinct fresh symbols for . Its size is at most by the two given bounds and F4. Let be the elementary diagram together with all for .
A finite subset of mentions finitely many of the symbols. The infinitude of permits interpreting them distinctly: after choosing fewer than their finite number of distinct elements, another exists because is not that finite set. Interpret diagram names by their named elements, and all other symbols by one fixed element of . This expansion satisfies the finite subset, because all its diagram sentences hold and all its listed inequalities hold. No requirement says the new values avoid the old named elements.
F2 under A1 supplies of size at most . The map is injective by the inequalities, so and therefore . F1 gives an elementary embedding of into the -reduct of and its transported copy as a literal elementary extension. The transport is a bijection, so size remains .
For an infinite model of a countable-language theory and any infinite cardinal , if apply step 3.1 with ; the language bound holds because . If , apply F3 with empty parameter set. An elementary extension or substructure satisfies the same sentences as , hence is a model of the theory. Equality of cardinals permits itself. This proves every infinite target size.
Depends on
- Models of the elementary diagram yield elementary embeddings
- Well-ordered language completeness with a size bound
- Downward Löwenheim–Skolem with parameters
- The Axiom of Choice
- Absorption: for cardinals $\kappa, \lambda$ with $\kappa$ infinite and $\lambda \le \kappa$, $\kappa \oplus \lambda = \kappa$, and $\kappa \otimes \lambda = \kappa$ when $\lambda \ne 0$
Used by
Dependency tree · two levels
35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Weiss–D’Mello, Theorem 6 proof p21, Theorem 9(2) and Exercise 15 p25; full elementary-diagram extension argument supplied locally. (standard reference, not scraped)