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.
Transitive ZF models have standard arithmetic and proof codes
Statement
A transitive set model M of ZF has the real omega and natural arithmetic, and all finite natural-number syntax and proof codes. Every fixed arithmetic predicate on these codes agrees with ambient arithmetic. If M models ZFC, it satisfies the standard Con(ZFC).
Facts & Assumptions
ZF has an effective standard arithmetic interpretation: ZF and ZFC have effective axiom presentations and an interpretation of PA on the actual internally defined , using von Neumann zero/successor and recursively defined addition/multiplication. For their standard presentations the arithmetic proof constructors and translations needed for D1–D3 are verifiable in that interpretation. AC is unnecessary for the PA interpretation; ZFC adds one encoded Choice sentence.
Primitive-recursive syntax and certified proof checking: For the fixed effective signature and sentinel encoding, term/formula recognition, free-variable and free-for tests, capture-free substitution, numeral formation, negation, and certified derivation checking are primitive recursive. Invalid inputs return zero or false.
Proof
Given: A nonempty transitive M satisfying ZF with actual restricted membership, and additionally ZFC for the last clause.
Let w be the internal omega. The internal empty set is actual zero by transitivity; pairing and union on existing sets have their actual values since all their members are in M. External induction therefore fixes each finite ordinal and puts it in w. Internally w is a nonzero ordinal with no greatest element and every member is zero or a successor. Those assertions transfer externally: all their tests are bounded through w and its elements, and transitivity preserves the quantifier ranges. In ambient Foundation the ordinal order is an actual well-order. If w properly extended omega as an ordinal, it would contain omega as an element, contrary to the zero-or-successor property. Since it contains all finite ordinals, w equals omega.
The arithmetic recursion of F1 then agrees on each natural input by external induction: both additions start at a and both successors add one; both multiplications start at zero and add the same a at each successor. Every finite list of natural numbers is present via its natural code, and F2 decodes it using this same arithmetic. Induction on a fixed arithmetic formula transfers atoms and Boolean operations, and transfers quantifiers because both range over the identical omega. Thus every fixed effective proof predicate, and also its Con sentence, is absolute.
If , an actual ZFC-refutation would, by induction on its finitely many lines, be true in M: each axiom line holds by the model assumption, and each logical axiom and rule preserves truth in a nonempty structure. Its last contradictory sentence cannot hold. Therefore no actual refutation exists. The standard proof predicate is correct on those natural codes by step 2.1, so its universal absence assertion Con(ZFC) holds both externally and in M.
Depends on
Used by
Dependency tree · two levels
13 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.