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.
The simple dichotomy for omega-one-generated ideals
Definition
Work in ZFC. Let be uncountable. An ideal of countable subsets of is a family that contains every finite subset of and is closed under taking subsets and finite unions. For , write when is finite.
The ideal is generated modulo finite by members if there are for such that
for every countable . This is equivalent to having an explicit family closed under finite unions: replace the displayed family by the sets for finite . The resulting family has cardinality at most in ZFC; if an -indexed family is desired, repeat members to pad the enumeration. Membership in then means almost containment in one member of that family. No increasing sequence is asserted: an ideal need not contain the union of countably many of its members.
For :
- is inside when ;
- is outside, or orthogonal to, when for every .
Equivalently, is outside exactly when its intersection with every chosen generator is finite: one direction uses that generators belong to the ideal; the other uses the finite-union and finite-error formula above. Also then consists only of finite sets.
The simple dichotomy for -generated ideals is the assertion that for every such and , either some uncountable is inside , or some uncountable is outside . “Either” is inclusive: different witnesses can in principle satisfy the two clauses. One uncountable cannot satisfy both in ZFC, because AC gives a countably infinite ; inside gives , while outside says is finite. This extraction of is the only choice used in the definitional discussion. Empty and finite are allowed by the two local predicates but are not witnesses to the dichotomy.
Depends on
Used by
Dependency tree · two levels
16 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, Three applications of ideal dichotomy, slides 2–4 (standard reference, not scraped)
- Abraham, Lecture notes on the P-ideal dichotomy, Definitions preceding Theorems 1.3–1.4 (standard reference, not scraped)