Hybrid Maximal Filter Spaces

We introduce a new way of encoding general topology in second order arithmetic that we call hybrid maximal filter (hybrid MF) spaces. This notion is a modification of the notion of a proper MF space introduced by Montalbán. We justify the shift by showing that proper MF spaces are not able to code most topological spaces, while hybrid MF spaces can code any second countable MF space. We then answer Montalbán’s question about metrization of well-behaved MF spaces to this shifted context. To be specific, we show that in stark contrast to the original MF formalization used by Mummert and Simpson, the metrization theorem can be proven for hybrid MF spaces within \(\text {ACA}_0\) instead of needing \(\varPi _2^1-\text {CA}_0\) .