Questions about Mitchell forcing and tree property

Question

For $\alpha < \beta$, where $\alpha$ is regular and $\beta$ is measurable, let $M(\alpha, \beta)$ be the Mitchell forcing for making $2^\alpha=\beta=\alpha^{++}$ and forcing the tree property at $\beta.$

Now suppose $\alpha<\beta<\gamma$, with $\alpha$ regular and $\beta, \gamma$ measurable. The product forcing $M(\alpha, \beta) \times M(\beta, \gamma)$ is the natural forcing for making $\alpha^{++}=\beta$ and $\alpha^{+4}=\gamma$ and forcing the tree property at both $\beta$ and $\gamma.$

Question 1. Is it known if the same conclusion works with iteration $M(\alpha, \beta) \ast \dot{M}(\beta, \gamma)$?

If not, then I have the following question ($\alpha < \beta<\gamma$ are supposed to be as above):

Question 2. Is there a forcing notion $P(\alpha, \beta)$ which is $\alpha$-directed closed, $\beta$-c.c. of size $\beta$ such that it forces $2^\alpha=\beta=\alpha^{++}$ also it forces tree property at $\beta$ and such that the iteration $P(\alpha, \beta) \ast \dot{P}(\beta, \gamma)$ makes $2^\alpha=\beta=\alpha^{++}$ and forces the tree property at $\beta.$ (clearly after the iteration tree property holds at $\gamma$, which is supposed to become $\alpha^{+4}$).

Giving references is appreciated.

Answer 1

At least in a variant of Mitchell's forcing, the iteration forces the tree property at both cardinals.

Let $M(\alpha, \beta)$ be the iteration $Add(\alpha, \beta) \ast \mathbb{C}(\alpha, \beta)$ where $p \in \mathbb{C}(\alpha, \beta)$ iff $p$ is a sequence of length $\beta$, with at most $\alpha$ non-trivial coordinates, and $p(\zeta)$ belongs to the collection of names for elements in $Add(\alpha^{+}, 1)^{V^{Add(\alpha, \zeta)}}$. Let $G\subseteq Add(\alpha, \beta)$ be a generic filter. $V[G] \models p \leq q$ iff for every $\zeta < \beta$, $p(\zeta)^{V[G\restriction \zeta]} \leq q^{V[G\restriction \zeta]}$.

The only difference between $M(\alpha, \beta)$ and Mitchell's forcing is that in this model we force at each step "first" with $Add(\alpha^{+}, 1)$ and then with $Add(\alpha, 1)$ and in Mitchell's forcing we use the opposite order.

Let $\alpha < \beta < \gamma$ be regular cardinals, with $\beta$, $\gamma$ measurable (weakly compact is enough, but it is simpler). Let us show that the tree property holds at $\beta$ in the generic extension (the proof for $\gamma$ is easier).

Let $\dot{T}$ be a $M(\alpha, \beta) \ast \dot M(\beta, \gamma)$-name for a $\beta$-tree. By the $\beta^{+}$-distributivity of the $\mathbb{C}$-part of $M(\beta, \gamma)$, $\dot{T}$ is added by $M(\alpha, \beta) \ast \dot{Add}(\beta, \gamma)$. By the chain condition and the homogeneity of $\dot{Add}(\beta, \gamma)$, $\dot T$ is equivalent to an $M(\alpha, \beta) \ast Add(\beta, 1)$-name. Let $\mathbb{Q} = M(\alpha, \beta) \ast Add(\beta, 1)$.

Let $j\colon V\to M$ be an elementary embedding with critical point $\beta$. Let $H\subseteq \mathbb{Q}$ be a generic filter. $$j(\mathbb{Q}) = M(\alpha, \beta) \ast Add(\alpha^{+}, 1) \ast \mathbb{R} \ast Add(j(\beta), 1)$$ for some $\mathbb{R}$.

Since $Add(\alpha^{+},1)$ is equivalent to $Col(\alpha^{+}, 2^\alpha)$ and after forcing with $M(\alpha, \beta)$, $2^\alpha = \beta$, it adds a generic filter for $Add(\beta, 1)$. Thus, we can represent $j(\mathbb{Q})$ in the following way:

$$j(\mathbb{Q}) \cong M(\alpha, \beta) \ast Add(\beta, 1) \ast Col(\alpha^{+}, \beta) \ast \mathbb{R} \ast Add(j(\beta), 1)$$ Using the closure of $Add(j(\beta), 1)$, one can obtain a master condition and force a generic filter $K$ over $M[H]$ such that $H \ast K$ is a generic filter for $j(\mathbb{Q})$ and $j \text{''} H \subseteq H \ast K$. Therefore, in $V[H][K]$ there is an elementary embedding $\tilde{j} \colon V[H] \to M[H][K]$ extending $j$. In particular, $\tilde{j}(\dot{T}^H)$ is $j(\beta)$-tree and thus by taking any element from the $\beta$-th level of $\tilde{j}(\dot{T}^H)$ one can obtain a branch in $\dot{T}$.

Let us show that the forcing $$Col(\alpha^{+}, \beta) \ast \mathbb{R} \ast Add(j(\beta), 1)$$ (that introduced $K$) cannot add a branch to a $\beta$-tree in $V[H]$. Indeed, this forcing is a projection of the product $Add(\alpha, j(\beta)) \times Col^{V^\mathbb{Q}}(\alpha^{+}, j(\beta))$. By standard arguments, this forcing cannot add a branch to a $\beta$-tree in the model $V[H]$.