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.
Size and rank bounds below an inaccessible
Statement
In ZFC let kappa be inaccessible. Then for every , every has size less than kappa, and every set of fewer than kappa elements of belongs to . For cardinals , , with . The strong-limit cardinals below kappa contain a club subset of kappa.
Facts & Assumptions
Given: ZFC. Supplied the cardinal-square proof and small-union estimate locally, identifying AC for simultaneous injections; then proved the rank, exponent and strong-limit club assertions with all zero and limit cases.
Inaccessible and Mahlo cardinals: Kappa is regular uncountable and strong limit; club uses closure at nonzero limit accumulation points.
The cumulative hierarchy: V grows by power sets at successors and unions at limits.
Membership rank under Foundation: Ranks are suprema of member ranks plus one, and rank below kappa means membership in V_kappa.
The Axiom of Choice: AC permits well-ordering sets, cardinal comparisons and simultaneous selection of injections for a set family.
Proof
We first justify the small-union estimate used here. For every infinite cardinal theta, : by induction on infinite cardinals order pairs by their maximum coordinate, then lexicographically. An initial segment ending at coordinates below has size at most , by the induction hypothesis at (or by finite counting). This well-order has type at most theta, since otherwise its first theta elements would be a proper initial segment of size theta. The reverse bound uses the injection . Consequently for fewer than kappa sets of size below kappa, regularity bounds the set of their cardinalities and the index cardinal below a common infinite cardinal . Such an eta exists because a strong-limit cardinal is a limit cardinal: if kappa were the successor of eta, Cantor diagonalization would give . AC selects injections of the sets into eta, embedding their disjoint union into . Its size is therefore below kappa.
Induct on . The empty V_0 is small. At a successor, by strong limit. At a nonzero limit alpha there are fewer than kappa earlier levels, so step 1.1 bounds their union below kappa. If , it is a subset of some earlier V level, hence has size below kappa.
If and , Replacement collects the ranks of its members; regularity bounds their supremum plus one below kappa. Thus the supremum of their ranks plus one, namely rank(Y), is below kappa, so . For empty Y the rank is zero.
For , graphs inject the set of functions into . Step 1.1 bounds the product size by some infinite , so . This also covers finite cardinals; more explicitly , for positive nu and .
Let C be the set of infinite strong-limit cardinals below kappa. It is unbounded: above a given bound start with an infinite cardinal larger than it, put and by regularity. Cantor diagonalization makes the sequence strictly increasing. Its supremum is a cardinal: a bijection of delta with a smaller ordinal would inject a larger theta_n into a smaller cardinal. For every cardinal some theta_n exceeds mu, hence . Thus delta is in C. If delta<kappa is a nonzero limit accumulation point of C, it is similarly a cardinal, and for every cardinal mu<delta there is above mu, giving . Thus delta is in C, proving closure. No enumeration choices are needed in this last uniquely defined iteration.
Depends on
Used by
- The least inaccessible is not Mahlo Example
- Henkin truth trees for infinitary compactness Lemma
- The critical point of a measurable ultrapower Lemma
- The inaccessible random algebra preserves cardinals and makes the continuum kappa Lemma
- Tree and partition characterizations at an inaccessible Lemma
- An inaccessible rank segment models ZFC Theorem
- Existence of a Laver function at a supercompact Theorem
- Supercompact preparation interface Theorem
- Weak compactness implies stationary reflection and Mahloness Theorem
Dependency tree · two levels
14 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
- Marks Theorem 18.16 p.79, prerequisite size estimate; Monk Chapter 17 pp.356–363 (standard reference, not scraped)