A supercompact cardinal can be forced to give PFA

By F2 fix a Laver function and form $P_{\kappa }$ as in F6. By F3 this forcing is proper, preserves ${\omega }_1$, and forces $\kappa ={\omega }_2$. Let $G\subseteq P_{\kappa }$ be arbitrary $V$-generic. F4 gives $V[G]\models \mathrm{Z}\mathrm{F}\mathrm{C}$. It remains to prove PFA in this arbitrary extension.

Work in $V[G]$. Fix a nonempty proper partial order $Q$ and a family $⟨D_{\xi }:\xi <\lambda ⟩$ of dense subsets, where $\lambda \le {\omega }_1$. If $\lambda =0$, any $q\in Q$ generates a filter and there is nothing to meet. Suppose $0<\lambda \le {\omega }_1$ and repeat $D_0$ to regard the family as an ${\omega }_1$-sequence. Choose ground names $\dot{Q},\dot{\vec{D}}$ for these objects. By F5 there is $p\in G$ forcing that $\dot{Q}$ is proper and that $\dot{\vec{D}}$ is an ${\omega }_1$-sequence of dense subsets of it. Restrict every coefficient of $\dot{Q}$ below $p$ and adjoin a new greatest condition, obtaining a name ${\dot{Q}}^{\ast }$. In a generic containing $p$ its value is $Q$ with that new top; in a generic on the incompatible side its value is the one-condition order. Adding a top preserves properness: an old condition uses a $Q$-master, while below the new top a countable model containing the nonempty $Q$ contains an old condition and a $Q$-master below it. The set of conditions below $p$ or incompatible with $p$ is dense, so F5 shows that $1_{P_{\kappa }}$ forces ${\dot{Q}}^{\ast }$ to be nonempty, proper, and to have a greatest condition. In the actual extension every $D_{\xi }\subseteq Q$ remains dense in $Q^{\ast }$.

Choose a cardinal large enough for the names in step 2.1 and all restrictions of the desired embedding to them. Laver anticipation and supercompactness give a correspondingly closed $j:V\to M$ with critical point $\kappa$ and $j(\mathrm{\ell })(\kappa )={\dot{Q}}^{\ast }$. By step 2.1 and F6 the image iteration uses ${\dot{Q}}^{\ast }$ at stage $\kappa$, and F3 gives in $M$ a tail name $\dot{R}$ and a canonical dense factorization $j(P_{\kappa })\simeq P_{\kappa }\ast {\dot{Q}}^{\ast }\ast \dot{R}\mathrm{.}$

By the outer-universe convention in Given, take $g\subseteq Q^{\ast }$ generic over $V[G]$, followed by an $M[G\ast g]$-generic $H\subseteq R$, all in a common outer universe. Under the factorization let $K=G\ast g\ast H$. Every condition of $G$ has countable, hence bounded, support in $\kappa$; the canonical first factor therefore sends it into $K$, so $j\mathrm{‘}\mathrm{‘}G\subseteq K$. Define $j_G({\mathrm{val}}_G(\tau ))={\mathrm{val}}_K(j(\tau ))\mathrm{.}$ If two $P_{\kappa }$-names have the same $G$-value, F5 gives a condition of $G$ forcing their equality; its image belongs to $K$, so F5 in $M$ makes the displayed definition independent of the name. The same argument, applied to a formula or its negation, proves formula-by-formula that $j_G:V[G]\to M[K]$ is elementary and extends $j$.

Enumerate in $V$ the transitive closure of the name ${\dot{Q}}^{\ast }$ below the closure bound chosen in step 3.1. Closure puts the pointwise image of that enumeration in $M$, and evaluating it with $G$ and $K$ constructs the set restriction $j_G\upharpoonright Q^{\ast }$ in $M[K]$. There form the upward-closed filter $F$ generated by $j_G\mathrm{‘}\mathrm{‘}g$. It is directed because $g$ is directed and $j_G$ preserves the order. Since $\mathrm{crit}(j_G)=\kappa >{\omega }_1$, $j_G(⟨D_{\xi }:\xi <{\omega }_1⟩)=⟨j_G(D_{\xi }):\xi <{\omega }_1⟩\mathrm{.}$ For every $\xi <{\omega }_1$, genericity gives $q_{\xi }\in g\cap D_{\xi }$, and $j_G(q_{\xi })\in F\cap j_G(D_{\xi })$. Thus $M[K]$ satisfies that a filter on $j_G(Q^{\ast })$ meets every member of the image sequence. Elementarity of $j_G$ reflects the existential assertion to a filter $f$ on $Q^{\ast }$ in $V[G]$ meeting every $D_{\xi }$. Because the sequence is nonempty and every $D_{\xi }$ lies in $Q$, $f\cap Q$ is nonempty; it is upward closed in $Q$, and any common extension in $f$ of two of its members lies in $Q$, not at the newly adjoined greatest condition. Hence $f\cap Q$ is the required filter on $Q$.

The choice of $Q$ and its dense family in $V[G]$ was arbitrary, including the empty-family case, so F1 and step 5.1 give $V[G]\models \mathrm{P}\mathrm{F}\mathrm{A}$. Since $G$ was an arbitrary generic, F5 yields $P_{\kappa }⊩\mathrm{P}\mathrm{F}\mathrm{A}$. Step 1.1 and F3 give preservation of ${\omega }_1$ and $P_{\kappa }⊩\kappa ={\omega }_2$, while F4 gives preservation of ZFC. All uses of Choice are those declared in A1; the outer generics facilitate the semantic argument and are not claimed to be elements of $V[G]$.