Foundations without axiom schema of replacement

Question

The axiom schema of replacement seems, to me, the least intuitive of the axioms of ZFC. Further, it seems that, at least according to the wikipedia page, most of the applications are in set theory proper. As such it doesn't seem like we'd lose much in "ordinary mathematics" if we dropped it. Further, the previous page seems to suggest that (ZFC - replacement) is "more consistent" than ZFC (i.e. ZFC implies consistency of (ZFC - replacement)), so this seems like a clear advantage. What is the states of (ZFC - replacement) as a foundational system? What would we lose in "ordinary mathematics" if we didn't have replacement?

Answer 1

This is an issue of two different perspectives "talking past each other."

$\mathsf{ZFC}$ is indeed massively overshooting what we actually need for "concrete" mathematics (I disagree with the use of "ordinary" mathematics in this context). But that's part of the point (well, that's ahistorical; rather, it has emerged as part of the appeal). By settling on such a strong theory as $\mathsf{ZFC}$ as our "default" theory for mathematics, we save mathematicians a lot of effort: it's easy to convince oneself that a given "natural-language" proof actually translates into $\mathsf{ZFC}$ - or more accurately, that if there is a serious issue re: fully formalizing that natural-language proof, it's not related to $\mathsf{ZFC}$ but rather reflects a genuine ambiguity/gap/error in the natural-language argument itself.

The question of what foundations are actually needed for various parts of mathematics is however an extremely interesting one. The relevant topic is reverse mathematics, and broadly speaking I'd say that the theory $\mathsf{ACA_0}$ is the "right" one for most contexts. For example, despite its extreme complexity it's generally believed that the proof of Fermat's Last Theorem can be modified to go through in $\mathsf{ACA_0}$. And this is well below $\mathsf{Z}$ (= $\mathsf{ZFC}$ without choice or replacement) in power.

That said, there are arguably concrete results which require serious axiomatic strength - this has been most intensively studied by Harvey Friedman (e.g. with Boolean relation theory). The relevant statements are fairly innocuous-seeming combinatorial principles. Now contra Friedman I don't actually find these statements particularly natural, and I think this is a common stance, but certainly his work points towards a real possibility that we may eventually find ourselves grappling with set-theoretic principles - at least up to consistency strength - in even very concrete questions.

Answer 2

Disclaimer: I'm not qualified to answer this question. Having said that, this paper seems relevant; I especially found the following quote stimulating, although it only addresses whether replacement is "intuitive", rather than its relevance to "ordinary mathematics".

Replacement can be seen as a crucial bulwark of indifference to identification, in set theory and in modern mathematics generally. To describe a prominent example, several definitions of the real numbers as generated from the rational numbers have been put forward — in terms of the geometric continuum, Dedekind cuts, and Cauchy sequences — yet in mathematical practice there is indifference to actual identification with any particular objectification as one proceeds to work with the real numbers. In set theory, one opts for a particular representation for an ordered pair, for natural numbers, and so forth. What Replacement does is to allow for articulations that these representations are not necessary choices and to mediate generally among possible choices. Replacement is a corrective for the other axioms, which posit specific sets and subsets, by allowing for a fluid extensionalism.