3 added 160 characters in body

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 $\Delta_0$-formula \Pi_1$-formula with$\lambda, M$as parameters so this doesn't increase the complexityeither. 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 Ms \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$\Delta_0$-formula, \Sigma_2$-formula, which is a $\Pi_1$ \Pi_3$formula. Please let me know if this is not correct. 2 added 36 characters in body 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)$. Next the statement$M \prec (H_{\lambda},..)$can be written as a$\Delta_0$-formula with$\lambda, M$as parameters so this doesn't increase the complexity either. 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 Ms \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 '$P$is proper' can be written as$\forall \lambda > 2^{|P|}\sigma(P, \lambda)$with$\sigma$a$\Delta_0$-formula, which is a$\Pi_1$formula. Please let me know if this is not correct. 1 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)$. Next the statement$M \prec (H_{\lambda},..)$can be written as a$\Delta_0$-formula with$\lambda, M$as parameters so this doesn't increase the complexity either. 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 Ms \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 '$P$is proper' can be written as$\forall \lambda > 2^{|P|}\sigma(P, \lambda)$which is a$\Pi_1\$ formula.

Please let me know if this is not correct.