This question arose in connection with a lecture series on Potentialism that I have just completed here in Hejnice in the Czech Republic at the Winter School 2018 (see Slides). Several of us discussed the question late into the evening after my talks, and still we have no resolution.

Consider the context of c.c.c. forcing over the set-theoretic universe $V$. Let us interpret the modalities by c.c.c. forceability, so $\Diamond\varphi$ means that $\varphi$ is c.c.c. forceable, and $\Box\varphi$ means that $\varphi$ holds in all c.c.c. extensions.

It is easy to see that under Martin's axiom $\text{MA}_{\omega_1}$, every instance of the $(.2)_{ccc}$ axiom scheme $$\Diamond\Box\varphi(a)\to\Box\Diamond\varphi(a)$$ holds, where $a$ is a parameter of hereditary size at most $\omega_1$. This scheme asserts that any statement that is c.c.c. possibly necessary is c.c.c. necessarily possible. Since it follows from MA, but does not hold in $L$, for example, one can view the axiom as a weak version of MA.

For example, the $(.2)_{ccc}$ axiom scheme implies that there are no Suslin trees. To see this, suppose $T$ is a Suslin tree and consider the statement "$T$ has a branch." This is c.c.c. possibly necessary, since we could force with $T$, but it is not c.c.c. necessarily possible, since we could force instead to specialize $T$, which would prevent it from getting a branch in any c.c.c. extension.

The $(.2)_{ccc}$ scheme holds provided merely that the product $\mathbb{P}\times\mathbb{Q}$ of two c.c.c. forcing notions is still c.c.c., which is a consequence of $\text{MA}_{\omega_1}$. To see this, suppose that $\Diamond\Box\varphi(a)$ holds. So there is a c.c.c. forcing notion $\mathbb{P}$ forcing $\Box\varphi(a)$. Now, for any c.c.c. forcing notion $\mathbb{Q}$, the product $\mathbb{P}\times\mathbb{Q}$ is c.c.c., and so $\mathbb{P}$ remains c.c.c. after forcing with $\mathbb{Q}$. The product extension will satisfy $\varphi(a)$, since it can be viewed as an extension of $V^{\mathbb{P}}$, and so $\Box\Diamond\varphi(a)$ holds in $V$, as desired.

Question.Is the (.2) axiom scheme for c.c.c. forcing $$\Diamond\Box\varphi(a)\to\Box\Diamond\varphi(a)$$ equivalent to the assertion that the product of c.c.c. forcing is necessarily c.c.c.?

We allow any $\varphi$ in the language of set theory and any parameter $a$ of hereditary size at most $\omega_1$.

The question is extremely natural, since the productivity of c.c.c. forcing is closely connected with directedness of the (mutually generic) c.c.c. extensions, and the finite directed pre-orders are complete for S4.2, whose central axiom is precisely the scheme in question.

Let me make several observations.

If one assumes the c.c.c. maximality principle, which is the S5 scheme $$\Diamond\Box\varphi(a)\to\varphi(a),$$ then indeed the product of c.c.c. forcing is c.c.c., and the reason is that if a product $\mathbb{P}\times\mathbb{Q}$ of c.c.c. forcing was not c.c.c., then there is an instance of size $\omega_1$ and the assertion "$\mathbb{P}$ is not c.c.c." would be possibly necessary by the c.c.c. forcing $\mathbb{Q}$, and so it would have to be already true by the maximality principle, contradicting the assumption that $\mathbb{P}$ was c.c.c.

The (.2) axiom is exactly equivalent to the assertion that there are no railway switches, to use the terminology of my talk. So the question is asking whether you can construct a railway switch from any violation of c.c.c. productivity.

Thus, the question appears to be fundamentally connected with the question: if a c.c.c. forcing notion $\mathbb{P}$ is not c.c.c. necessarily c.c.c., then must there be fundamentally two different and incompatible ways to c.c.c. destroy the c.c.c.ness of $\mathbb{P}$? If so, then this would amount to an affirmative answer to the question, because the statement that $\mathbb{P}$ was not c.c.c. because of the first way would be c.c.c. possibly necessary, but not c.c.c. necessarily possible, because we could destroy it the other way.

Lastly, here is a slightly weaker version of the question.

Weaker Question.Does the (.3) axiom scheme for c.c.c. forcing, with parameters of hereditary size at most $\omega_1$ $$\Diamond\varphi(a)\wedge\Diamond\psi(a)\to\Diamond[(\varphi(a)\wedge\Diamond\psi(a))\vee(\psi(a)\wedge\Diamond\varphi(a))]$$ imply the productivity of c.c.c. forcing?

The point is that S4.3 implies S4.2, and so this question may be easier to answer. The axiom (.3) should be thought of as expressing the linearity of truth, since it says that if two statements are c.c.c. forceable, then one of them can be viewed as happening before the other. This is weaker than the maximality principle, and stronger than (.2), but still I don't know how to prove it implies the product of c.c.c. forcing is c.c.c.