"Clarithmetic" is a generic name for formal number theories similar to Peano
arithmetic, but based on Computability Logic (see
this http URL) instead of the more traditional
classical or intuitionistic logics. Formulas of clarithmetical theories
represent interactive computational problems, and their "truth" is understood
as existence of an algorithmic solution. Imposing various complexity
constraints on such solutions yields various versions of clarithmetic. The
present paper introduces a system of clarithmetic for polynomial time
computability, which is shown to be sound and complete. Sound in the sense that
every theorem T of the system represents an interactive number-theoretic
computational problem with a polynomial time solution and, furthermore, such a
solution can be efficiently extracted from a proof of T. And complete in the
sense that every interactive number-theoretic problem with a polynomial time
solution is represented by some theorem T of the system. The paper is written
in a semitutorial style, and targets readers with no prior familiarity with
Computability Logic.