Complexity of the statement 'P is proper'

Question

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'?

Answer 1

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.

Answer 2

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.

Answer 3

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:
  1. $\forall y \in \sigma\\ [y$ is an ordered pair $(y_1,y_2)$, $y_1$ is natural, and $y_2$ is an ordinal$]$
  2. $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))$.