Recently I got interested in [predicative foundations](https://ncatlab.org/nlab/show/predicative+mathematics), mostly because of Laura Crosilla's work and because Agda employs a predicative type theory.


From the point of view of a predicative foundation to arithmetic, for instance as proposed in [Nelson's book](https://web.math.princeton.edu/~nelson/books/pa.pdf), the consistency of Peano Arithmetic and even of PRA is entirely unclear. From the point of view of a predicative foundation to set theory, such as [CZF](https://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html) or Kripke–Platek set theory, the consistency of impredicative set theories such as IZF, ZF or ZFC is entirely unclear.


**Question.** Impredicative foundations such as PRA or ZF seem to be consistent. I'm wondering whether there are any arguments explaining this apparent consistency from the point of view of predicative arithmetic or predicative set theory. Surely there are no *formalizable* such arguments, since the impredicative systems encompass their predicative analogues, but I'm also interested in informal, philosophical or somewhat vague arguments.


**Analogue.** A mathematician who commits to constructive foundations for philosophical reasons (as opposed to practical reasons) believes that classical systems such as PA and ZF prove lots of falsehoods. Hence the argument "PA and ZF are consistent because their axioms are true, when interpreted to refer to the actual numbers respectively the actual sets" doesn't work for her. But she can still understand why PA and ZF are consistent, since the double negation translation provides embeddings of PA into HA and ZF into IZF. Hence the consistency of classical systems is no deep mystery to her, and because she can also in many cases extract constructive content from classical proofs, she can even appreciate the usefulness of classical systems. I'm looking for similar arguments for "predicative vs. impredicative" instead of "constructive vs. classical".



Explaining the consistency of PRA and ZF from predicative foundations
From the point of view of what you call predicative set theory --- I would say "predicativism given the natural numbers" --- I don't think there are any known arguments for the consistency of ZF, and such a thing seems very unlikely. The proof-theoretic strength of natural predicative theories are quite weak, generally around the level of PA. You can push this up a bit, but in order to show that ZF is consistent you would need proof-theoretic ordinals vastly beyond anything that anyone thinks is predicative.


(The generally accepted ordinal limit of predicative theories is $\Gamma\_0$, but this is incorrect. I do not say "I believe" or "it seems": the analysis that concludes $\Gamma\_0$ is hopelessly wrong. I explain why in [this paper](https://arxiv.org/pdf/1811.03543.pdf).)


I realize that you are only asking for an "informal" argument, but I don't see how that really helps. Looking at the question from the point of view of proof-theoretic ordinals, I think it's clear that ZF is utterly out of reach.


The best a predicativist can do with ZF may just be to assign some credence to its consistency based on the fact that no inconsistency has been found yet. I'm not sure how strongly that evidence should be weighed. It's also true that the consistency of ZF is implied by various, arguably natural arithmetical statements; Harvey Friedman is known for his work on this. Possibly that could be considered more reason to believe consistency.


I want to emphasize, though, that people often talk about consistency as if that is the only thing that matters. Surely, if you are a predicativist, you should care not only about whether ZF is consistent, but also about whether it proves true arithmetical theorems. You want it to be arithmetically sound, not just consistent. For instance, if ZF proves that Turing machine $x$ halts on null input, for some specific value of $x$, we should care about whether this is actually the case. It could well be consistent while proving false statements of this type. I made this point [here](https://arxiv.org/pdf/0905.1680.pdf).


EDIT: in the comments, Ingo Blechschmidt suggests that "(apparent) consistency of impredicative systems is an unexplainable mystery from a predicative point of view". I'd say this is less of a mystery than it seems, when you remember that there have been many formal systems for various types of impredicative mathematics over the years which *did* turn out to be inconsistent. Most notably, the very first, Frege's Grundgesetze.


So instead of saying "Wow, all these formal systems for impredicative mathematics turned out to be consistent, isn't that amazing!" we should say "Wow, all these formal systems for impredicative mathematics turned out to be consistent, except for the ones that didn't. Maybe not so amazing."


