Proving that the partial order for adding a dominant real is weakly homogeneous I am trying to prove that the partial order that adds a dominant real is weakly homogeneous. This is listed as exercise IV.4.17 of Kunen's Set Theory (the "new" one).
The details are as follows:

*

*Two elements $p, q$ of a partial order $(\mathbb P, \leq)$ are said to be compatible if there exists $r\leq p, q$ in $\mathbb P$.

*A partial order $\mathbb P$ is said to be weakly homogeneous if for every $p, q \in \mathbb P$ there exists an automorphism $\phi$ of $\mathbb P$ such that $\phi(p)$ and $q$ are compatible.

*The partial order in question is the set $\mathbb P$ of all pairs $(p, F)$ where $p$ is a function into $\mathbb N$ whose domain is a finite subset of $\mathbb N$ (that is, $p \in \text{Fn}(\mathbb N, \mathbb N)$) and $F$ is a finite set of sequences of natural numbers (that is, $F \in [\mathbb N^{\mathbb N}]^{<\omega}$). We say that $(p, F)\leq (q, K)$ iff $p$ extends $q$ as a function, if $K\subseteq F$ and if for all $i \in \text{dom } p\setminus \text{dom } q$ and for all $f \in K$, $p(i)>f(i)$. It is easy to verify that $\mathbb P$ is a partial ordered set whose maximum element is $(\emptyset, \emptyset)$.

I am trying to prove that $\mathbb P$ is weakly homogeneous. I noticed that given $(p, F)$, $(q, K)$, in order to show that $\phi$ exists it is enough to consider the case $\text{dom }p=\text{dom }q$. I tried to "swap" $p$ by $q$ within the whole set (including within the functions $f$'s in the $F$'S). The function $\phi$ that I obtained this way a bijection whose inverse is itself and it carries $(p, F)$ in something compatible with $(q, K)$, but I believe that it is not increasing.
Can someone point me out how to construct such $\phi$?
 A: I don't think this is correct, and in fact, if $\pi$ is an automorphism of $\mathbb{P}$ then $\pi(p)\leq p\leq\pi(p)$ for all $p$, so it couldn't achieve what is desired.
To see this,  let's first replace $\mathbb{P}$ with the forcing-equivalent version $\mathbb{P}'$, given by modding out by the equivalence relation $p\approx q\iff p\leq q\leq p$; if we had an automorphism $\pi$ of $\mathbb{P}$ and $p$ such that $\pi(p)\not\leq p$ or $p\not\leq\pi(p)$, then $\pi$ would induce a non-trivial automorphism of $\mathbb{P}'$. So it suffices to see there are no non-trivial automorphisms of $\mathbb{P}'$. Note that $\mathbb{P}'$ is isomorphic to the forcing $\mathbb{Q}$ with conditions $(f,F)$ where for some $n<\omega$, we have $f:n\to\omega$ and $F:[n,\omega)\to\omega$,
and ordering $(f,F)\leq(g,G)$ iff $f\supseteq g$ and $f(i)\geq G(i)$ for all $i\in\mathrm{dom}(f)\cap\mathrm{dom}(G)$ and $F(i)\geq G(i)$ for all $i\in\mathrm{dom}(F)$.
(Here is a little further explanation as to the isomorphism between
$\mathbb{P}'$ and $\mathbb{Q}$: Given a condition $p=(f,K)\in\mathbb{P}$,
where $f:n\to\omega$ and $K$ is a finite set of functions,
if $K=\emptyset$, then send $p$ to $(f,F_0)\in\mathbb{Q}$, where $F_0$ is the constantly $0$ function (with domain $[n,\omega)$), and if $K=\{g_1,\ldots,g_m\}$ where $m\geq 1$,
send  $p$ to $(f,F)$ where $F:[n,\omega)\to\omega$ and $$F(i)=1+\max(g_1(i),\ldots,g_m(i))$$ for $i\in[n,\omega)$. I have used ``$1+$'' here, and the lower bound function $F_0$, since in the definition of the ordering of $\mathbb{Q}$ I only demand $f(i)\geq G(i)$, not $f(i)>G(i)$, whereas in your definition of $\mathbb{P}$, you use $>$ at the analogous point. It is more convenient for me to have a function always there, so I am forced to use $\geq$ instead of $>$.)
So suppose $\pi:\mathbb{Q}\to\mathbb{Q}$ is an automorphism. We want to see that $\pi=\mathrm{id}$. The plan is to figure out various features
of conditions which must be preserved by $\pi$, until we eventually see that $\pi=\mathrm{id}$. Note that since $\pi$ is an automorphism,
it certainly preserves $\leq$ and compatibility.
Let $\mathbb{Q}_n$ be the set of conditions $(f,F)\in\mathbb{Q}$ such that $\mathrm{dom}(f)=n$.
Claim 1: $\pi``\mathbb{Q}_0=\mathbb{Q}_0$.
Proof: Just note that $p\in\mathbb{Q}_0$ iff $p$ is compatible with every other
condition in $\mathbb{Q}$. Since this property must be preserved by $\pi$, the claim follows.
Claim 2: Let $p=(f,F)\in\mathbb{Q}_{n+1}$. Then $(\emptyset,f\cup F)$
is the $\leq$-least element $p_0\in\mathbb{Q}_0$ such that $p\leq p_0$.
Proof: Easily $(f,F)\leq(\emptyset,f\cup F)$. But if $(\emptyset,g\cup G)\in\mathbb{Q}_0$ where $g:n\to\omega$ and $G:[n,\omega)\to\omega$,
and if $(f,F)\leq(\emptyset,g\cup G)$, then just note that $(\emptyset,f\cup F)\leq(\emptyset,g\cup G)$.
So define $p_0$ from $p$ in this manner for each $p\in\mathbb{Q}$.
By the two claims, the operation $p\mapsto p_0$
is preserved by $\pi$, i.e. $\pi(p_0)=\pi(p)_0$.
Claim 3: Let $p=(f,F)\in\mathbb{Q}_{n+1}$. Then there are exactly
$n$ elements $q\in\mathbb{Q}$ such that $p<q<p_0$.
Proof: If $n=0$, so $\mathrm{dom}(f)=\{0\}$, this just says there are no elements $q\in\mathbb{Q}$
such that $p<q<p_0$, i.e. no $(g,G)$ such that $$(f,F)<(g,G)<(\emptyset,f\cup F).$$
This is straightforward to see. (If $(\emptyset,h\cup H)<(\emptyset,f\cup F)$
where $\mathrm{dom}(h)=\{0\}$ and $H:[1,\omega)\to\omega$, then either $h(0)>f(0)$, or there is some $i\in[1,\omega)$ such that $H(i)>F(i)$, but in either case, then $(f,F)\not\leq(\emptyset,h\cup H)$.
If $n=1$, so $\mathrm{dom}(f)=\{0,1\}$, it says there is exactly one $q\in\mathbb{Q}$ such that $p<q<p_0$, i.e. exactly one $(g,G)$ such that $$(f,F)<(g,G)<(\emptyset,f\cup F).$$
This unique $(g,G)$ is just $g=f\upharpoonright\{0\}$ and $G:[1,\omega)\to\omega$ is $G(1)=f(1)$ and $g(i)=F(i)$ for $i>1$. It is straightforward to see that $(g,G)$ is unique such.
If $n>1$, it is similar; we get the conditions of the form $(g,G)$
where $g=f\upharpoonright\{0,\ldots,i\}$ where $i<n-1$ and $G$ agrees appropriatley with $f$ and $F$.
Claim 4: $\pi``\mathbb{Q}_{n}=\mathbb{Q}_{n}$ for each $n<\omega$.
Proof: This is an immediate consequence of the preceding claims.
Given $p=(f,F)\in\mathbb{Q}$, let $C_{np}=\{q\in\mathbb{Q}_n\bigm|q\text{ is compatible with }p\}$. Since $\pi``\mathbb{Q}_n=\mathbb{Q}_n$,
we get:
Claim 5: $\pi``C_{np}=C_{n\pi(p)}$.
Claim 6: Let $p,q\in\mathbb{Q}_{n+1}$ with $p=(f,F)$ and $q=(f,G)$ (the same first stem $f$). Then $\pi(p),\pi(q)\in\mathbb{Q}_{n+1}$ have a common stem $f'$.
Proof: This follows immediately from the fact that $\pi``\mathbb{Q}_{n+1}=\mathbb{Q}_{n+1}$ and the fact that
$p_0,p_1\in\mathbb{Q}_{n+1}$ are compatible iff the have the same stem. QED (Claim 6).
Since $\pi$ is also surjective, this means that for each $n$,
there is a bijection $\sigma_n:\omega^n\to\omega^n$
which specifies the action of $\pi$ on the stems
of elements of $\mathbb{Q}_n$, i.e. if $(f,F)\in\mathbb{Q}_n$ then $\pi(f,F)=(\sigma_n(f),F')$ for some $F'$.
Claim 7: $\sigma_n=\mathrm{id}$ for each $n$.
Proof: Suppose not and let $n$ be least such that $\sigma_n\neq\mathrm{id}$.
Let $i<n$ be least such that for some $f\in\omega^n$, we have $\sigma_n(f)(i)\neq f(i)$. Let $m<\omega$ be the least possible value of $f(i)$ where $f$ is such.
Now suppose $i=n-1$. Since $\sigma_n$ is a bijection, we can find $g\in\omega^n$ such that $\sigma_n(g)=f$. By the minimalities, $g\upharpoonright n-1=f\upharpoonright n-1$ and $g(n-1)\geq f(n-1)$. Suppose $g(n-1)>f(n-1)$. Let $p\in\mathbb{Q}_n$ with $p=(f,F)$ and $q\in\mathbb{Q}_n$ with $q=(g,G)$ (for some $F,G$).
So $\pi(p)=(\sigma_n(f),F')$ and $\pi(q)=(\sigma_n(g),G')$ for some $F',G'$.
Note that because $g\upharpoonright n-1=f\upharpoonright n-1$ and $g(n-1)>f(n-1)$,
we have $C_{0p}\subsetneq C_{0q}$. Therefore by Claim 5, $C_{0\pi(p)}\subsetneq C_{0\pi(q)}$.
But because $\sigma_n(f)\upharpoonright n-1=f\upharpoonright n-1=\sigma_n(g)\upharpoonright n-1$
and $$\sigma_n(f)(n-1)>f(n-1)=\sigma_n(g)(n-1),$$ we actually have
$C_{0\pi(q)}\subsetneq C_{0\pi(p)}$, contradiction. So $g(n-1)=f(n-1)$.
But then with $p,q$ as before, we have $C_{0p}=C_{0q}$, so again by Claim 5,
$C_{0\pi(p)}=C_{0\pi(q)}$, but this gives a contradiction much like before.
So $i<n-1$.
Let's define, for $k<\omega$ and $p\in\mathbb{Q}$,
$$D_{kp}=\{q\in\mathbb{Q}_k\bigm|\exists q'\in\mathbb{Q}_k\ [q,q'\text{ have the same stem and }q'\text{ is compatible with }p]\}.$$
We know that  $q,q'\in\mathbb{Q}_k$ have the same stem iff $\pi(q),\pi(q')$ have the same stem. So $\pi``D_{kp}=D_{k\pi(p)}$.
Now by minimality of $n$, $\sigma_{i+1}(f')=f'$ for all $f'\in\omega^{i+1}$.
Let $p=(f,F)\in\mathbb{Q}_n$ be such that $\sigma_n(f)(i)\neq f(i)$. We have $\sigma_{i+1}(f\upharpoonright(i+1))=f\upharpoonright(i+1)$. Note that
for $q\in\mathbb{Q}_{i+1}$, there is $q'\in\mathbb{Q}_{i+1}$
with the same stem as $q$ and with $q'$ compatible with $p$,
iff the stem of $q$ is $f\upharpoonright(i+1)$. That is, with the notation just introduced above, $$D_{i+1,p}=\{(f',F')\in\mathbb{Q}_{i+1}\bigm|
f'=f\upharpoonright(i+1)\}.$$ So $D_{i+1,\pi(p)}=\pi``D_{i+1,p}=D_{i+1,p}$,
since $\sigma_{i+1}=\mathrm{id}$. But since $\sigma_n(f)(i)\neq f(i)$,
this is impossible, i.e. in fact $$D_{i+1,\pi(p)}=\{(f',F')\in\mathbb{Q}_{i+1}\bigm|f'=\sigma_n(f)\upharpoonright(i+1)\}\neq D_{i+1,p}.$$
Contradiction. QED (Claim 7)
Claim 8: $\pi=\mathrm{id}$.
Suppose not and let $n$ be least such that $\pi\upharpoonright\mathbb{Q}_n\neq\mathrm{id}$. Since $\sigma_n=\mathrm{id}$, for each $(f,F)\in\mathbb{Q}_n$ we have $\pi((f,F))=(f,F')$
for some $F'$. Let $m$ be least such that for some $p=(f,F)\in\mathbb{Q}_n$,
letting $p'=(f,F')=\pi((f,F))$, we have $F'(m)\neq F(m)$.
Note that (since $F'(m)\neq F(m)$) we have $C_{m+1,p}\neq C_{m+1,p'}$, and in fact the set of stems
of conditions in $C_{m+1,p}$ is distinct from the set of stems of conditions in $C_{m+1,p'}$. But $\pi``C_{m+1,p}=C_{m+1,p'}$ and since $\sigma_{m+1}=\mathrm{id}$,
$\pi\upharpoonright\mathbb{Q}_{m+1}$ preserves stems, and therefore
the set of stems in elements of $C_{m+1,p}$ is the same as those in $C_{m+1,p'}$,
contradiction. QED.

Edit: However, a weaker but related condition does hold for $\mathbb{Q}$:
Below every condition $p\in\mathbb{Q}$, the forcing below $p$,
i.e. the suborder with conditions $\{q\in\mathbb{Q}\bigm|q\leq p\}$, is isomorphic to $\mathbb{Q}$. This is enough to get, for example, that statements about elements of the ground model are all decided by the top condition.
