Hilbert's Question and Proof Systems

     In the year 1900 David Hilbert asked (among a set of 23 questions/problems) if there is a program that takes as input any given statement and decides whether it is true or not, i.e, it should output either a true or false. This will immediately bring to our mind the questions about automated reasoning,artificial intelligence pattern recognition and such other themes. However the above mentioned question came up in the context of mathematical logic and one should keep in mind the kind of computational power we had back then in the early 1900’s. In Mathematics we generally deduce statements from a set of axioms or priorly ascertained facts. So one can imagine feeding a database of mathematical facts and their interrelations and from this create a system to check whether a certain mathematical statement or conjecture is true or false. So we shall call this elusive procedure demanded by David Hilbert as ‘Hilbert’s program’. In fact a famous result in Mathematics namely the the four color problem was approached in a similar fashion.

It was K. Godel and A. Turing who showed the way toward solving Hilbert’s question and finally it was known that there were logical obstructions to get the Hilbert’s program. Godel showed that the axioms of arithmetic on which proof systems depend sometimes lead to paradoxes thus asserting that there is the so called Incompleteness in logical reasoning. Well Godel and Turing worked independently under different contexts but essentially came to the same conclusion. For more on this one can read [1].

However an Indian origin scientist Madhu Sudan developed the so called probabilistically checkable proof system which uses probability theory to check the correctness of a given proof. The crux of the matter lies in his PCP Theorem (probabilistically checkable proof theorem) for which he was awarded the Rolf Nevanlinna prize in 2002.The PCP theorem says that for some universal constant K, for every n, any mathematical proof of length n can be rewritten as a different proof of length poly(n) that is formally verifiable with 99% accuracy using a randomized algorithm.

[1] H. Ramesh, V. Vinay “Who will win the toss?” Resonance Journal of Science Education, April 1998.
ALSO AVAILABLE ON MY CONNECTRONIX BLOG