# Elementary proof of compact space = exhaustible space?

The work of Martín Escardó has demonstrated close parallels between classical topology o one hand and computability on the other hand. (See for example "Infinite sets that admit fast exhaustive search" 22nd Annual IEEE Symposium on Logic in Computer Science (2007) 443–452) Escardó identifies continuous functions with computable functions, and open sets with recursively enumerable sets.

Another identification is between the exhaustible sets on one hand and compact sets on the other. A set $S$ is exhausible if, given a total predicate $P:S\to\mathbf{Bool}$, one can always decide whether $P$ holds for every element of $S$. According to Escardó, there is a close relationship between exhaustible and compact sets. For example:

• Finite sets are both compact and also obviously exhaustible.
• The natural numbers are not compact and are not exhaustible. (If they were, we could solve the halting problem.)
• But the one-point compactification of the naturals is exhaustible.
• The Cantor set of all sequences of booleans, that is all functions $f:\Bbb N\to\mathbf{Bool}$ is both compact and exhaustible.

I have found the discussion of compactness in Escardó's papers very hard to follow, with many forward references. The nearest thing to a proof that I can identify is in section 8 of his notes on "synthetic topology of data types". The proof in chapter 8 is very advanced. In these notes compactness is initially defined to be exhaustibility, which doesn't make it easier to follow what is going on.

My question is:

I keep hoping for an elementary proof, one which relates the conventional definition of compactness, in terms of open covers, to exhaustibility. I have not been able to find one myself and I have not been able to extract one from Escardó's papers. Is there such a proof?