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.
Condensation, GCH, and Diamond in L: Examples and Counterexamples
1 · Prerequisites
- Cardinal Arithmetic, Cofinality and the Alephs
- Club, Stationary Sets, and Pressing Down
- Condensation, GCH, and Diamond in L
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Deduction, Soundness, Completeness, and Compactness
- Finite Counting, Factorials and Binomial Coefficients
- Formal Set-Theoretic Syntax, Structures, and Satisfaction
- Foundations of the Real Numbers for Analysis
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Reflection, Absoluteness, and Elementary Submodels
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- Set-Theoretic Trees, Delta Systems, and Diamond
- Suprema and Infima
- The Constructible Hierarchy and Inner Models
- The ZFC Axioms and the Basic Set Constructions
- Well-Founded Relations, Rank, and the Cumulative Hierarchy
2 · Summary
The real example calculates the countable collapse of the hull generated by and obtains an explicit countable stage containing a constructible real. The diamond example concerns the precise antichain guessed at a sealing stage of the Suslin-tree construction. It proves its conditional stage claim directly and computes a binary-tree instance with eventually-zero branches; the separate theorem supplies global diamond existence.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Condensation bounds a constructible real
Example
If and , the hull-and-collapse proof produces a countable ordinal such that .
Facts & Assumptions
Given: Ambient ZF and a constructible real .
Canonical L-hulls are elementary and small makes the hull of the countable seed elementary and countably infinite.
Condensation for constructible levels identifies the transitive collapse of that hull with .
What the collapse fixes fixes every transitive subset of the hull pointwise and computes collapsed ordinals as order types.
Constructible subsets appear before successor cardinals gives the general conclusion ; the calculation below exhibits its sharper witness .
Verification
Choose a nonzero limit with and form . F1 gives and a bijection between and . In particular every natural number belongs to , not merely the set as one element.
Collapse by to using F2. Since is transitive, F3 fixes every natural number. The map is an isomorphism onto the transitive set : if , surjectivity gives with , and relation reflection gives ; conversely implies . Since and there, . Hence . This includes the empty real.
The collapse is a bijection, so is countable. Since , the ordinal is countable and therefore . Thus the hull calculation proves the claimed bound and, consistently with F4, yields . No ambient Choice is used.
Diamond sealing a maximal antichain in L
Example
Work internally in , and consider a stage of the diamond tree construction with a supplied guessing sequence. Let be a nonzero countable limit ordinal, let be the preceding normal tree with countable levels, and suppose the stage guess is a maximal antichain of this partial tree. Choosing the new level above a covering family of cofinal branches meeting seals : every new node, and every node at a later level of a continuation preserving predecessor sets, extends a member of . In particular a global antichain whose restriction is cannot acquire members at heights at least .
A concrete local instance has , ordered by proper extension, and . The new tops may be indexed by the eventually-zero binary sequences. This illustrates the local sealing operation; it does not claim that this finite-branching tree is the exact consecutively coded tree used by the published global construction.
Facts & Assumptions
Given: The stated stage and correct maximal-antichain guess. Assume AC for assembling the countably many earlier countable levels; when working internally in this is supplied by F5. The local operation after a countable partial tree is supplied is choice-free.
Diamond constructs a normal splitting Suslin tree proves in ZFC that a diamond sequence constructs a normal splitting Suslin tree with underlying set and countably infinite positive levels.
Seal a maximal antichain at a countable limit level supplies a countable covering family of distinct cofinal branches meeting the given maximal antichain, and proves normality after adjoining their tops, without Choice.
Tree predecessors and compatibility supplies the unique predecessor at every smaller height and comparability below a common extension.
Countable unions of at most countable sets, assuming makes a countable union of countable levels countable under countable choice.
The constructible universe satisfies AC proves AC internally in from ambient ZF.
The Axiom of Choice specifies the assumed choice function principle; it supplies the countable choice used in F4.
Verification
Since is countable, the family of earlier countable levels is a countable family. F4 and A1 make countable. It is nonempty by its root, so the empty antichain is not maximal: the root could be adjoined. F2 applies to the given normal tree and nonempty maximal antichain , yielding countably many distinct covering branches and a top for each. Its predecessor set is exactly , and some belongs to , hence . No family of chosen is needed for this existential assertion.
For the concrete instance, height consists of the binary strings of length . The code injects all finite strings into the positive integers, so the partial tree is countable without Choice. Its root is the empty string, every string extends to every larger finite height by appending zeros, and every string has its two immediate successors. The two strings in are incomparable; every nonempty string extends exactly one of them and the root precedes both. Thus is maximal. There is no positive limit height below requiring a further predecessor-uniqueness check.
For every finite binary string put and view this infinite sequence as the branch of all its finite initial segments. It is cofinal, contains , and meets in exactly its length-one initial segment. The distinct are precisely the eventually-zero binary sequences. They form a countable set by taking, for each sequence, the least numerical code of a string producing it; this is an injection into . They form an infinite set because the sequences with a unique at position are distinct for distinct . Adjoin a separate top for each distinct sequence. Its predecessors have order type ; distinct tops have distinct predecessor sets. Every old string lies below a top, and the countable new level preserves normality and all old splitting. This computes the branch family directly, including empty, which gives .
In either construction, a node at a later height has a unique predecessor at height by F3. Since is one of the added tops, there is with , so . A node at height already has this property. If a global antichain restricts below to and contained such a , it would contain the distinct comparable members , which is impossible. Thus has no members at or above . This is the failed-antichain-extension conclusion that sealing enforces.
The singleton root antichain is the degenerate maximal guess handled by the same argument: every cofinal branch contains the root. Heights zero and successor heights are excluded from this limit-stage operation. Choice entered only when obtaining countability of the unspecified family of earlier levels; the binary calculation and F2's least-index branch construction use no Choice. Inside , F5 supplies the A1 hypothesis. The example assumes the particular correct stage guess, so it does not require an existence proof for a diamond sequence from ; F1 is the separate global theorem that combines such guesses with the stage construction. [F1, F2, F5, A1, step 1.1, step 3.1] QED.