Alphabeta MathHow 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 Halpern–Läuchli theorem and the basic Cohen BPI model
Statement
ZF proves the finite-product Halpern--Läuchli dense-matrix dichotomy. Separately, from a transitive ZFC ground and a supplied Cohen generic, the basic Cohen finite-support symmetric model is a transitive model of
The model conclusion uses the Halpern--Lévy search-and-shift construction in the hereditarily symmetric presentation. It does not rely on the defective parameter-definable-maximal-ideal shortcut, and the choice-free combinatorial theorem does not by itself perform the symmetric-name analysis.
Facts & Assumptions
Given: For the model clause, a transitive ZFC ground and a supplied generic for the basic Cohen forcing. The combinatorial clause has no construction hypothesis.
Halpern–Läuchli dense-matrix dichotomy proves in ZF that for every positive finite family of finitistic trees and every subset of the full product, either the subset has matrices of every depth or its complement has matrices of every depth above one common level.
The basic Cohen model satisfies BPI and fails Choice proves the exact semantic model assertion in the hereditarily symmetric presentation.
Proof
F1 is already a theorem of ZF: its word calculus, finite thinning, and common-height cone repair use only finite coded selections. This proves the Halpern--Läuchli clause without AC.
Under the separate construction hypotheses, F2 supplies a transitive symmetric model satisfying ZF, BPI, and failure of AC. Its BPI proof works with finite supports and forcing-name orbits, so no identification with a parameter-HOD presentation is needed.
Steps 1.1 and 1.2 prove the two assertions and keep their axiom bases distinct. The empty family of trees is excluded by F1's positive-dimension hypothesis, while the model clause treats every nontrivial Boolean algebra through BPI.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
11 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 H. Läuchli, A partition theorem, Theorem 1, pp.360-367 (standard reference, not scraped)
- 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)