Over at the nForum, we've been discussing sequential compactness. The discussion led me to realise that I naively assumed that nets were simply Big Sequences, and that I could make a reasonable guess at how nets would behave by thinking of them as such.
Not so. The crucial point, that I hadn't realised, was that subnets are not sub-nets in the way that subsequences are sub-sequences.
Where this came to light was in a discussion of the relationship between compactness and sequential compactness. Compactness can be expressed as:
Every net has a convergent subnet.
Sequential compactness as:
Every sequence has a convergent subsequence.
So, in my naivety, I assumed that compactness implied sequential compactness since I could take a sequence, think of it as a net, find a convergent subnet, and - ta-da - there's my convergent subsequence. The error, as Mike Shulman pointed out, is that not every subnet of a sequence is a subsequence.
And, indeed, there is a space that is compact but not sequentially compact. Writing $I = [0,1]$ then $I^I$ is compact but not sequentially compact. In particular, it is possible to find a sequence that has no convergent subsequence (the argument is a variant of Cantor's diagonal theorem) but that has plenty of cluster points and thus plenty of convergent subnets.
But the compactness of $I^I$ seems to require a Big Axiom (not quite the axiom of choice, or so I'm led to believe since $I$ is Hausdorff, but almost). I say "seems to" since I'm not an expert and there may be a way to prove that this specific space, $I^I$, is compact with only the basic axioms of ZF.
That's basically my question, except that I'm a topologist so I'm more interested in the implications for topological stuff than in the exact relationship between the Axiom of Choice and Tychanoff's theorem (and since I can just read the nLab page to learn that!). So, without further ado, here's the question:
Is "Compactness => Sequential Compactness" consistent with ZF?
This could be answered by a topologist since all it would require to show that this isn't so would be an example of a space that was compact but not sequentially compact and such that proving that didn't require any Big Axioms.References: