Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Shelah's CH-length homogeneous sweet construction

Statement

Assume ZFC and CH, explicitly P(ω)=1. There is a continuous increasing chain of sweetness models (Pα,Dα,Enα)α<ω1. Put Bα=BA(Pα) and P=α<ω1Pα. Then the Bα form an increasing chain of complete Boolean algebras of size at most ω1, and the final completion B=BA(P)=α<ω1Bα is ccc and has size ω1, such that (i) every complete isomorphism between countably generated complete subalgebras of B extends to an automorphism of B, and (ii) every task scheduled by the construction is met: every free-amalgamation task whose data appear at a stage is answered at a later stage, and above every stage there is a later quotient with the canonical UM presentation (equivalently, its Boolean completion is identified with the quotient completion). This is Shelah's continuous sweet construction (Main Lemma 7.14(b),(d)); it is not identified with an ordinary finite-support iteration.

Facts & Assumptions

Given: ZFC and CH in the form P(ω)=1.

[F1]

The Axiom of Choice: well-orderings of the sets of task codes used in the set-length recursion. No global choice principle is assumed.

[F3]

Sweet amalgamation extends partial Boolean isomorphisms: every complete isomorphism between countably generated complete subalgebras of a sweet algebra extends to an automorphism after one extension step.

[F4]

Shelah amalgamation preserves sweetness and Composition with universal-meagre forcing preserves sweetness: the named amalgam and canonical UM composition give sweetness models extending the fixed old model.

[F5]

Continuous countable unions of sweetness models remain sweet: sweet models are preserved at limits of countable cofinality, with every earlier stage complete in the union.

[F6]

Sweet forcings are countable unions of directed sets and ccc: every sweet stage is ccc. Under CH, (ω1)0=(20)0=20=ω1; hence a ccc forcing of size at most ω1 has a Boolean completion of size at most ω1, because each completion element is the join of a countable maximal antichain from a dense copy of the forcing.

[F7]

Shelah's Main Lemma 7.14 supplies the final-union clauses that are not consequences of [F5]: for the constructed chain, if P=α<ω1Pα and B=BA(P), then B is ccc and B=α<ω1BA(Pα). It also states the union-level automorphism-extension and free-amalgamation clauses and identifies arbitrarily late quotients with the canonical UM forcing in the relevant intermediate extension. [source]

[F8]

Shelah's Claim 7.13 permits arbitrary complete subalgebras, not only countably generated ones: any isomorphism between two complete subalgebras of a sweet completion extends to an automorphism after an extension of the fixed sweetness model. This stronger source interface is used when continuing a previously extended map whose domain is an entire stage completion. [source]

Proof

1.1

Well-order all countable task codes: complete isomorphisms between countably generated complete subalgebras, pairs C0C1 of such subalgebras requiring a free copy over C0, and canonical UM-extension requests. Under CH the set of countable sequences from ω1 has size ω1 by [F2], so use ω1 bookkeeping that repeats every task cofinally often. A homogeneity task retains its last partial extension; later occurrences extend that coherent map over the then-current stage.

F1F2
1.2

Begin with the trivial sweetness model. At a successor, perform the named task only after all of its data have appeared. For an isomorphism task use [F8] to extend the current coherent map over the whole current completion. For C0C1, first use the named amalgam [F4] to create a second canonical copy of C1 freely amalgamated with the first over C0, then use [F3] to extend the copy isomorphism to the required automorphism. For a UM task use the fixed-model composition in [F4]. Every successor is therefore an extension of sweetness models.

F3F4F8
1.3

At a nonzero limit λ<ω1, put Pλ=α<λPα,Dλ=α<λDα,Enλ=α<λEnα. Since every such limit is countable and has countable cofinality, [F5] makes this a sweetness model extending every earlier stage. Only after forming this direct union forcing set Bλ=BA(Pλ). In general Bλ is not asserted to equal α<λBα; completing the direct union is a separate operation.

F5
2.1

The recursion is well defined, every Pα is sweet, and each earlier Pα is complete in every later Pβ. Consequently the induced maps make Bα a complete subalgebra of Bβ. The word "continuous" refers to the forcing/sweetness-model chain of step 1.3, not to an unproved direct union of complete algebras.

F3F4F5step 1.2step 1.3
2.2

Inductively keep Pαω1: each successor construction is made from at most ω1 conditions, and each limit below ω1 is a countable union. Every Pα is ccc by [F6]. A completion element is the join of a maximal antichain from the dense image of Pα, that antichain is countable, and [F6] gives at most (ω1)0=ω1 such codes. Hence Bαω1 at every stage without treating the construction as a finite-support iteration.

F2F6step 1.2step 1.3
2.3

Every countable task has a bounded set of birth stages, hence is active at all sufficiently late occurrences of its code. Repeated occurrences of an isomorphism task form a coherent cofinal chain of extensions. A free-amalgamation requirement, once realised, remains realised in all later complete extensions. UM requests occur unboundedly often, so arbitrarily late successor quotients are the canonical UM forcing.

F1F2F3F4step 1.1step 1.2
3.1

Let P=α<ω1Pα and put B=BA(P). This is an ω1-length union, so [F5] does not apply. Instead the special final-union conclusion recorded in [F7] proves the identity B=α<ω1BA(Pα) and proves that B is ccc. The identity and step 2.2 give Bω1. The unboundedly many nontrivial UM quotients make the chain strictly increase unboundedly often, so Bω1. Hence B=ω1.

F4F7step 2.2step 2.3
4.1

Let f:AA be a complete isomorphism between countably generated complete subalgebras of B. By the final identity in step 3.1, the countable generating data occur at a bounded stage. Its repeated bookkeeping thread extends coherently over unboundedly many later stages, and its union is an automorphism of B extending f. This is clause (b) of [F7], not the unsupported extension of a single-stage automorphism. Clause (c) gives the final free-amalgamation property, and clause (d) gives the arbitrarily late UM quotients.

F2F3F7step 1.1step 2.3step 3.1
5.1

Steps 1.1--2.3 construct the continuous chain of sweetness models; step 3.1 performs the distinct final Boolean-completion argument; and step 4.1 gives the union-level homogeneity, free-amalgamation and UM clauses. This proves the Statement.

step 2.3step 3.1step 4.1

Depends on

Used by

Dependency tree · two levels

38 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