Abstract:
In this talk I will describe a formal system of infinitesimal analysis that is weak in proof-theoretic terms, yet it is strong enough to formalize a significant fragment of classical real analysis. The system, called Elementary Infinitesimal Analysis (EIA), has the property that the computational time bounds of its provably computable functions on the natural numbers are given by exponential terms. On the other hand, EIA can prove important theorems of classical real analysis; we show, as an example, that the existence theorem for ordinary differential equations, in the language of infinitesimal analysis, can be directly carried out in EIA. Moreover, EIA uses infinitesimals and infinite numbers in a simple and natural way so that proofs in this system are straightforward to construct and comprehend.

Back to Talks Page