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 Feferman–Levy symmetric collapse system
Definition
Work over a transitive ground model . The use of Choice is confined to the ground-model aleph sequence and the GCH cardinal calculations below; The Axiom of Choice is not assumed in the eventual symmetric model. Put for and let be the set of finite partial functions
such that whenever , ordered by reverse inclusion. Equivalently, is a finite set of triples , functional in , with . Its restriction to the first layers is
Thus the th layer is the collapse order from Cohen, collapse, and Lévy-collapse forcing orders, and is their finite-support product.
Let consist of the permutations of which preserve the first coordinate. Thus for a sequence of permutations . It acts on by
and on names by Automorphisms acting on forcing names. For let
The subgroups are normal, , and their upward closure is a normal filter of subgroups. Hence is a symmetric system in the sense of Symmetric forcing systems, supports, and hereditarily symmetric names. If is -generic, its hereditarily symmetric interpretation
is called the Feferman–Levy model. A name is said to have -bounded layer support when fixes it.
Depends on
Used by
Dependency tree · two levels
12 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
- Thomas Jech, The Axiom of Choice, Theorem 10.6, equations (10.2)–(10.5), printed pp. 142–143 (standard reference, not scraped)