Derived Models in PFA

We discuss a conjecture of Wilson that under the proper forcing axiom, $Θ_0$ of the derived model at $κ$ is below $κ^+$. We prove the conjecture holds for the old derived model. Assuming mouse capturing in the new derived model, the conjecture holds there as well. We also show $Θ< κ^+$ in the case of the old derived model, and under additional hypotheses for the new derived model.