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.

Pincus transfer for BPI and injectively boundable conjunctions

Statement

Let a ZFA permutation model be given, and let $T_{1}, \dots, T_{k}$ be finitely many certified atom-blind boundable sentences. Then the conjunction $T_{1} \land \dots \land T_{k}$ transfers to a model of $Z F$ . Moreover, if the permutation model satisfies BPI (The Boolean prime ideal principle), BPI may be conjoined with the certified sentences and transferred with them. If the model satisfies both BPI and Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), the simultaneous conjunction $B P I \land {A C}_{ω}$ may be transferred with the certified sentences. This item does not assert an ${A C}_{ω}$ -only exceptional clause. No arbitrary ZFA truth, no full Choice, and no uncertified sentence is transferred.

Facts & Assumptions

Given: A permutation model of ZFA with atom set $A$ ; finitely many certified atom-blind boundable sentences with their absolute rank bounds.

[F1]

A boundable statement is injectively boundable (Pincus, cited in Tachtsis as Fact 5.4). Thus an atom-blind boundable statement carrying the typed certificate of Jech–Sochor transfer for certified atom-blind boundable sentences has the preservation data needed by the Pincus theorem (Boundable sentences over an atom set).

[F2]

Pincus's transfer theorem admits BPI as a named exceptional conjunct alongside a finite conjunction of injectively boundable statements. Tachtsis Theorem 5.5 records the stronger simultaneous $B P I \land {A C}_{ω}$ form. It does not state an ${A C}_{ω}$ -only exceptional clause, so none is used here. This is direct source input, not an inference from the orientation-only remark Pincus transfer interfaces and preservation limits (The Boolean prime ideal principle, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1

Fix the finite list $T_{1}, \dots, T_{k}$ of certified sentences. By [F1], each $T_{j}$ is injectively boundable; the finite conjunction retains the finitely many certificates and absolute bounds.

givenF1

2.1

Let $Ω$ be the conjunction of the $T_{j}$ , together with BPI when that exceptional clause is to be used, and together with both BPI and ${A C}_{ω}$ when the simultaneous exceptional clause is to be used. No other truth of the permutation model is included in $Ω$ , and ${A C}_{ω}$ is never adjoined here without BPI.

step 1.1givenF2

3.1

Apply the corresponding Pincus theorem in [F2] to $Ω$ . It produces an atom-free model of ZF satisfying every injectively boundable conjunct and the named exceptional principle or principles. In particular, omitting the exceptional clauses transfers the finite conjunction alone, adjoining BPI transfers BPI with it, and adjoining the simultaneous $B P I \land {A C}_{ω}$ clause transfers both principles with it.

step 1.1step 2.1F2

4.1

Step 3.1 is exactly the transfer asserted in the Statement. BPI and the simultaneous $B P I \land {A C}_{ω}$ conjunction enter only through [F2]'s exceptional clauses and are not relabelled as injectively boundable; the typed certificates restrict all other transferred content to the named $T_{j}$ .

step 2.1step 3.1F1F2∎

Remarks

What is exceptional about BPI and countable choice. BPI is transferable alongside an injectively boundable conjunction, and the cited stronger theorem transfers BPI and countable choice together. Neither principle is relabelled as injectively boundable here, and this interface supplies no countable-choice-only transfer.
What the statement does not do. It does not transfer the truth of the permutation model wholesale, and in particular it does not transfer the failure of well-orderability of the atom set or the countable-choice structure of the model; only the named principles and the certified sentences cross.

Depends on

Used by

Dependency tree · two levels

15 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

David Pincus, Zermelo–Fraenkel consistency results by Fraenkel–Mostowski methods (standard reference, not scraped)
David Pincus, Adding dependent choice (standard reference, not scraped)
Eleftherios Tachtsis, The Boolean prime ideal theorem does not imply the extension of almost disjoint families to MAD families (standard reference, not scraped)