Saturday, May 31, 2008
APAL paper: A sequent calculus for limit computable mathematics
Stefano Berardi and I co-authored a paper appeared Annals of Pure and Applied Logic.
A sequent calculus for limit computable mathematics
You need register ScienceDirect to read the article. If you are interested the article but do not have the access right, please write to me (yoriyuki.y@gmail.com). Then, I send a personal copy. The article is a part of the special issue dedicated "Classical Logic and Computation 06" held in
The purpose of the article is to give a sequent calculus which is sound and complete formulation of limit computable mathematical (LCM for short). Surprisingly, if we remove Exchange rule (changing order of formulas in sequents) from infinitary sequent calculus for classical logic, we obtain sequent calculus for LCM. This is the first formal (albeit infinitary) system for LCM, since previously LCM was defined by semantics (realizability or games).
But, what is LCM? Now, let me explain the motivation behind LCM first. There are thoughts called "intuitionism", or "constructivism". For "ordinal" mathematics, proofs are exercise to establish the truthness of the conclusion. In a sense, the focus is on statements established by proofs, not proofs themselves. "Intuitionism” or "constructivism” argues that proofs themselves have meaning as a "guidance" to establish "intuition" of statements. Using modern computer science word, proofs are programs which output "direct evidence" of statements.
Mathematics based on intuitionism has rich structures, and applied to automatic program derivation from proofs. Yet, it has a draw back that it invalidates an important logical principle called Excluded Middle. Excluded Middle states that for any statements “A”, “A” holds or “not A” holds. Intuitionism rejects Excluded Middle because there is no general way to construct intuition of either “A” or “not A”, since if it is possible, there is a decision procedure of truthness of statements of the given languages, which is generally not the case.
However, this draw back is serious draw back since Excluded Middle is heavily used in “ordinal” Mathematics.
Here comes LCM comes to rescue. LCM allows limited form of Excluded Middle, that is, existential statements for decidable properties. Yet, its proofs have a meaning as a “learning process” of evidence of statements. Unlike intuitionism, proofs of LCM do not construct evidence of statements directly. Instead, they output infinite stream of “guess” of the correct evidence, and reach the correct answer after finite (but unpredictable numbers of) steps. Difference here is that in LCM, there is no general way to know whether proofs construct the correct evidence already or not. Only we can know sure that proofs reach the correct evidence after infinite step, hence they are called “limit” computable.
Unfortunately, before our article, there is no simple syntactic description of correct inferences in LCM. Correct inferences of LCM were defined as proofs which allow interpretation as learning processes. Later, characterization using game semantics is found, which is greatly related to our article. In fact, our article proves not just soundness and completeness, but formal proofs of our system are isomorphic to winning strategies of game interpretation of its conclusion. There is some subtlety here. What “isomorphic” means? This is the reason that we had to rewrite the article. I do not content the final formulation appeard in the APAL paper either. I would love suggestions from the readers.
