Initial proof that RP^2 has cardinality \aleph_1

[coycatrett]

No description provided.

[pzjp]

Welcome to pi-base/data! We appreciate you would like to contribute to the base but it seems your proposition is invalid.

First of all you edit property for cardinality $\aleph_1$ not $0$, as in the title.
And projective plane, has cardinality continuum and it cannot be decided (it does not follow from ZFC) whether $\mathfrak c=\aleph_1$ or not.

[coycatrett]

Ah, my apologies! Admittedly, I was excited because I thought that $\aleph_1$ and $\mathfrak{c}$ were the same. After some more research, suggested by your comment, it seems that they are only the same assuming the continuum hypothesis. Will be sure to refresh myself on definitions next time.

How do you deal with statements that cannot be proven in ZFC in $\pi$-base? Some kind of note at the beginning?

[Moniker1998]

@coycatrett we don't have support for such properties right now. I've collected a few but its not publicly available yet

[Moniker1998]

#1118 see here, there's some links to other discussions there including the discussion on the web github