Sequence with convergent subnets but no convergent subsequences We can regard a sequence as a special kind of net.  But the definition of "subnet" is more flexible than that of "subsequence", so it's easy to find subnets of a sequence that aren't subsequences.
In fact, if $X$ is a compact topological space that is not sequentially compact, like 
$$  X = \prod_{x \in \mathbb{R}} [0,1] \; ,$$
we can have a sequence in $X$ that has no convergent subsequences, but it must have convergent subnets!  I've always found this phenomenon mysterious.  
Can someone describe, as explicitly as possible, a sequence in some topological space that has no convergent subsequences, but has a convergent subnet? 
Does finding an example require the axiom of choice, or is there an 'explicit' one?
 A: I give an explicit example here: let $X = \{0,1\}^I$ where $I = \{0,1\}^\mathbb{N}$. This is a compact space by Tychonoff's theorem, so every net has a convergent subnet.
If we denote for $i \in I$ and $n \in \mathbb{N}$ by $\pi_n(i)$ the $n$-th coordinate of the sequence (or function) $i$, then the required sequence is $(f_n)_n$, where all $f_n : I \to \{0,1\}$ are given by $f_n(i) = \pi_n(i)$ for all $i \in I$.
In the linked answer I give a diagonalisation argument why no subsequence of $(f_n)$ can converge in $X$ (i.e. pointwise). 
I think a convergent subnet of the $(f_n)$ (which exists by compactness) will probably involve some ultrafilter on $\mathbb{N}$, e.g. and so won't be as explicit.
A: Much to my surprise, there is an explicit example, and it comes about at least in part because it seems that the theorem going back and forth between cluster points and convergent subnets does not require the axiom of choice, when done the right way. In the first part of my answer, I describe the example, being as explicit with the subnet as I possibly can to show there's no AC up my sleeve. In the second part I comment on why choice is necessary for Henno Brandsma's example. 

To get a sequence with a convergent subnet but no convergent subsequence in just ZF, we only really need to work out the details of Exercise E from Chapter 2 of Kelley's General Topology. Accordingly I will be following Kelley's definitions of subnet and so on throughout.
Just for clarity, we will be taking $\newcommand{\N}{\mathbb{N}}\N$ to include $0$ in the following. We define a topology on $\N \times \N$ where $\{(n,m)\}$ is open if $(n,m) \neq (0,0)$ and $U \subseteq \N \times \N$ is an (open) neighbourhood of $(0,0)$ iff it contains $(0,0)$ and for all but finitely many $m \in \N$, the set $\{ n \in \N \mid (m,n) \not\in U \}$ is finite. Or, if you prefer, the open sets are


*

*Sets not containing $(0,0)$.

*Sets containing $(0,0)$ such that for all but finitely many $m \in \N$, the set $\{ n \in \N \mid (m,n) \not\in U \}$ is finite.


The first thing we need is:

Lemma 1: Any sequence $(m_i,n_i)_{i \in \N}$ of elements in $\N^2\setminus\{(0,0)\}$ does not converge to $(0,0)$. 

Assume for a contradiction that there is such a sequence $(m_i,n_i)_{i \in \N}$ converging to $(0,0)$. Given $k \in \N$, define $V_k = \{ (m,n) \in \N^2 \mid m \neq k \} \cup \{ (0,0) \}$. This is a neighbourhood of $0$ (using the "all but finitely many $m$ part"), so for each $k \in \N$ there is an $N_k$ such that for all $i \geq N_k$, $(m_{i},n_{i}) \in V_k$, i.e. $m_i \neq k$. It follows that there are only finitely many $i \in \N$ such that $m_i = k$. 
Now consider $U = \N^2 \setminus \{(m_i,n_i)\}_{i \in \N}$. It contains $(0,0)$, and for each $m \in \N$, 
$$
\{ n \in \N \mid (m,n) \not\in U \} = \{ n \in \N \mid (m,n) \in \{(m_i,n_i)\}_{i \in \N} \},
$$
and this set is finite because $m_i = m$ only happens if $i < N_m$. Therefore $U$ is a neighbourhood of $(0,0)$ (using the other part of the definition). But this contradicts $(m_i,n_i)_{i \in \N}$ converging to $(0,0)$, so there is no such sequence. $\square$
Now, we define a sequence $(x_i)_{i \in \N}$ to be any enumeration of $\N^2 \setminus \{ (0,0) \}$. There are many ways to do it, and it does not particularly matter how, so I won't give one explicitly as I don't want to get caught out in a silly mistake. By Lemma 1, no subsequence of it converges to $(0,0)$. We define a subnet as follows. Take $\mathcal{N}$ to be the set of neighbourhoods of $(0,0)$, ordered by $\supseteq$. This is a directed poset. We define
$$
J = \{ (i,U) \in \N \times \mathcal{N} \mid x_i \in U \},
$$
with the ordering being as a subposet of $\N \times \mathcal{N}$. We take $f : J \rightarrow \N$ to be the projection mapping $\pi_1$, and for each $(i,U) \in \N \times \mathcal{N}$ we define $y_{i,U} = x_i$.

Proposition $((y_{(i,U)})_{(i,U) \in J}, f)$ is a subnet of $(x_i)_{i \in \N}$ converging to $(0,0)$.

We first need to show that $J$ is directed as a poset. If $(i_1,U_1), (i_2,U_2) \in J$, then $U_1 \cap U_2$ is a neighbourhood of $(0,0)$, so is infinite, so there must exist $j \geq i_1,i_2$ such that $x_j \in U_1 \cap U_2$. Then $(j,U_1 \cap U_2)$ is the upper bound we need. 
To show that $(y_{(j,U)})_{(j,U) \in J}$ is a subnet, we only need to show that for each $i \in \N$ there exists $(j,U) \in J$ such that for all $(j',U') \geq (j,U)$ $f(j',U') \geq i$. To do this, we define $(j,U) = (i,\N^2)$. For all $(j',U') \geq (i,\N^2)$ we have $f(j',U') = j' \geq i$, as required. 
The last remaining part is to show that this subnet converges to $(0,0)$. If $U \subseteq \N^2$ is a neighbourhood of $0$, then it contains some $(m,n) \neq (0,0)$, and by the definition of $(x_i)_{i \in \N}$ there exists some $i \in \N$ such that $x_i = (m,n) \in U$. Now, for all $(j,V) \geq (i,U)$, $y_{(j,V)} = x_j \in V \subseteq U$, so $y_{(j,V)} \in U$. $\square$

Henno Brandsma's example uses the Boolean ultrafilter lemma in the form of Tychonoff's theorem for Hausdorff spaces. There's a related example that shows that $\N$, embedded in $\beta(\N)$ has no convergent subsequence (because convergent sequences in Stonean spaces are eventually constant). Both of these examples actually require the existence of non-principal ultrafilters on $\N$, which I will show as follows.
Suppose $((y_i)_{i \in I}, f: I \rightarrow \N)$ is a convergent subnet of $(\pi_n)_{n \in \N}$ converging to $y \in 2^{2^{\N}}$. Each $\pi_n$ is actually a Boolean homomorphism $2^\N \rightarrow 2$, and since convergence in the product topology is pointwise, this implies that $y : 2^\N \rightarrow 2$ is a Boolean homomorphism. 
Therefore $y^{-1}(1)$ is an ultrafilter on $\N$. In fact it is non-principal. This can be shown by the following argument. Define $\delta_n : \N \rightarrow 2$ to be the indicator function of $\{n\} \subseteq \N$, and $N_{\delta_n,1}$ to be the subbasic clopen
$$
N_{\delta_n,1} = \{ f : 2^\N \rightarrow 2 \mid f(\delta_n) = 1 \}.
$$
If $y(\delta_n) = 1$, then $y \in N_{\delta_n,1}$ so by the definition of convergence, there exists $i_1 \in I$ such that for all $i' \geq i_1$, $y_{i'} \in N_{\delta_n,1}$. We also have, from the definition of subnet, that there exists $i_2 \in I$ such that for all $i' \geq i_2$, $f(i') \geq n+1$. By directedness of $I$, there exists $i_3 \geq i_1,i_2$. For all $i' \geq i_3$, we have $y_{i'}(\delta_{n}) = 1$, but also $y_{i'} = \pi_{f({i'})}$ with $f(i') \geq n+1$ and so $y_{i'}(\delta_{n}) = 0$, a contradiction. Therefore $y(\delta_n) \neq 1$ for all $n \in \N$ and so $y^{-1}(1)$ is a non-principal ultrafilter. 
Now, there are various models of ZF in which dependent choice holds but there are no non-principal ultrafilters on $\N$. Solovay's model in which all sets are Lebesgue measurable is a famous one, but there are many others such as the Solovay-Pincus model in which the Hahn-Banach theorem holds, but there are no non-principal ultrafilters on any set whatsoever. In these models, therefore, $(\pi_n)_{n \in \N}$ has no convergent subnets. Similarly, the set of principal ultrafilters in $\beta(\N)$ has no convergent subnets because it is closed, being all of $\beta(\N)$. 

As a coda, I'll say that I have not addressed the question of whether "every compact space is sequentially compact" is consistent with ZF or ZF + DC. All we've seen is that the standard counterexamples don't work, but that we cannot go as far as "every sequence with a convergent subnet has a convergent subsequence". This seems to be a hard question, more suitable for MathOverflow. I couldn't find anything about it in standard references such as Howard and Rubin's Consequences of the Axiom of Choice. 
Added in edit: Apparently Andrew Stacey asked it on MathOverflow donkey's years ago, getting two bad answers, and an interesting answer by K.P. Hart explaining a mistake in one of the answers. However, no answer to the original question was forthcoming. 
