@David: Yes, Timothy's paper is an excellent survey of the question of the consistency of PA! And Gentzen's proof provides a rich understanding of the consistency of PA for someone who adopts $\text{PRA}+\text{QF-TI}(\varepsilon_0)$ as their metatheory: Firstly, it provides a proof of consistency; secondly, while they still might doubt the truth of theorems of PA, Gentzen's proof still provides them with some meaning to theorems of PA, namely winning strategies in Gentzen's game of reductions.

@cody: CZF + EM = IZF + EM = ZF is a standard fact, see for instance Corollary 4.2.8 in Rathjen and Aczel's book draft.

Just as a short late addendum: The general completeness theorem, stating that consistency is equivalent to having a model (in $\mathrm{Set}$), is indeed not constructively provable. A simple way to see that is that in the effective topos, there is no model of PA, though PA is still consistent (being equiconsistent to HA, which does have a model, namely the naturals (and somewhat amazingly, has the naturals as its only model [van den Berg--van Oosten])). However, for the fragment of predicate logic without $\exists$ and $\vee$, the completeness theorem [Herberlin--Ilik] is constructive.

@aws: The reflection principle seems to be equivalent to $\mathbf{RRS}_2$, the following strengthening of $\mathbf{RRS}$: Let $X$ and $R \subseteq X \times X \times X$ be classes. Assume $\forall x \in X. \forall x' \in X. \exists y \in X. \langle x,x',y \rangle \in R$. Let $A \subseteq X$ be a set. Then there is a set $B$ such that $A \subseteq B \subseteq X$ and such that $\forall x \in B. \forall x' \in B. \exists y \in B. \langle x,x',y \rangle \in R$.

@aws: I now noticed a problem even with the case of existential quantifiers. The proof of Lemma 3.4 only works in the case of a single free variable. I'm trying to fix this by encoding multiple values by tuples, but the naive way doesn't seem to work because we cannot ensure that the partial universe $M$ is closed under pairs.

@aws: Anyway, no matter how not earth-shattering the whole story is, I do think that it deserves to be written up and hence started doing so. You should definitely be coauthor! Please feel free to contact me at [email protected].

@aws: That's a neat trick! I too think that universal quantifiers can be treated with it. By the way, using the equivalent $\mathbf{MDC}$ (Palmgren's multivalued dependent choice) instead of $\mathbf{RRS}$ seems to make the proofs (very slightly) easier, at least for my taste. Regarding $\mathbf{CZF}$: I believe that by now we have used unbounded separation far too often, right? :-) That is, independence of $\mathbf{RRS}$ from $\mathbf{CZF}$ will not immediately help us to settle independence over $\mathbf{IZF}$.

@aws: Thank you for the pointer to $\mathbf{RRS}$! I see that the reflection principle implies $\mathbf{RRS}$. I also see the converse, but only for formulas which don't contain the universal quantifier. Probably you meant to restrict to this class of formulas, right? Yes; I'd also be very much interested in the situation for $\mathbf{CZF}$.

(And upon further reflection, I see that the argument can be simplified to use the reflection principle only once.)

@aws: Yes, that's it, thank you for the reference! And now I think we have a proof that the reflection principle does not hold for $\mathbf{IZF}$: If it would, then by applying the reflection principle twice, in a mostly but not entirely straightforward way (I could provide details if interested), we could show that that IZF proves that DC implies RDC. Which it presumably doesn't, even though, not being particularly familiar with IZF, I don't personally know a model in which DC holds but RDC doesn't.

About the possible mismatch between the object logic and the meta logic: Most of the time this isn't a problem. But sometimes one gets unexpected results. For instance, if we adopt some ultrafinitist meta theory, then we might be in doubt regarding expressions such as $2^{2^{2^{2^2}}}$. However, Peano Arithmetic easily proves that these ultrafinitistic systems verify the existence of these large numbers, essentially by repeating the (ultrafinitistically acceptable) principle "the successor of any number exists" sufficiently (non-ultrafinitistically-acceptably often) often.

A common base system for proving the basic results of the study of formal systems (such as representability of computable functions, the diagonal lemma, Gödel's incompleteness theorems and so on) is ... informal human reasoning! A common formal such system is PRA, primitive-recursive arithmetic.

@aws: Let me add a correction to my previous comment. I stated that dependent choice would be enough. That's not true, because it's not clear that there is a set of suitable sets we could apply choice ot. We'd need some form of choice for iterative non-deterministic constructions of sets.

@aws: I see. We'd need definability, or, failing that, unique existence (among all other candidate sets $C'$ with some property) in order to avoid having to appeal to the axiom of dependent choice. Very interesting! I'll think about this some more.

Excellent question. Have you found out any news since 2015?

@Andrej: Currently only for the empty fragment, that is, not at all; but if a version of Scott's trick could be salvaged (given a class $C$, we need a subset $C'$ with the property that $C'$ is inhabited if $C$ is), then for the fragment not containing the universal quantifier.

Olivia Caramello's book /Theories, Sites, Toposes/ is definitely relevant and contains several examples of the kind you're looking for.