Explications in mathematics

Abstract Carnap introduced his notion of explication to arrive at concepts that are precise enough for scientific purposes. As Carnap wants to precisify concepts, his notion of explication targets less precise concepts so that explications within mature mathematics are not possible. We argue that explications of mature mathematical concepts are both possible and widespread. We focus on foundational work, especially as done in the context of interactive theorem proving. Taking foundational work seriously necessitates explicit decisions which are generally ignored in mathematical practice—and such developments are not captured by our usual notions of explication. To see this, we introduce Carnapian and Quinean explication and argue that they are not capable of accounting for intra-mathematical conceptual changes. We argue that these changes are best understood as explications and so need a different notion of explication. We suggest one candidate, called tolerant explication, and sketch how it handles the intra-mathematical cases.