Calculus in finitistic systems I was just curious if there were some approaches to prove major theorems of calculus in finitistic systems like PRA?
Some related questions are, e.g.,
https://mathoverflow.net/questions/551/does-finite-math-need-the-axiom-of-infinity
Math without infinity
If all sets were finite, how could the real numbers be defined?
 A: One issue here is the meaning of "finitistic system". $\mathsf{PRA}$ is usually considered a finitistic system, but every model of $\mathsf{PRA}$ is infinite. So the mere presence of an axiom of infinity is not an obstacle for a system to be finitistic.
Also, it is well known that if we let $\mathsf{ZFC}^i$ be $\mathsf{ZFC}$ with the axiom of infinity replaced by its negation, then $\mathsf{ZFC}^i$ is mutually interpretable with Peano arithmetic. Peano arithmetic is not usually considered a finitistic system, and so neither is $\mathsf{ZFC}^i$. Thus just removing the axiom of infinity does not make $\mathsf{ZFC}$ become finitistic.
In Simpson's book, quite a bit of calculus is formalized in a system $\mathsf{WKL}_0$. This system is not itself finitisitic, but it is conservative over $\mathsf{PRA}$ for $\Pi^0_2$ sentences. So, even though $\mathsf{WKL}_0$ is not finitistic, if it proves a sentence of the form that a finitist would recognize, that sentence is finitistically provable (in $\mathsf{PRA}$). This is the sense in which Simpson's book does some calculus in a way compatible with finitism.
To actually do calculus in $\mathsf{PRA}$ or another first-order arithmetic, it would be necessary to represent all the objects in question with natural numbers. The result would be something like a weak form of "Russian-style" computable analysis. That is the school of computable analysis in which all objects are coded by natural numbers. 
