Highly improper forcings

Question

The following question comes from a typo in an old notebook of mine (I changed what I was calling my forcing notion partway through writing the definition of properness):

Say that a forcing $\mathbb{P}$ is pseudoproper iff for all sufficiently large $\theta$, all countable $M\prec H_\theta$, and all $\mathbb{P}$-generic-over-$V$ filters $G$, there is some $\mathbb{Q}\in M$ and some $\mathbb{Q}$-generic-over-$M$ filter $\hat{G}$ such that $M[\hat{G}]=M[G\cap M]$.

For example, the (definitely non-proper) Levy collapse $Col(\omega,\omega_1)$ is pseudoproper. Roughly, given $M$ appropriate, let $\mathbb{Q}$ be the forcing consisting of all (in the sense of $M$) finite partial maps $p:\omega\rightarrow\omega_1\cup\{\perp\}$ which never take on the same ordinal value twice but are allowed to re-use $\perp$. If $G$ is $Col(\omega,\omega_1)$-generic over $V$, then $G\cap M$ gives a partial map $\omega\rightarrow\omega_1$, and "filling in the gaps with $\perp$" gives a $\mathbb{Q}$-generic-over-$M$ (indeed, over $V$) filter $\hat{G}$ which is appropriately equivalent to $G\cap M$.

It's easy to see that pseudoproperness is not preserved by equivalence of forcing notions; a more "annotated" version of the Levy collapse fails to be pseudoproper. This suggests the following strong antithesis of pseudoproperness. Say that a forcing $\mathbb{P}$ is rude if there is no pseudoproper $\hat{\mathbb{P}}$ such that $(i)$ forcing with $\mathbb{P}$ adds a $\hat{\mathbb{P}}$-generic and $(ii)$ forcing with $\hat{\mathbb{P}}$ adds a $\mathbb{P}$-generic.

Question: Do rude forcings exist?

Answer 1

If we allow only for separative forcings $\hat{\mathbb{P}}$ in the definition of rudeness then all non-trivial separative $\sigma$-closed forcings are rude. This does not answer your question literally, but hopefully in spirit.

EDIT: This restriction is not necessary after all, see below.

Suppose that $\mathbb P$ is some non-trivial separative $\sigma$-closed forcing and that $\hat{\mathbb{P}}$ is any separative forcing which is forcing equivalent to $\mathbb P$.

Claim: There is an embedding $\tau\colon 2^{<\omega}\rightarrow\hat{\mathbb{P}}$ so that the pointwise image of any branch through $2^{<\omega}$ has a lower bound in $\hat{\mathbb{P}}$.

This is straightforward to arrange for $\mathbb P$ but to do it for $\hat{\mathbb{P}}$ requires a little bit of care. First as both $\hat{\mathbb{P}}$, $\mathbb P$ are separative forcings, we can consider them as dense subsets $\hat{\mathbb{P}}\subseteq \mathbb B$, $\mathbb P\subseteq\mathbb C$ of complete Boolean algebras. Now $\mathbb B$ and $\mathbb C$ are forcing equivalent so that there are $b\in\mathbb B$ and $c\in\mathbb C$ and an isomorphism $\pi\colon\mathbb B\upharpoonright b\rightarrow\mathbb C\upharpoonright c$. Now choose some $p_\emptyset\in \hat{\mathbb{P}}$, $p_\emptyset\leq b$. If $s\in 2^{<\omega}$ and $p_s$ is defined, then find incompatible $q_{s^\frown 0}, q_{s^\frown 1}\in\mathbb P$ so that $q_{s^\frown i}\leq \pi(p_s)$ and then further find $p_{s^\frown i}\in\hat{\mathbb{P}}$ with $\pi(p_{s^\frown i})\leq q_{s^\frown i}$ for $i<2$. This completes the construction. Set $\tau(s)=p_s$. Clearly if $b$ is any cofinal branch through $2^{<\omega}$ then $\pi[\tau[b]]$ is interlaced with a descending sequence in $\mathbb P$ and thus has a lower bound.

It follows that $\hat{\mathbb{P}}$ cannot be pseudoproper: Suppose $\theta$ is sufficiently large and $M\prec H_\theta$ is countable with $\mathbb P,\tau\in M$. Pick a real $x\in 2^{\omega}$ which codes an ordinal above the ordertype of $M\cap\mathrm{Ord}$ and let $p\in\mathbb P$ be a lower bound of $\tau[\{x\upharpoonright n\mid n<\omega\}]$. $p$ is not in $M$, but if $G$ is $\hat{\mathbb{P}}$-generic with $p\in G$ then $M[G\cap M]$ can define $x$. But $x$ is not definable over $M[\hat{G}]$ whenever $\mathbb Q\in M$ and $\hat{G}$ is $\mathbb Q$-generic-over-$M$ (assuming that $H_\theta$ is a model of sufficiently much of $\mathrm{ZFC}$).

EDIT: Now lets show that there is no pseudoproper $\hat{\mathbb P}$ forcing equivalent to $\mathbb P$ at all: Suppose $\hat{\mathbb P}$ were such a forcing. There always is a some separative $\hat{\mathbb P}'$ and some surjection $\rho:\hat{\mathbb P}\rightarrow \hat{\mathbb P}'$ which preserves the order and so that $p ,q $ are compatible in $\hat{\mathbb P}$ iff $\rho(p), \rho(q)$ are compatible in $\hat{\mathbb P}'$. As before let $M\prec H_\theta$ with $\hat{\mathbb P}, \hat{\mathbb P}', \mathbb P, \rho, \tau\in M$, $x$ be a complicated real, $p\in\mathbb P'$ below $\tau[\{x\upharpoonright n\mid n<\omega\}]$ and $G'$ $\hat{\mathbb P}'$-generic with $p\in G'$. Then $G:=\rho^{-1}[G']$ is $\hat{\mathbb P}$-generic and $M[G\cap M]$ can compute $G'\cap M=\rho[G\cap M]$, so we get a contradiction as before.