Skip to content

Theorem Suggestion: $W$-Space (P187) implies $\alpha_2$ (P212) #1630

@felixpernegger

Description

@felixpernegger

The proof is quite straightforward. Let $x\in X$, $S_i$ as in the definition of $\alpha_i$. (wlog pairwise different to simplify the argument slightly)
Note that for every neighborhood $U$ of $x$, $|S_i \setminus U|$ is infinite. (+)
Play the game of $W$-Space. By the observation (+), Player II may first (injectively) choose an element of $S_1$ then $S_2$, $S_1$, $S_2$, $S_3$, $S_1$, $S_2$, $S_3$, $S_4$, $S_1$, ...
Let $S$ denote the set of elements chosen by Player II.
Since $X$ is P187, $S$ converges to $x$, but clearly $S_i \cap S$ is infinite, so $X$ is $\alpha_2$.

This is significant since this is the first theorem we have (excluding metaproperties) differentiating between different $\alpha_i$. This does not (trivially at least) generalise to $\alpha_1$.
The contrapose of this theorem gives 2 new traits, the direct implication 1 namely the Thomas plank (S91). It is therefore good to check if S91 is $\alpha_1$ or $\alpha_{1.5}$. (EDIT: Sadly $\alpha_1$ appears to hold for S91 by #1617 :( )

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions