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 LevyHierarchy) 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. 


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. 


How about the Proper Game formulation? $(P, \leq, 1)$ is proper iff
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))$. 

