![\"ptarithmetic\"](\"http:\/\/arxivblog.com\/wp-content\/uploads\/2009\/02\/ptarithmetic.gif\" "\\"ptarithmetic\\"")
<\/p>\n<\/p>\n
In the last few years, a small group of logicians have attempted the ambitious task of re-inventing the discipline of formal logic.<\/p>\n
In the past, logic has been thought of as the formal theory of “truth”.\u00a0 Truth plays an important role in our society and as suchm a formal theory is entirely laudable and worthy. But it is not always entirely useful.<\/p>\n
The new approach is to reinvent logic as the formal theory of computability. The goal is\u00a0 to provide a systematic answer to the question “what is computable”. For obvious reasons,\u00a0 so-called computability logic may turn out to be much more useful.<\/p>\n
To understand the potential of this idea , just think for a moment about the most famous of logical systems called Peano Arithmetic, better known to you and me as “arithmetic”.<\/p>\n
The idea is for computability logic to do for computation what Peano Arithmetic does for natural numbers.<\/p>\n
The role of numbers is played by solvable computations and the collection of basic operations that can be performed on these computations forms the logical vocabulary of the theory.<\/p>\n
But there’s a problem. There can be a big difference between something that is computable and something that is efficiently computable, says Giorgi Japaridze, a logician at Villanova University in Pennsylvania and the inventor of computability logic.<\/p>\n
So he is proposing a modification (and why not, it’s his idea)–the system should allow only those computations that can be solved in polynomial time. He calls this polynomial time arithmetic or ptarithmetic for short.<\/p>\n
The promise is that Japaridze’s system of logic will prove as useful to computer scientists as arithmetic is for everybody else.<\/p>\n
What isn’t clear is whether the logical vocabulary of ptarithemtic is well enough understood to construct a system of logic around and beyond that, whether ptarithemtic makes a well-formed system of logic at all.<\/p>\n
Those are big potential holes which Japaridze\u00a0 may need some help to fill–even he would have to admit that he’s been ploughing a lonely furrow on this one since he put forward the idea in 2003.<\/p>\n
But the potential pay offs are huge which make this one of those high risk , high potential pay off projects that just might be worth pursuing.<\/p>\n
Any volunteers?<\/p>\n