Derived Models in PFA

We discuss a conjecture of Wilson that under the proper forcing axiom, ${\mathrm{\Theta }}_0$ of the derived model at $\kappa$ is below ${\kappa }^{+}$. 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 $\mathrm{\Theta }<{\kappa }^{+}$ in the case of the old derived model, and under additional hypotheses for the new derived model.