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.




  • $\begingroup$ I don't know anything about continuous logic. Yet, if---as you say---it is conservative over classical logic (for all first order formulas?) then wouldn't it have to satisfy some form of Gödel's incompleteness theorems? For example, one wouldn't be able to prove new theorems of arithmetic in continuous logic so arithmetic in continuous logic would still be incomplete. Also if it is conservative, couldn't one add the axioms of ZFC to continuous logic to get a foundation for math. (However, maybe I don't know what "conservative" means in this regard, as I don't know the syntax.) $\endgroup$ – Jason Rute Jun 3 '13 at 22:36
  • $\begingroup$ I kept saying "continuous logic" but I meant to say "computability logic". $\endgroup$ – Jason Rute Jun 3 '13 at 22:47

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.