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.
Check-name evaluation and reconstruction of G
Statement
In ZF, for every nonempty , and . Hence for a transitive ZF model M containing P, and . The inclusion is not asserted to be elementary.
Facts & Assumptions
Given: ZF; G nonempty. Direct valuation calculations establish check recovery and dot G recovery, then ground membership of the names gives M subset M[G] and G in M[G].
Check names without a largest condition: Check names have every condition as a coefficient; dot G uses the name of p with coefficient p, and these names belong to the ground model.
Proof
By membership induction suppose the assertion holds for each . The valuation equation for check x gives exactly . The nonemptiness of G supplies the existential coefficient for every y. For x empty both sides are empty.
Apply step 1.1 to every p in P. The valuation equation gives . For each , F1 puts check x in M, so step 1.1 puts x in M[G]. F1 also puts dot G in M, so its value G lies in M[G]. No genericity or directedness was needed for these identities.