In the last few years, a small group of logicians have attempted the ambitious task of re-inventing the discipline of formal logic.
In the past, logic has been thought of as the formal theory of “truth”. 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.
The new approach is to reinvent logic as the formal theory of computability. The goal is to provide a systematic answer to the question “what is computable”. For obvious reasons, so-called computability logic may turn out to be much more useful.
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”.
The idea is for computability logic to do for computation what Peano Arithmetic does for natural numbers.
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.
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.
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.
The promise is that Japaridze’s system of logic will prove as useful to computer scientists as arithmetic is for everybody else.
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.
Those are big potential holes which Japaridze 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.
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.
Ref: arxiv.org/abs/0902.2969: Ptarithmetic