Can Tychonoff's theorem be applied to topological spaces generated by program output in ZFC?

Question

I am confused about an issue in set theory.

Tychonoff's theorem says that "an arbitrary product of compact topological spaces is compact". We often talk of an index set $I$ and then for each $n\in I$ we have a compact topological space $X_n$, and the claim is that $\prod_{n\in I}X_n$ is compact. There's a really cool super-short proof of this using filters by the way ;-)

My question is about how one might formalise this in ZFC. In Lean I just found myself writing X : I → Type for the family, and in the set theory model of Lean this is a "function" from a set $I$ to "the universe of all sets". This can't be done in ZFC, so one might want to start brandishing the axiom of replacement around a bit. My question is I think on the details of this.

Let's say I'm talking to you, a set theorist, and I ask you what your definition of a topological space structure is. You say it's an ordered pair consisting of a set $X$ and a topology $\mathcal{T}$ on $X$, which is a collection of subsets of $X$ satisfying some axioms. I say great, I write a few lines of computer code (just a small interface corresponding to your definition), run a proof checking system on my code, and it outputs a Haskell function which takes as input a natural number n and then prints out two strings which uniquely define a set X n and a topology T n on X n. To be more precise, for an input n it actually prints out a term which a set theory-based theorem prover such as Mizar or Metamath can understand -- it makes no "external" assumptions about the explicit model of ZFC we're working in, and X n and T n are provably well-defined unique objects. Furthermore I can prove that X n is compact for all n and indeed a computer has checked my proof, but I won't bore you with the details. The question is how now to state that the product of the X n is compact in ZFC, because I have not given you a function in the internal sense of a set which happens to be a function in the sense that it's a set of ordered pairs blah blah blah.

What I am unclear about is whether one can make the set of pairs $(n,X_n)$ in ZFC in order to be able to form the product needed to state Tychonoff's theorem.

Answer 1

This seems to require Replacement, as you point out. But not really, as you're about to find out.

What $\sf ZFC$ proves is that if $f$ is a function, i.e. a set of ordered pairs etc. (or however you choose to encode a function, really), such that for every $i$ in the domain of $f$, $f(i)$ is a topological space, that is an ordered pair $(X_i,T_i)$ satisfying the axioms of a compact topological space, then the topological space defined as $\prod X_i$ with the product topology, is also compact.

What $\sf ZFC$ does not prove is that if you, living in the meta-theory, specify for each $i$ in some index set, a topological space, in the meta-theory, then the product is compact, or even exists. If $M$ is a countable model of $\sf ZFC$, you can enumerate all the compact spaces inside of it, and consider for each $n<\omega$, the $n$th compact space. Obviously the product is not going to be in the model, since from the internal point of view this is a proper class.

So you, writing in Haskell¹ need to decide what you want to do. If type theory is your meta-theory, then the function $\tt X\colon I\to Comp$ is not really inside the universe of set theory, and is not subject to the definitions and consequences of $\sf ZFC$.

But if your type theory is taking place inside a universe of set theory, then $\tt X$ is a function, internal to the universe of sets. So you don't even need Replacement anymore, since by positing that $\tt X$ "exists" you already posits that it is a set, and therefore has a domain and range, as wanted.

This is similar to saying that as a professor you can answer each of the questions, and quite possibly make a mistake in your solution. But you're not module to failing the course and being kicked out of the degree. You're only subject to the scorn of your angry students (and possibly other issues on a faculty level).

---

1. We are currently not accepting Haskell code. Come back when you wrote it in Common Lisp. But let's put that aside for the moment.