CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Consistency of a Urysohn counterexample theory obstructs a ZF proof

Statement

Let $T$ be any first-order theory extending ZF and containing the negation of Urysohn's lemma for normal spaces (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly). If $T$ is consistent, then ZF does not prove Urysohn's lemma.

This is a conditional criterion. It asserts neither consistency of such a $T$ nor existence of a model or a counterexample space.

Facts & Assumptions

Given: A consistent theory $T$ containing every ZF axiom and the sentence $\neg U R Y$ , where $U R Y$ asserts continuous separation of disjoint closed sets in every normal space.

[F1]

A finite derivation using axioms of a subtheory is a derivation in the extending theory, since each axiom used is still available.

Proof

1.1givenF1assume-contra

Suppose ZF proves $U R Y$ . The same finite derivation is a $T$ derivation by F1 and the given inclusion of axioms.

2.1givenstep 1.1discharge-contradiction∎

Since $T$ also has $\neg U R Y$ as an axiom, it would derive a contradiction. This contradicts the assumed consistency of $T$ ; therefore ZF does not prove $U R Y$ .

Depends on

Normal spaces and $T_4$ spaces, with the source disagreement over whether normality includes $T_1$ stated explicitly

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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)