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.
Any volunteers?
Ref: arxiv.org/abs/0902.2969: Ptarithmetic
The theory of computability has existed for years. As far as Japaridze’s idea of limiting analysis to polynomial time is a choice to consider a countably infinite set of functions while disregarding the larger and considerable uncountable infinity of functions that are both poly-time and non-poly time. This includes those theories concerned with whether P = NP (no!), for instance. While Japaradize’s idea may lead to formal “truths” as a dual to formal logic, it will be relevant only to those poly-time functions. Its like making rules about Integers when really its all about the real numbers. You have to start somewhere, though.
awesome a homomorphism between peano arithmetic and computability logic. I guess that makes sense since algorithmically even stack turing computers can be bijected to a system of formal logic which can be bijected to a statement in peano arithmetic. That would mean that goedels incompleteness would hold over the computability. Wow with this much already on my mind this is an interesting subject to consider. I want to hear more!
From Goedel inconsistency theorem follows, inside of sufficiently large group of natural numbers the number of mutual connections and dependencies increases up to level, which would require even more numbers and connections for its reasoning.
http://aetherwavetheory.blogspot.com/2009/01/awt-theories-and-gdels-incompleteness.html
“…disregarding the larger and considerable uncountable infinity of functions that are both poly-time and non-poly time…”
Anatraj, there are only countably many (polynomial time or not) computable functions. Because there are only countably many Turing Machines that compute them.
@Zephir
I checked out your website, it’s full of a bunch of nonsense and technical jargon thrown together in an apparent attempt to blind the reader, and awful grammar, mixed with whimsical, irrelevant analogies. In the particular case of your comment here, no, that does not follow at all from Godel’s Incompleteness Theorem. What you are saying is ambiguous, or seems so to me. No, there are no additional dependencies, all the dependencies are laid out in the axioms that define Peano Arithmetic. Yes, there are additional interesting mutual connection such as the prime numbers, however all of these interesting connections are built up from the basic axioms. We define new operations that are distinct and consistent that are based on the axioms to make things more convenient for us, but we could write it out using just the operators and properties used to define the axioms if we really had the desire to. Godel’s work on incompleteness requires self-reference, which is absent in Peano Arithmetic, and doesn’t arise until we define new operations upon the set defined by Peano Arithmetic. Perhaps you are groping towards the fact that the Natural Numbers are not a complete set of the Real Numbers because of the existence of the Division operation, i.e. 4/7 is not a Natural Number?
efficiently verifiable ?
http://en.wikipedia.org/wiki/Logical_positivism
http://en.wikipedia.org/wiki/Verificationism