On the definition of $\alpha$-proper poset

Question

I am reading Uri Abraham's chapter on Proper Forcing in the Handbook of Set Theory and I have a quite trivial question on the definition of $\alpha$-proper forcing. Since there are many equivalent definitions and characterizations, let me recall those related to my question.

If $\lambda$ is a fixed regular cardinal and $\alpha>0$ a countable ordinal, an $\alpha$-tower is a sequence $\left<M_i\mid i<\alpha\right>$ of elementary substructures of $H_\lambda$ such that $M_\delta=\bigcup_{i<\delta}M_i$ when $\delta$ is a limit ordinal and $\left<M_i\mid i\leq j\right>\in M_{j+1}$.

A poset $P$ is $\alpha$-proper if for every sufficiently large $\lambda$ and every $\alpha$-tower such that $P\in M_0$, every $p\in M_0$ can be extended to a condition $q$ which is $(M_i,P)$-generic for each $i<\alpha$.

Among the characterizations of $\alpha$-properness, there is the following one:

Let $T^\alpha(P)$ the set of all sequences $\{a_i\mid i<\alpha\}$ of countable subsets of $A=P\cup \mathcal PP$ such that every $p\in a_0\cap P$ can be extended to $q\in P$ such that if $D\in a_i\cap \mathcal PP$ dense in $P$ then $D\cap M_i$ is pre-dense below (or above) $p$.

$(*)$ $P$ is $\alpha$-proper iif $T^\alpha(P)\in \mathcal D^\alpha(A)$ (a generalization of the club-filter for sequences of countable subsets).

In Proper and Improper Forcing, Shelah requires $i\in M_i$ in the definition of $\alpha$-tower, Abraham does not include this, but I have needed an even stronger hypothesis in order to prove that $(*)$ implies $\alpha$-properness, namely, that $\alpha\in M_0$.

I see that it is not relevant, since what really matters is that the set of all $\alpha$-towers satisfying the definition of $\alpha$-proper poset belongs to $\mathcal D^\alpha(H_\lambda)$ (and this is an easy consequence of the proof of this characterization), but I have been wondering whether $(*)\Rightarrow \alpha$-proper can be shown without restricting the definition to $\alpha$-towers satisfying $\alpha\in M_0$.

The idea of the proof is to show that $\{M_i\cap A\}_{i<\alpha}\in T^\alpha(P)$, and I need $\alpha\in M_0$ to guarantee that $T^\alpha(P)\in M_0$.

Answer 1

Does a proof by contradiction work here?

Your (*) is stated as a theorem and not a hypothesis, so I am assuming by $(*)$ you really mean the right-hand side. Since it depends on $\alpha$, I'll call it $(*)_\alpha$.

Given $P$, we want to see that $(*)_\alpha$ implies $\alpha$-proper for all $\alpha<\omega_1$. If this fails, let $\alpha$ be the least witness. Now given a tower of models with $P\in M_0$, we get $\alpha\in M_0$ automatically, as it is definable from $P$, etc.

Now your proof should give a contradiction.