Assume that $(P,\le)$ is a notion of forcing. There are several ways to define what it means for $P$ being proper and I would like to know: What is the complexity (in terms of the Levy-Hierarchy) of the statement 'P is proper'?



Complexity of the statement 'P is proper'
Properness is observable in any sufficiently large $V\_\alpha$, and therefore has complexity $\Sigma\_2$. In oktan's answer, it suffices to consider sufficiently large $\lambda$, rather than all $\lambda$. I think this is proved in some of the standard accounts of proper forcing.


