CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

If ZF is consistent, ZF does not prove Urysohn's lemma

Statement

If $Z F$ is consistent then $Z F$ does not prove Urysohn's lemma: there is a model of $Z F$ in which some normal space has two disjoint closed sets that admit no continuous separation (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

The statement is conditional on $Con (Z F)$ and is stated in the metatheory; no model of $Z F$ is exhibited in the library and no unconditional nonprovability is asserted.

Facts & Assumptions

Given: A proof of Urysohn's lemma in $Z F$ and the consistency of $Z F$ .

[F1]

Relative to $Con (Z F)$ , the theory $Z F + {A C}_{ω} + \neg U R Y$ is consistent (Relative consistency of Countable Choice without Urysohn's lemma, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L1]

If $T^{'} \supseteq T$ and $T$ proves a sentence $σ$ , then $T^{'}$ also proves $σ$ ; consequently $T^{'} + \neg σ$ is inconsistent. Equivalently, if $T^{'} + \neg σ$ is consistent, then $T$ does not prove $σ$ . In particular, if $Z F$ proves $σ$ , then so does $Z F + {A C}_{ω}$ (elementary consequences of the definition of derivability).

Proof

technique · contradiction

1.1

Assume, for the sake of contradiction, that $Z F$ proves Urysohn's lemma, and assume $Con (Z F)$ .

assume-contra

2.1

Then $Z F + {A C}_{ω}$ proves Urysohn's lemma, since it extends $Z F$ ; but Urysohn's lemma is the sentence $U R Y$ whose negation is consistent with $Z F + {A C}_{ω}$ by [F1].

step 1.1F1L1

3.1

The theory $Z F + {A C}_{ω} + \neg U R Y$ is therefore inconsistent, contradicting its consistency given by [F1] under the assumption $Con (Z F)$ ; hence $Z F$ does not prove Urysohn's lemma.

step 2.1F1discharge-contradiction∎

Remarks

Why the conditional is not weakened to a ZF theorem. The nonprovability is relative to the consistency of $Z F$ ; this library proves no independence result unconditionally, and the cited relative-consistency theorem carries the same qualification.
The stronger statements this corollary is drawn from. The cited theorem gives a model of $Z F$ with countable choice in which Urysohn's lemma fails; the same failure occurs in the BPI model of this page, and either witness would serve. The corollary records the catalogue clause that Urysohn's lemma is not a theorem of $Z F$ alone, using the countable-choice witness, and it is generated directly from the published relative-consistency statement.

Depends on

Used by

The converse from Urysohn's lemma to DMC is open Remark

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.

Sources

Eleftherios Tachtsis, The Urysohn Lemma is independent of ZF + Countable Choice (standard reference, not scraped)
Eleftherios Tachtsis, Erratum to The Urysohn Lemma is independent of ZF + Countable Choice (standard reference, not scraped)