Universal first countability in ZF? It's easy to come up with examples of spaces which are provably-in-ZFC not first countable: e.g. the order topology on $\omega_1+1$, or the cocountable topology on any uncountable set. However, these proofs tend to rely on principles of the form "every 'small' union of 'small' sets is 'small'," and these can fail quite badly without choice.
Conversely, at the other end of things, if we extend ZF by a strong anti-choice principle, we can often get provably non-first-countable spaces. For example, the cofinite topology on an amorphous set $A$ is non-first-countable. 
Why? Pick $a\in A$, and consider a sequence $(U_i)_{i\in\mathbb{N}}$ of neighborhoods of $a$. The union of the complements of the $U_i$s must not be finite in order for the sequence to witness first countability. Let $V_i$ be the set of points "thrown out for the first time" at stage $i$: that is, $V_i$ is the set of $y$ such that $y\not\in U_i$ but $y\in \bigcup_{j<i} U_j$. Infinitely many of the $V_i$s must be nonempty; WLOG suppose each $V_i$ is nonempty. But then $\bigcup_{i\in\mathbb{N}}V_{2i}$ and $\bigcup_{i\in\mathbb{N}}V_{2i+1}$ are two disjoint infinite subsets of $A$.
So my question is whether we can find non-first-countable spaces in ZF alone. Phrased most simply, this is:

Does ZF prove that there are non-first-countable spaces?

We can also ask a question which might be a bit more satisfying:

Is there a formula $\varphi$ which ZF proves defines a non-first-countable topological space?

I suspect that the answer to even the first question is "no," and that this is witnessed in something like Gitik's model; but I'm not sure.
 A: Let $X=\mathbb{N}\times\mathbb{N}\cup\{\infty\}$, topologized such that a nonempty set is open iff it contains $\infty$ and contains cofinitely many points of $\{n\}\times\mathbb{N}$ for each $n\in\mathbb{N}$.  Then $X$ is not first-countable at $\infty$.  Indeed, suppose $(U_n)$ is a local base at $\infty$.  For each $n$, let $j_n$ be the least $j$ such that $(n,j)\in U_n$ (since $U_n$ is nonempty and open, it must contain $(n,j)$ for all but finitely many $j$).  Now let $$U=\{\infty\}\cup\{(n,j)\in\mathbb{N}\times\mathbb{N}:j>j_n\}.$$ Then $U$ is an open neighborhood of $\infty$.  However, $U$ does not contain any $U_n$, since for each $n$, $(n,j_n)\in U_n$ but $(n,j_n)\not\in U$.
This is not just a pathological example--similar examples come up very naturally when you glue together infinitely many spaces at a point, for instance, when considering non-locally finite CW complexes in algebraic topology.  As a very concrete example, a wedge sum of countably infinitely many copies of $[0,1]$ can be proven (in ZF) to not be first-countable at the basepoint by essentially the same argument.
A: Topologize $\mathbb N$ so that a subset $U$ of $\mathbb N$ is open if either $1\notin U$ or else $\sum\{\frac1n:n\in\mathbb N\setminus U\}\lt\infty.$
I claim that there is no countable base for the neighborhoods of $1.$
Suppose $U_1,U_2,U_3,\dots$ is an infinite sequence of open sets containing $1.$ For each index $i,$ since $U_i$ is an infinite set, we can define $n_i$ as the least element of $U_i$ which exceeds $2^i.$ Then, since $\sum_{i=1}^\infty\frac1{n_i}\lt\sum_{i=1}^\infty2^{-i}\lt\infty,$ the set $U=\mathbb N\setminus\{n_1,n_2,n_3,\dots\}$ is an open set containing $1;$ and for each $i$ we have $U_i\not\subseteq U$ since $n_i\in U_i\setminus U.$
