Recently I got interested in predicative foundations, 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, 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 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".

The Consistency of Arithmetic, gives a variant on Gentzen's proof of the consistency of PA (Theorem 2). One doesn't have to rely on"PA ... [is] consistent because [its] axioms are true, when interpreted to refer to the actual numbers ..."Instead, one has to believe a primitive recursive sequence decreasing sequence of ordinals stabilises. $\endgroup$ – David Roberts Feb 17 at 23:58anyargument (formal or informal) for its consistency convincing. $\endgroup$ – Timothy Chow Feb 18 at 19:13