TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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 basic Cohen model satisfies BPI and fails Choice

Statement

Let $M$ be a transitive model of ZFC, let $G$ be $M$ -generic for $Add (ω, ω)^{M}$ , and let $N = {H S}^{G}$ be the finite-support basic Cohen symmetric model. Then $N$ is a transitive model of

$Z F + B P I + \neg A C .$

Its symmetric set $A$ of coordinate Cohen reals is infinite and Dedekind-finite, and in particular is not well-orderable in $N$ .

Facts & Assumptions

Given: The ground, generic, and model in the Statement.

[F1]

The basic Cohen symmetric system defines $N$ and its coordinate set $A$ .

[F2]

Hereditarily symmetric interpretations form a transitive ZF model proves that $N$ is a transitive ZF model.

[F3]

Search-and-shift prime-ideal construction in the basic Cohen model proves inside this exact hereditarily symmetric presentation that every proper set filter extends to an ultrafilter and hence that BPI holds.

[F4]

The basic Cohen model fails well-orderability and AC proves that $A$ is infinite, Dedekind-finite, not well-orderable, and that AC fails in $N$ .

[F5]

The Boolean prime ideal principle and The Axiom of Choice fix the two object-theory assertions.

Proof

technique · composition of the symmetric-model, BPI, and failure-of-choice modules

1.1

F1 and F2 give a transitive model $N$ of every ZF axiom.

F1F2

2.1

F3 applies to the same $M$ , $G$ , finite-permutation group, normal filter, and class of hereditarily symmetric names, so $N$ satisfies the BPI assertion of F5. This route does not use the unsupported promotion of a parameter-definable maximal ideal in the Repický shortcut.

F3F5step 1.1

2.2

F4 applies to the same orbit set $A$ and shows internally that $A$ is infinite and Dedekind-finite. A well-order would enumerate its least unused elements and contradict Dedekind-finiteness, so $A$ is not well-orderable; by F5, AC would well-order it. Thus $N ⊨ \neg A C$ .

F4F5step 1.1

3.1

Combining steps 1.1, 2.1, and 2.2 gives $N ⊨ Z F + B P I + \neg A C$ . The ground-model AC used by the search-and-shift construction is a metatheoretic construction hypothesis and is not asserted in $N$ .

step 1.1step 2.1step 2.2∎

Depends on

Used by

Relative consistency of BPI without Choice over ZF Corollary
BPI well-orders every set False statement
The Halpern–Läuchli theorem and the basic Cohen BPI model Theorem

Dependency tree · two levels

22 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

J. D. Halpern and A. Lévy, The Boolean prime ideal theorem does not imply the axiom of choice, pp.83-134 (standard reference, not scraped)
Brian Ransom, On BPI in Symmetric Extensions Part 1, Theorem 3.10, Lemma 4.6, Theorem 4.9, and Theorem 5.27–Corollary 5.28 (standard reference, not scraped)