I am looking for an example of a proper forcing notion $ \mathbb{P} $ such that $ \mathbb{P} \times \mathbb{P} $ is not proper.
Maybe someone knows an obvious example or can give a reference to such an example in the literature?!
I am looking for an example of a proper forcing notion $ \mathbb{P} $ such that $ \mathbb{P} \times \mathbb{P} $ is not proper.
Maybe someone knows an obvious example or can give a reference to such an example in the literature?!
On
Here is an example showing that it is at least consistent that such a $\mathbb{P}$ exists. Work over $L$ and let $T$ be the $L$-least Suslin tree. Let $\mathbb{P}$ be the lottery sum of the forcings to shoot a branch through $T$ and to specialize $T$. Since both of these are ccc, $\mathbb{P}$ is also ccc, so in particular proper. But the product $\mathbb{P}\times\mathbb{P}$ has conditions which force that $\omega_1$ is collapsed (e.g. the condition opting for shooting a branch in the first factor and specializing in the second), so it cannot be proper.
Added: Here is an argument from just ZFC, similar to what we did before. It was shown by Shelah that there are proper posets $\mathbb{Q}_1,\mathbb{Q}_2$ such that $\mathbb{Q}_1\times\mathbb{Q}_2$ collapses $\omega_1$. Let $\mathbb{P}$ be the lottery sum of $\mathbb{Q}_1$ and $\mathbb{Q}_2$. Then $\mathbb{P}$ is proper but, as above, $\mathbb{P}\times\mathbb{P}$ has conditions which force that $\omega_1$ is collapsed, so it cannot be proper.
There is a natural example (provable in $\mathsf{ZFC}$), that probably goes back to Shelah, see his Proper and improper forcing book, on chapter XVII:
Consider $\mathbb P=T=(\omega_2)^{<\omega_1}$, so conditions are functions $f$ with domain a countable ordinal, and range contained in $\omega_2$, and extension is extension of functions. Note that $\mathbb P$ is a tree and, as a forcing notion, it is $\sigma$-closed (thus proper), and collapses $\aleph_2$ by adding a branch through $T$ that is actually a surjection from $\omega_1$ onto $\omega_2^V$.
Now, following Baumgartner, let $\mathbb Q_1$ be the forcing that adds $\aleph_2$ Cohen reals, followed by $\mathrm{Coll}(\omega_1,2^{\aleph_1})$ (so $\mathbb Q_1$ is proper as it has the form ccc$*$$\sigma$-closed). As explained in Baumgartner's paper Applications of the proper forcing axiom, forcing with $\mathbb Q_1$ makes $\omega_2^V$ of cofinality $\omega_1$ and, most importantly, in $V^{\mathbb Q_1}$, $T^V$ has no branch with supremum $\omega_2$, and has no new $\aleph_1$-branches (this is a classical argument due to Silver), so that $T$ has at most $\aleph_1$ many $\omega_1$-branches. Finally, let $\mathbb Q$ be $\mathbb Q_1$ followed by the sealing forcing, the (ccc) forcing that "specializes" $T$ in the sense of Baumgartner. What matters is that this forcing "seals" the branches of $T$ in the sense that any outer model of $V^{\mathbb Q}$ with the same $\aleph_1$ has precisely the same branches through $T$ as $V^{\mathbb Q}$ does.
The point is that $\mathbb P\times \mathbb Q$ collapses $\aleph_1$, so it cannot be proper. To see this, note that in $V^{\mathbb P\times\mathbb Q}$ there is a new branch through $T$ (since we are adding a generic for $\mathbb P$), but this is a generic extension of $V^{\mathbb Q}$, so necessarily $\aleph_1^V$ was collapsed.
(So, to get the example that you want, consider $\mathbb R=\mathbb P\oplus\mathbb Q$, the lottery sum of $\mathbb P$ and $\mathbb Q$, so $\mathbb R$ is proper, but $\mathbb R\times\mathbb R$ cannot be, as some of its generics collapse $\aleph_1$.)
Chapter XVII of Shelah's book discusses many more elaborate examples, in particular verifying that if $\alpha<\beta<\omega_1$ are indecomposable ordinals, the forcing axiom for $\alpha$-proper forcing notions does not imply the forcing axiom for $\beta$-proper forcing notions. This work has been recently extended by Aspero-Friedman-Mota-Sabok, who have similarly separated the bounded forms of these forcing axioms, and in the process solved negatively an old conjecture of Baumgartner, by verifying that not every axiom $A$ forcing embeds into a $\sigma$-closed$*$ccc forcing. (Note that the example above is axiom $A$, and of the form ccc$*$$\sigma$-closed$*$ccc.) They have also characterized precisely the class of axiom A forcings for which the conjecture holds. Their paper, Baumgartner’s conjecture and bounded forcing axioms, appeared in Annals of Pure and Applied Logic, 164 (12), (2013), 1178-1186.