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.
Relative consistency from a forced sentence
Statement
Let be a fixed membership sentence. Suppose a uniform formal finite-fragment forcing verification over ZFC forces and verifies each required finite target fragment, with the total proof-constructor verification in an arithmetic base B specified by Formal consistency transfer by forcing. Then
A single externally supplied CTM and its semantic extension do not provide the stipulated formal verification data.
Facts & Assumptions
Given: A fixed sentence phi, the effective presentation obtained by adding that sentence to ZFC, and the B-verified finite-fragment forcing data of the statement.
Formal consistency transfer by forcing gives formal Con transfer for a certified effective target with B-verified source-model, conversion and soundness constructors.
Proof
Take in F1. Its certified axioms are either certified ZFC axioms or the single extra sentence phi, distinguished by a fixed tag and exact sentence-code equality. For a certified T-refutation its finite support is therefore a finite list of ZFC axioms, possibly together with phi. The assumed uniform verification supplies the constructors for that exact list; if phi is absent, restrict the same target verification to the smaller list. Thus T meets every hypothesis of F1.
F1 now yields the claimed implication in B. No existence assertion for a full ZFC CTM occurred in step 1.1: the hypothesis supplied verified proof constructors for the finite supports. Consequently a semantic extension of a single CTM does not suffice to instantiate this corollary unless those additional data are also provided.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
4 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.