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