Is the axiom $\Diamond\Box\varphi\to\Box\Diamond\varphi$ in c.c.c. forcing potentialism equivalent to the productivity of c.c.c. forcing? 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.
 A: 
Failure of $\sf CH$
It seems I was a bit off on my initial go at showing $(.2)_{ccc}$ entails the failure of $\mathsf{CH}$. Here is the correct argument.
Proposition 1: Assuming $(.2)_{ccc}$. 


*

*If $K\subset [\omega_1]^2$ is uncountable and c.c.c. then the graph $L = [\omega_1]^2 \backslash K$ is not powerfully c.c.c. 


(in particular $\mathsf{CH}$ fails, see Galvin1977; also, if I understand correctly, this statement is an odd mix of some of the c.c.c. partition relations listed here LarTodo2001, p. 87.)
Proof: Consider the statement $\varphi(a) := (\exists H)(\vert H \vert > \omega$, and $[H]^2 \subset a)$, then for each uncountable c.c.c. graph $K$, we have $\diamondsuit \square \varphi(K)$ (as witnessed by the partial order $\mathbb{P}_{K}$ of finite $K$-cliques, which is assumed to be c.c.c.) Applying $(.2)_{ccc}$ we must conclude $\square \diamondsuit \varphi(K)$. 
To establish the result, note that if the finite support product of countably many copies of $\mathbb{P}_L$ is c.c.c., then in the corresponding extension, $\omega_1$ is covered by countably many $L$-homogeneous sets. It follows that in no further $\omega_1$-preserving forcing extension, can the statement $\varphi(K)$ hold. $\square$
Remark: the use of "not powerfully c.c.c." in the above was a bit of a cop-out since I spent far to long treading water on simply "not c.c.c."; however it does seem to be important.

Partial Result on Products.
It turns out, under $(.2)_{ccc}$, there is a connection between being powerfully c.c.c. and productively c.c.c.; in particular
Proposition 2: Assuming $(.2)_{ccc}$:


*

*If $\mathbb{P}$ is powerfully c.c.c. (that is, each finite power of $\mathbb{P}$ is c.c.c.), then $\mathbb{P}$ is productively c.c.c. (i.e. the product of $\mathbb{P}$ with any other c.c.c. forcing, is again c.c.c.)


Proof: Given an order relation $a \subset \omega^{V}_1 \times \omega^{V}_1$ defined on $\omega^{V}_1$, let $\varphi(a)$ be the statement
$\varphi(a):= \left(\exists \mathcal{C} \subset \mathcal{P}(\omega^V_1)\right)(| \mathcal{C} | \le \omega$, each $C \in \mathcal{C}$ is centered with respect to $\le_a$, and $\omega^V_1 \subset \cup\mathcal{C})$
(it should be clear that $\varphi(a)$ holds, iff, the partial order $(\omega^V_1, \le_a)$ is $\sigma$-centered.)
Now, for each powerfully c.c.c. order relation $R \subset \omega^V_1 \times \omega^V_1$, the statement $\diamondsuit \square \varphi(R)$ holds (since by assumption, the finite support product of countably many copies of the partial order $(\omega^V_1, \le_R)$ is c.c.c. and in the extension generated by this product, the $\Sigma_1$ statement $\varphi(R)$ holds.) As such, from $(.2)_{ccc}$, we can conclude $\square \diamondsuit \varphi(R)$.
To establish the result, fix some c.c.c. partial order $\mathbb{P}$. Applying our interpretation of the modal operators $\square$ and $\diamondsuit$, we are guaranteed the existence of a $\mathbb{P}$-name $\dot{\mathbb{Q}}$, such that, the iteration $\mathbb{R}=\mathbb{P}\ast \dot{\mathbb{Q}}$ is c.c.c. and forces $\varphi(R)$.
Therefore, fixing an $\mathbb{R}$-name $\dot{\mathcal{C}}$ witnessing $\varphi(R)$ and arbitrary $\mathbb{P}$-name $\dot{A}$ forced by $1_\mathbb{P}$ to be an $R$ anti-chain, the following hold: 


*

*$\Vdash_\mathbb{R} (\forall C \in\dot{\mathcal{C}})( |C \cap \dot{A}| < \omega)$

*$\Vdash_\mathbb{R} |\mathcal{\dot{C}}| < \dot{\omega}_1=\omega^V_1$, and

*$\Vdash_\mathbb{R} \dot{A} \subset \bigcup \mathcal{\dot{C}}$
and combine to imply $\Vdash_\mathbb{P} | \dot{A} | < \dot{\omega}_1 = \omega^V_1$. Hence $\Vdash_{\mathbb{P}} (\omega^V_1, \le_\check{R}) \text{ is c.c.c. }$ and the result follows. $\square$
Remark: It's worth pointing out that under $\sf CH$, powerfully c.c.c. does not imply productively c.c.c. ( Galvin1977 )

The following dichotomy is an interesting corollary to Proposition 2.
Product Dichotomy: Assuming $(.2)_{ccc}$:
For every partial order $\mathbb{P}$: Exactly one of the following holds,


*

*The product of $\mathbb{P}$ with any c.c.c. partial order is c.c.c.


Or,


*

*Some finite power of $\mathbb{P}$ is not c.c.c.


Proof: Without loss of generality assume $\mathbb{P}$ is c.c.c. and apply Proposition 2.

In light of the previous corollary, the following seems like a natural question.
Question: Does $(.2)_{ccc}$ imply every c.c.c partial order is powerfully c.c.c.? 
As pointed out by @JoelDavidHamkins, it was already enough to just consider the square of c.c.c. partial orders.
