Thanks, Bas!

]]>I’ve added some links to the constructive literature, both Bishop and locales. I haven’t traced everything back to the original sources yet.

]]>You are right. The last step in my proof is actually wrong.

]]>Wait, are you claiming that the Tychonoff theorem for products of intervals doesn’t require the ultrafilter principle?

I think the ultrafilter principle should follow from the Tychonoff theorem for intervals. If the power $I^J$ is compact for any set $J$, then so is the power $2^J$ (being a closed subspace). But it is not hard to prove the Boolean prime ideal theorem from compactness of $2^J$, and this is equivalent to the ultrafilter principle.

]]>Thank you, I wasn’t aware of this subtlety. But what about this rescue of Tychonov’s theorem:

In the case of an product of intervals $\prod I_j$ we use Definition 2.5:

- Given any proper filter $\mathcal{U}$ on $\prod I_j$.
- For each $j$ take the infimum $x_j$ of all cluster points of $pr_j (\mathcal{U})$. This is again a cluster point.
- The point $x = (x_j)\in \prod I_j$ is now a cluster point of $\mathcal{U}$.

For the second step: take any neighborhood $B$ of $x_j$. It contains a neighborhood of some cluster point of $pr_j (\mathcal{U})$. Hence the intersection of any set in $pr_j (\mathcal{U})$ with $B$ is inhabited.

For the last step in this argument: it is obvious that for any neighborhood $A$ belonging to the subbase of the topology of $\prod I_j$ consisting of all preimages of all open sets under all projection maps it holds that $A = pr_j^{-1} B$ has nonempty intersection with every $U \in \mathcal{U}$ as $B_j \cap pr_j(U)$ is inhabited. This holds also for finite intersection $A = A_1\cap \ldots \cap A_n$. Finally, it holds for products.

]]>You still need the ultrafilter principle/theorem though, which is where I found the needed link to the page on the B-A theorem.

]]>Perhaps it’s worth noting that even in the non-separable case the Axiom of choice is not required for the proof: it bases on the product $\prod_X [-1,1]$. As discussed here in Remark 2.1 Tychonoff’s theorem holds without AC in this case as $[-1,1]$ is Hausdorff.

]]>I created a short entry Banach-Alaoglu theorem to fulfil a grey link. While the general theorem is equivalent to the Tychonoff theorem for *Hausdorff* spaces, the case of separable Banach spaces is constructive. I do wonder *how* constructive, but apparently this gets used to construct solutions to PDEs, so I guess it’s quite concrete.