What can be done with computability logic that previous logic systems can't? I've been reading a lot about computability logic lately and I'm superficially aware that it unifies classical, intuitionistic and linear logics.
What I'm seeking to know is:
Can computability logic be used as a foundation for mathematics (or rather arithmetic) in the same sense classical logic has been proposed before by Russell, Whitehead and other authors? Is it subject to the same restrictions (like Gödel theorems) like the other logics (considering that it conservatively extends classical logic)?
I hope I've been clear enough.
References:
http://www.cis.upenn.edu/~giorgi/cl.html
http://www.csc.villanova.edu/~japaridz/ICL.pdf
 A: I would say yes, it can. However, in the research I found that you should take 2 things into account.
First, don't take the Turing-Halting problem as basis. Because, I didn't find a way to directly reason about halting problems. For a proof, you need to hop between the proof-steps. This does not seem to be possible with the halting problem. However, you can take as basis the inequality of 2 computable predicates. If you have p1 and p2 and you write p1 >= p2 when for all x p2(x) => p1(x). Then some reasoning becomes possible.
Second, instead of deterministic functions, you should use non-deterministic (but still computable) functions. Again, there is no practical known way to transform deterministic functions directly into other deterministic functions. However, if you allow non-deterministic functions (as intermediate), then these become possible.
In this way you get a rather simple logic based on computation. Still, if you want to use as the basis of mathematics, you get problems when going to uncountable sets. You are hitting the failure of Hilbert's program, or you should find a way to repair that.
I hope this is somewhat in the direction of the answer you were looking for. 
