Complexity of the statement 'P is proper' 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'?
 A: 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.
A: I think that I might have found a solution to this rather dispensable question. I will sketch it:
Consider the following characterization of properness:
$P$ is proper iff for all $\lambda > 2^{|P|}$ there is a club $C$ of elementary submodels $M \prec (H_{\lambda},...)$ such that  $\forall p \in P \, \exists q \le p$ ($q$ is $ (M,P)$-generic). The latter statement will be denoted by $\psi(P)$
Now the part ..there exists a club $C$... can be written as $\exists C \in P(H_{\lambda})$ $\varphi(C,...)$, moreover '$C$ is a club' is $\Delta_0$, hence this part doesn't increase the order of $\psi(P)$. Further the formula $x= tc(y)$ is a $\Delta_1$ formula, hence $ C \in P(H_{\lambda})$ is $\Pi_1$.
Next the statement $M \prec (H_{\lambda},..)$ can be written as a $\Pi_1$-formula with $\lambda, M$ as parameters so this doesn't increase the complexity.
Last the statement '$p$ is $(M,P)$-generic' can be written as a formula with paramters $M,P,p$ by the following characterization:
$p$ is $(M,P)$-generic iff $\forall \dot{\alpha}$ $\in M$ $\forall r \le p$ $\exists s \le r$ $\exists \beta \in M$ $s \Vdash \dot{\alpha} = \beta$.
The relation $ s \Vdash \dot{\alpha} = \beta$ is $\Delta_0$ with parameter $P$ hence '$p$ is ($M,P$)-generic' is a $\Delta_0$ formula again.
Thus '..there exists a club $C$...' is $\exists C \in P(H_{\lambda}) \varphi(C,..)$ which is a $\Sigma_2$ formula.
Thus '$P$ is proper' can be written as $\forall \lambda > 2^{|P|}$ $\sigma(P, \lambda)$ with $\sigma$ a $\Sigma_2$-formula, which is a $\Pi_3$ formula.
A: How about the Proper Game formulation?  
$(P, \leq, 1)$ is proper iff 

$\exists
> \Sigma \\ \forall \pi \\ \forall p \in
> P :$  
  
  
*
  
*IF $\forall x \in \pi [x$ is an ordered pair $(x_1, x_2)$, $x_1$ is natural, and $1 \Vdash _P\\ (x_2$ is an ordinal$)]$
  
*THEN $\Sigma (p, \pi)$ is an ordered pair $(q, \sigma)$ such that:
  
*
  
*$\forall y \in \sigma\\ [y$ is an ordered pair $(y_1,y_2)$, $y_1$ is natural, and $y_2$ is an ordinal$]$
  
*$q \in P\\ $ is such that:
  i. $q \leq p$
  ii. $\forall x \in \pi\\ [q\\ \Vdash _P\\ \left ( \exists y \in
> \sigma \right )\left (x_2 =
> y_2\right )] $
  
  

In other words this is saying there's a strategy $\Sigma$ for player II such that for any play from player I, consisting of a condition $p$ and a (partial) $\omega$-sequence of $P$-names for ordinals $\pi$, $\Sigma (p, \pi)$ produces a condition $q$ extending $p$, and a (partial) $\omega$-sequence of ordinals $\sigma$ such that $\forall n \in \mathrm{dom} (\pi),\\ q \Vdash \exists k \in \mathrm{dom} (\sigma) (\pi (n) = \sigma (k))$.
