A post on comp.theory newsgroup referred to this paper, by Giorgi Japaridze. I read a bit of this paper, and believe the thoughts presented here are quite promising (at least, I found the goal of this study quite ambitious). I guess, people with interest in computer logic might find this interesting.
This paper introduces ptarithmetic (short for "polynomial time arithmetic") - a formal number theory similar to the well known Peano arithmetic, but based on the recent, computability logic instead of classical logic.
The arithmetic primitives defined in this theory, compute in polynomial time (as against classical logic, operations in which can compute in exponential or combinatorial time).