Motivated by this question I'm looking for a pair of Baire topological spaces whose product is not Baire and whose construction does not need the axiom of choice.

The example of such spaces I'm familiar with, which is due to Cohen, is to consider $\Bbb P_{S_1}\times\Bbb P_{S_2}$, where $S_1,S_2\subseteq\omega_1$ are disjoint stationary subsets of $\omega_1$ and $\Bbb P_{S_i}$ is the usual $\sigma$-distributive forcing that adds to $\omega_1$ a club contained in $S_i$, but this construction needs some choice.

I'm not too familiar with other examples of Baire spaces which are not productively Baire, but those that I could find in the literature all seemed to need some form of choice. Is there a construction in $\mathsf{ZF}$ of two Baire spaces $X,Y$ such that $X\times Y$ is not Baire? Or at the opposite, is it consistent with $\mathsf{ZF}$ that every finite product of Baire spaces is Baire?

thinkthere is enough structure there to ensure that new clubs are not too many, and are also met. This can probably be significantly tweaked and improved, too. $\endgroup$no$\sigma$-distributive forcings to begin with. For example, what is the situation in Gitik's model where every set is a countable union of smaller sets? Unclear. This somewhat relates to Foreman's maximality principle as well (without choice), that every forcing adds a real or collapses cardinals. But without choice. $\endgroup$4more comments