Formal systems needed to formalize relative independence results We know that Con(ZF) implies Con(ZFC+GCH), Con(ZF+neg(AC)) and Con(ZFC+neg(CH)).  But what are some weak theories in which these relative independence results are provable? In particular, are they provable in PA and even in some interesting proper subtheories of PA?  Are there similar relative independence results whose proofs require more than PA or even ZFC?
 A: Independence results such as the ones mentioned that can be proved using basic syntactic methods (relative interpretation, forcing) can be formalized in the theory $\mathit{PV}_1$ (also known as $T^0_2$, $\mathit{VP}$, and the $\forall\Sigma^b_1$-fragment of $S^1_2$): it has function symbols for all polynomial-time algorithms introduced by means of Cobham’s limited recursion on notation, and it can be axiomatized by definitional equations for the functions, a form of quantifier-free induction, and something to the effect of $0\ne1$ and $x\le1\to x=0\lor x=1$. This theory is as weak as it gets among usable fragments of arithmetic: it is interpretable in Robinson’s arithmetic $Q$ on a definable cut. It is included in $I\Delta_0+\Omega_1$, and a fortiori in stronger fragments of PA.
I should perhaps clarify how one deals with forcing, as it is conceptually a model-theoretic method. Let me take $\mathrm{Con}(\mathit{ZFC})\to\mathrm{Con}(\mathit{ZFC}+\neg\mathit{CH})$ for concreteness. In ZFC, you can define the relevant Cohen algebra $B$, and build the Boolean-valued universe $V^B$. In particular, for each formula $\phi(x_1,\dots,x_n)$, you can construct a definable function $\|\phi\|\colon(V^B)^n\to B$ that gives the truth value of $\phi$ in the Boolean universe. Then, in $\mathit{PV}_1$, you prove $\forall\phi\,(\mathit{ZFC}+\neg\mathit{CH}\vdash\phi\Rightarrow\mathit{ZFC}\vdash\|\phi\|=1)$ by induction on the structure of the proof.
There are some more demanding relative consistency results: in particular, the consistency of GB relative to ZF, or of $\mathit{ACA}_0$ relative to PA, rely on cut elimination; they are provable in $I\Delta_0+\mathit{SUPEXP}$, but not in $I\Delta_0+\mathit{EXP}$. This is still nowhere near as strong as PA or ZFC. I can’t recall any examples of the latter sort, and somewhat suspect that in most cases, if your relative consistency required such a strong theory, you could as well make it an absolute consistency result.
