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.
False statement: the CTM presentation proves Con(ZFC)
Statement
False statement: Con(ZFC) alone supplies a countable transitive model of all ZFC, so the semantic forcing presentation proves Con(ZFC) inside ZFC.
The refutation has two precise consistency qualifications. Under external Con(ZFC), the asserted internal proof of Con(ZFC) is impossible. For a set-model counterexample to the claimed derivable implication from consistency to a transitive model, retain the stronger external premise , where .
Facts & Assumptions
Given: The standard certified proof predicates. Use external Con(ZFC) for the unprovability assertion, and external Con(S) for the stronger countermodel assertion.
Semantic generic extensions of countable transitive models assumes a CTM and does not construct one from consistency.
Formal consistency transfer by forcing gives relative consistency from verified finite-fragment proof constructors.
The transitive-model consistency-strength gap under Con(S) gives a model of and nonderivability of the claimed TM implication.
Second incompleteness for standard provability forbids a consistent effective theory satisfying the standard arithmetic/derivability hypotheses from proving its own Con sentence.
ZF has an effective standard arithmetic interpretation verifies those hypotheses for ZFC's standard presentation.
Refutation
Under Con(S), apply F3 to obtain a set model K of . Inside K, Con(ZFC) holds and there is no transitive model of ZFC, hence no countable transitive one either. This is an actual model witness against derivability of the asserted consistency-to-CTM implication in ZFC. It is not asserted that K is externally well-founded or that Con(S) follows from Con(ZFC).
Independently, under external Con(ZFC), F5 verifies the arithmetic and standard derivability conditions for ZFC. F4 therefore gives . Thus the claimed internal proof of its own consistency cannot be furnished by forcing or by any other ZFC argument under this premise.
F1 begins with a full CTM as a hypothesis; applying it preserves that hypothesis and supplies no missing model-existence proof. F2 instead transforms verified finite-fragment constructions into a conditional Con implication. Accordingly neither theorem licenses the false inference, and the two precise failures in steps 1.1 and 1.2 refute its two assertions without confusing full CTMs with finite reflected fragments.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
25 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.