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$.



On the definition of $\alpha$-proper poset
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.


