Ptarithmetic

TL;DR

This paper introduces ptarithmetic, a formal system based on computability logic, where formulas represent interactive computational problems solvable in polynomial time, and proves its soundness and completeness.

Contribution

It develops a polynomial time arithmetic system grounded in computability logic, establishing its soundness and completeness for interactive problems.

Findings

Soundness: every theorem corresponds to a polynomial time solvable problem

Completeness: all polynomial time solvable problems are represented by theorems

Effective extraction of solutions from proofs is possible

Abstract

The present article introduces ptarithmetic (short for "polynomial time arithmetic") -- a formal number theory similar to the well known Peano arithmetic, but based on the recently born computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html) instead of classical logic. The formulas of ptarithmetic represent interactive computational problems rather than just true/false statements, and their "truth" is understood as existence of a polynomial time solution. The system of ptarithmetic elaborated in this article 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 effectively 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 self-contained, and can be read without any previous familiarity with computability logic.