According to constructivism, "it is necessary to find (or "construct") a mathematical object to prove that it exists". There are several formulas to calculate $\pi$, such as:
so I take it $\pi$ exists according to constructivism.
According to finitism, which is a form of constructivism, "a mathematical object does not exist unless it can be constructed from natural numbers in a finite number of steps."
Where does that leave irrational numbers, such as $\pi$? Do they simply not exist according to finitism? How does one reason about the ratio between a circle's circumference and its diameter, if one is working within a finitistic/ultrafinitistic framework?
Best Answer
Primitive recursive arithmetic (PRA), mentioned on the second Wikipedia page to which the question links, is, I believe, generally accepted as an appropriate formalization of finitist foundations. The appropriate way to deal with numbers like $\pi$ when working in this theory would be to use a primitive recursive function that produces (natural number codes for) a sequence of approximations to $\pi$ (with a specified rate of convergence). I'm not sure one could even formulate, in this context, the statement "$\pi$ exists", since the theory's quantifiers range only over natural numbers. That does not, however, prevent one from working with $\pi$ and proving appropriate formalizations (in terms of primitive recursive algorithms) of basic facts about $\pi$.
You shouldn't worry about the problematic "existence" of the ratio between a circle's circumference to diameter, since the "existence" of the circle itself seems just as problematic.
I suspect that, if people want to work in the context of PRA, they actually work in a conservative extension, where many more entities (like $\pi$) are available without making new theorems provable about the original entities (natural numbers) --- just as when most mathematicians work in the framework of ZFC set theory, they don't limit themselves to the primitive notion $\in$ but introduce lots of definitions and abbreviations, and perhaps talk about proper classes (as in NBG class theory).