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.
Universal pcf sequences have strong increase and exact bounds
Statement
Assume AC. Let be a nonempty progressive set of infinite regular cardinals, and . Let be the least ordinal with . There is a universally cofinal -sequence with modulo for every infinite regular , and an exact upper bound with a limit ordinal for every .
Either , in which case , and a principal-coordinate construction suffices, or is a singular limit cardinal less than . The latter case has , so the general exact-bound theorem applies. No finite-support case is inferred from that theorem.
Facts & Assumptions
Given: AC, , , as in the statement. The property means every unbounded subset of the sequence's indices contains a strongly increasing subsequence of order type .
Product ultrafilter cofinalities are infinite regular cardinals at least the smallest coordinate; restriction to an ultrafilter support preserves them; finite PCF equals the coordinate set (Progressive products and true cofinality transfers).
is proper, and exactly when ; its subset criterion tests all supported ultrafilters (Pcf cofinality ideals and cutoff conventions).
The product modulo is -directed and every cofinality- ultrafilter avoids (Pcf ideal directedness and ultrafilter cofinality cutoffs).
A universal -sequence exists (Progressive pcf has universally cofinal sequences).
Directedness gives one dominating strict chain with for every uncountable regular with and ; its projection and exact-bound conclusions apply with their stated cardinal inequalities (Directed progressive products have club continuous chains).
Exact bounds are least bounds and are unique modulo the ideal; the general projection theorem yields positive limit representatives (Bounding projections produce an exact upper bound with large coordinate cofinalities).
Smaller subsets of a regular cardinal are bounded; cofinality of a limit ordinal is regular (; and ; for a limit ordinal the value is an infinite cardinal with , so it is regular; and every cofinal subset of has cardinality at least , a value that is attained, (c)–(d)).
Successor cardinals are regular under AC ( is regular in ZF; assuming the Axiom of Choice every successor aleph is regular; , so is singular, and under choice it is the least singular infinite cardinal, (b)).
A specified rule recurses on an ordinal (Transfinite recursion).
AC supplies choices from nonempty sets (The Axiom of Choice).
Proof
Choose a cofinality- ultrafilter , which exists by the definition of . Put . If , its complement belongs to : a maximal proper filter omitting has a member disjoint from , since otherwise adjoining would generate a proper larger filter. On that complement every coordinate exceeds ; F1 would give product cofinality greater than , a contradiction. Thus , and F3 implies . The least positive initial segment therefore exists with . Also by F1 and progressiveness. If , minimality gives , and positivity of its union with forces and . F2 gives , while gives . Thus .
In this successor case let . Then . No member of contains a coordinate , by its singleton subset and F2; hence . Define on and off . Since off , these are product functions. For , everywhere off , so the whole sequence is strongly increasing with constant exceptional set . Every unbounded has an increasing sequence of indices of order type any infinite : recursively take its least member above previous indices, using regularity from F1 and boundedness from F7 at stages below , and F9 for the recursion. Restriction proves each required . Every cofinality- ultrafilter contains : it avoids by F3 and cannot concentrate on the coordinates greater than by F1; the finite intersection rule forces that singleton. At that coordinate the values enumerate , so the sequence is universal.
Otherwise is a limit ordinal and is unbounded in . Indeed, a bound would give . An unbounded set of infinite cardinals has a cardinal supremum: for each some cardinal satisfies , ruling out any bijection of with a smaller ordinal by restriction to . Thus is a limit cardinal. Also by F7 and progressiveness. It is singular; since is regular and , it follows that . The support is infinite, and, as is a limit cardinal above , . For every infinite regular its double successor and the ordinal are below . Minimality therefore gives .
In the successor case of step 2.1, set on and off . These are positive limit ordinals and . Every . Given , its failure set is a subset of , so for every . There are at most such values, so F7 bounds their successors by some ; if their supremum is zero, take . Then off , proving exactness. This proves the complete conclusion in the successor case. In particular it covers finite : the finitely many initial segments change only at successors, so a least positive one cannot first occur at a limit.
In the limit case of step 2.2, AC in A1 supplies the choice hypothesis of the following two existence results. Apply F4 to obtain a universal sequence , and F5 using F3's directedness to obtain a strict chain with everywhere. For every uncountable regular , step 2.2 checks both eligibility inequalities and the small-coordinate condition, so this one chain has . It also has : because is a limit cardinal greater than the infinite cardinal , and is regular by F8; restrict each strong subsequence to its first terms. If has cofinality , F3 transfers every comparison to . Given a product function , universality of supplies with , proving universality of .
Put . By F8 is regular and uncountable; step 2.2 gives and makes it eligible in F5. Thus F5's projection and exact-bound clauses supply an exact bound with positive limit values. Let , a pointwise bound for every product function. Leastness in F6 gives . Set ; it is positive and limit-valued, lies below everywhere, and differs from only on the small set . Consequently each upper-bound comparison and each comparison is unchanged from , so exactness is preserved. Together with the successor-case construction in step 3.1 and universality in step 3.2 this proves all the assertions. QED.
Depends on
- Progressive products and true cofinality transfers
- Pcf cofinality ideals and cutoff conventions
- Directed progressive products have club continuous chains
- Pcf ideal directedness and ultrafilter cofinality cutoffs
- Progressive pcf has universally cofinal sequences
- Strongly increasing subsequences force a bounding projection
- Bounding projections produce an exact upper bound with large coordinate cofinalities
- The Axiom of Choice
- $\operatorname{cf}(\alpha) \le \alpha$; $\operatorname{cf}(0) = 0$ and $\operatorname{cf}(\alpha + 1) = 1$; for a limit ordinal $\lambda$ the value $\operatorname{cf}(\lambda)$ is an infinite cardinal with $\operatorname{cf}(\operatorname{cf}(\lambda)) = \operatorname{cf}(\lambda)$, so it is regular; and every cofinal subset of $\lambda$ has cardinality at least $\operatorname{cf}(\lambda)$, a value that is attained
- $\aleph_0$ is regular in ZF; assuming the Axiom of Choice every successor aleph $\aleph_{\alpha+1}$ is regular; $\operatorname{cf}(\aleph_\omega) = \aleph_0$, so $\aleph_\omega$ is singular, and under choice it is the least singular infinite cardinal
- Transfinite recursion
- Commutativity, associativity, distributivity and monotonicity of $\oplus$ and $\otimes$, the unit laws, the two exponent laws, and $\kappa \le \lambda$ if and only if $\kappa$ injects into $\lambda$
- 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
49 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
- Abraham and Magidor, Cardinal Arithmetic, Lemma 4.6 p. 40, Theorem 4.8 p. 41 and Exercise 2.1 p. 11 (standard reference, not scraped)