Leibniz and Computing

If you are interested in the history of the philosophical/logical/poetical dimensions of computing, you will be interested in Leibniz, the greater contemporary of Newton who independently created calculus. Martin Davis's astonishing history of just this dimension of the history of computing, titled Engines of Logic, provides fascinating insight into the life and work of Leibniz and its relation with the history of computing. Leibniz is often thought of as the granddaddy of computing.

You will also be interested in Godel's work. The incompleteness theorems. For these suggested an answer in 1930 to a question posed at the turn of the century by Hilbert, a question that is important in the development of the theory of computation. And Turing used Godel's work in his 1933 paper on the 'decision problem' to answer the question and, almost incidentally, introduce the notion of the Turing machine, the theoretical model of a computing device that is still used today.

I picked up an excellent book: Gottfried Wilhelm Leibniz: Philososophical Writings edited by G.H.R. Parkinson. It's actually readable and understandable, neither of which is true of another translation I have of this work by Leibniz.

Anyway, what I wanted to point out tonight is that in the brilliant introduction by Parkinson to this volume, he says that Leibniz thought of what he called the "principle of sufficient reason" as one of his guiding lights.

"Leibniz said many times that reasoning is based on two great principles--that of identity or contradiction, and that of sufficient reason....The principle of sufficient reason says that every truth can be proved..."

Now, it is just this which Godel demonstrates is false. Godel proved the necessary existence, in sufficiently powerful formal systems, of what he called "undecidable propositions", namely ones that are true but not provable. These are ideas that are true for no reason; they're definitely true but definitely not provable. That makes them true for no reason.

It's the necessary existence of these sorts of propositions that complicates the entire structure of human knowledge. Leibniz's principle of sufficient reason is what he needs to lay the foundation for the possibility of machines that reason as far and wide as it is possible to reason, verily and forsooth into a perfectly known and understood universe.

If everything that is true is provable, and if devising proofs can be reduced to a mechanical procedure, then there is no impediment, except possibly time and an infinity of theorems, to a machine generating all the proofs of all the theorems.

Mathematics becomes, in such a world, something that we can leave to a machine.

But Godel showed that not everything that is true is provable (his example was a lot like the proposition "This proposition is not provable."). If not everything that's true is provable, then knowledge, perforce, must always be incomplete. Everything that's true can't be completely exhausted via a theorem-proving machine.

Anyway, it's interesting that Leibniz's "principle of sufficient reason" back in the 17th century, is so strongly related to Godel's work.