7.1.6 Sidetrack: Calculemus!

A historical motivation of inferencing.

Greek Philosophers like Aristotle already realized that the validity of arguments at a certain level does not depend on any particular circumstances of the world. For example, the argument

``Socrates is human''. ``All humans are mortal''. ``Therefore Socrates will die''.

is valid irrespective of facts such as aging or the inadvisability of accepting drinks from your enemies. As we would put it, this is due to the coincidence between logical consequence and derivability. The only thing that matters is the syntactic form of the argument. Whenever we know `` is .'' and ``All are .'' then we can conclude `` is .''

Calculemus!

Later, in the century the German philosopher Gottfried Leibniz (getting tired about the endless debates of his colleagues about questions like ``how many angels can dance on a pinpoint'') dreamed of a formal language that could express all of natural language (lingua universalis ) and a calculus (calculus ratiocinator ) that could compute all truths of this language. He wanted to be able to call out to his colleagues Calculemus! (let us just calculate who is right).

Today the discovery that syntactic and semantic determination of truth conditions can be equivalent under certain conditions is still considered as one of the great achievements of the human mind.

In fact if one day a committee of aliens lands on planet Earth to determine whether they should just blast it away to make way for a new intergalactic hyper-way, or if the human race is intellectually advanced enough to be worth saving, then we should try to bring this fact to their attention in order to save our planet (provided we're on the welcome comittee).