@LeakyNun I'm not familiar with Hausdorffication, but it feels like the Cantor-Bendixson rank where the most obvious route is to iterate long enough. As in the proof of Zorn's lemma, it's not that bad because we don't have to go through all the ordinals, and can in fact just use one particular well-ordering that does not inject into the original space. Then at each step either the space is Hausdorff or we remove some points. We must reach a Hausdorff space at some point.
In other words, the 'most problematic' part is in the construction of said well-ordering. If for whatever reason one does not believe that there is a well-ordering that does not inject into the original space, then the proof fails.
I'm not sure whether I mentioned before, but in my type theory one can prove that for every separable type (a predicative type that has boolean equality on members) there is a well-ordered separable type that does not inject into the original type.
Despite not being able to construct von Neumann ordinals, or any canonical type of well-orderings.
@LeakyNun Given a well-ordering W that does not inject into the original space, we can easily obtain a well-ordering of the original space, and I think we can use that to avoid AC. (I did use choice all over to construct W, mostly for my convenience, but I think the only essential use of choice is to get a well-ordering of a collection from a well-ordering that does not inject into it.)
You'd have to ask Asaf if your question is about Hausdorffication without choice (because who knows there may be another way), but I suspect the answer is also that it requires some amount of choice.
Can the left adjoint to the inclusion functor $i : \mathbf{Haus} \to \mathbf{Top}$ be constructed constructively and predicatively in ZF?
If all three conditions are not possible, why and what is the best we can do?
But, you should more precisely define "predicatively".
For example, say BZF (bounded ZF) where all defining quantifiers are bounded.
Then it's a well-defined question.
Also, you should phrase it in terms of concrete stuff that people can grasp immediately, such as "Does every topological space have a quotient that is Hausdorff?".
user131753
Also I think @LeakyNun, you may give an explicit list of "all three conditions" that you mentioned in your post and possibly include some of your ideas in trying to answer the question.
@user21820 I don't think that's good enough. I could quantify over the subsets of A to define the maximal hausdorff quotient of A (although that would use choice)
user131753
@LeakyNun Well then maybe consider writing it in that way, like:
user131753
"Can the left adjoint to the inclusion functor $i : \mathbf{Haus} \to \mathbf{Top}$ be constructed (1) constructively, (2) predicatively and (3) in $\mathsf{ZF}$?
If a construction satisfying all three conditions (i.e., (1), (2) and (3)) are not possible, why and what is the best we can do?"
user131753
Also please consider including some of your ideas in trying to answer the question (maybe by giving a link to this chatroom and the ongoing discussion).
user131753
What I proposed above mayn't be the optimal one @LeakyNun. But for me your current version read like you were only talking about two conditions, namely, "constructed constructively" and "predicatively in ZF".
If LeakyNun follows your suggestion, it is still valid to criticize the question as being imprecise. Even logicians do not agree on "predicativity".
And we don't know the reason for the downvote, which could be just because of that word.
user131753
@user21820 Sure, I agree. Then @LeakyNun should more precisely define that term in his/her question like for example, as you said, or by articulating his/her own definition of the term.
@LeakyNun It seems Eric's answer settles your question completely, even though he didn't know what "predicative" means. Because as long as you accept that predicative types is closed under function types then the intersection he wants is predicative.
In particular, are you saying that even given the topological structure as an oracle (telling you whether a given subset of the space is an open set or not), you are unable to push the proof through?
This is what I would still consider as constructive.
And also given the ability to construct procedures given the available oracles and previously constructed procedures.
If you say it can't be done, I'll just believe you for now, because I'm kind of busy with other things haha..
Can the left adjoint to the inclusion functor $i : \mathbf{Haus} \to \mathbf{Top}$ be constructed constructively and predicatively in ZF?
If all three conditions are not possible, why and what is the best we can do?
