Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-09
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 M be an infinite structure for a set signature L. For every infinite cardinal κmax(M,L), M 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 M, the stated cardinal inequality, and AC.

[F1]

A model of the elementary diagram of M induces an elementary embedding of M, and this can be transported to literal inclusion. (Models of the elementary diagram yield elementary embeddings)

[F2]

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)

[F3]

An infinite structure in a language of size at most infinite λ has an elementary substructure of size λ when λM. (Downward Löwenheim–Skolem with parameters)

[A1]

AC is assumed, including for the general-language theorem and hulls. (The Axiom of Choice)

Proof

1.1

Expand L by one diagram name for each element of M and by distinct fresh symbols dα for α<κ. Its size is at most κ by the two given bounds and F4. Let S be the elementary diagram together with all dαdβ for αβ<κ.

F1F4
2.1

A finite subset of S mentions finitely many of the d symbols. The infinitude of M permits interpreting them distinctly: after choosing fewer than their finite number of distinct elements, another exists because M is not that finite set. Interpret diagram names by their named elements, and all other d symbols by one fixed element of M. This expansion satisfies the finite subset, because all its diagram sentences hold and all its listed inequalities hold. No requirement says the new d values avoid the old named elements.

F1step 1.1
3.1

F2 under A1 supplies NS of size at most κ. The map αdαN is injective by the inequalities, so Nκ and therefore N=κ. F1 gives an elementary embedding of M into the L-reduct of N and its transported copy as a literal elementary extension. The transport is a bijection, so size remains κ.

F1F2A1step 1.1step 2.1
4.1

For an infinite model M of a countable-language theory and any infinite cardinal λ, if λM apply step 3.1 with κ=λ; the language bound holds because L0λ. If λM, apply F3 with empty parameter set. An elementary extension or substructure satisfies the same sentences as M, hence is a model of the theory. Equality of cardinals permits M itself. This proves every infinite target size.

F3A1step 3.1

Depends on

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