ETHIOPIAN BINARY MATH
Today, a witch doctor practices computer arithmetic. The University of Houston’s College of Engineering presents this series about the machines that make our civilization run, and the people whose ingenuity created them.
The scene is a remote Ethiopian village in 1940. A Farmer offers his herd of 34 goats for sale. One goat is worth, say $7. The villagers don’t know how to multiply, so they call in a shaman. They ask him to set a fair price for the whole herd.
The shaman digs two rows of small holes in the hard dry earth. He reaches into his sack of pebbles and goes to work. He puts 34 stones in the first hole on the left — one for each goat. He puts half that, or 17, in the next — half 17, or 8, in the next — and so on. He keeps dividing by two and dropping the remainder, until the sixth hole has only one stone in it.
Now he goes to the other row. He puts 7 stones — the value of one goat — in the first hole. He puts twice that, or 14 stones in the next hole, and so on. Now his deliberations begin.
He goes down the left-hand side, seeing whether the holes are good or evil. An even number of stones makes the hole evil. An odd number makes it good. Two holes are good. The holes next to them, in the right row, contain 14 stones and 224 stones. He adds those numbers together. The result is the fair market value of the herd. It’s $238.
You and I know about multiplication. So we multiply the number of sheep, by the value of a sheep — 7 times 34. When we do that, we get $238. But that’s just what the shaman got! So what in the world was all the business with the holes? And would he get the right answer with different numbers?
We try it with other numbers. It works every time. So we turn to a mathematician. He says it’s not at all obvious. He puzzles for a long time. Finally he sees it. This Ethiopian shaman has created a remarkable algorithm.
All that business with the holes identifies the numbers in their binary form. That lets the shaman reduce multiplication to simple addition. He’s multiplied just the way a digital computer does. Where did his method come from? How long have his forbears carried this rote tradition?
An anonymous genius lurks somewhere in the haze of his history. So we look at our own multiplication and realize that we too use ritual to find what 7 times 34 is. It makes no more sense to most people who use it than the shaman’s holes. Our multiplication algorithm was also given us by an anonymous genius. He is also lost in rote tradition.
So how do we and that Ethiopian shaman differ? Very little, I reckon. Very little indeed. Of course, I wouldn’t be surprised if he makes fewer mistakes than we do.
I’m John Lienhard at the University of Houston, where we’re interested in the way inventive minds work.
Computers Prove Existence of God
Kurt Gödel proposed an argumentation formalism to prove the necessary existence of God. In a current collaboration we have succeeded to formalise, mechanize and (partly) automate Gödel’s ontological argument with modern higher-order theorem provers on a computer. This work has attracted significant media attention in recent weeks.
Attempts to prove the existence (or non-existence) of God by means of abstract, ontological arguments are an old tradition in Philosophy. Before Gödel, already St. Anselm, Descartes und Leibniz have presented similar arguments. What motivated Gödel as a logician was the question, whether it is possible to deduce the existence of God from a small number of (debatable) foundational axioms and definitions, with a mathematically precise and logically formal argumentation chain.
The core proposition, the necessary existence of God, was divided in our work in four argumentation steps, as proposed by Gödel, and each step was proved and verified with an automated theorem prover. Also the consistency of the axioms and definitions was analyzed and established automatically with the help of a computer.
In theoretical philosophy, formal logical confrontations with ontological arguments had been so far limited to pen and paper. Up to now, the use of computers was prevented, because the “logics” of the available theorem proving systems were not expressive enough to formalize the abstract concepts adequately. Gödel’s proof uses, for example, a complex higher-order modal logic to handle concepts such as “possible” and “necessary”.
Recent works of Benzmüller and Larry Paulson (Cambridge University, UK) show that many expressive logics, including higher-order modal logics, can be embedded into the classical higher-order logic, which can be seen as a universal logic. For this universal logic, efficient automated theorem provers have been developed in recent years, and these systems were now employed in our work on Gödel’s proof.
Our approach opens up new perspectives for a computer-assisted theoretical philosophy. The critical discussion of the underlying concepts, definitions and axioms remains a human responsibility. But the computer can help to avoid mistakes of a logical nature: the computer can check the argumentation chain and partially fulfill Leibniz’ dictum in case of logical disputes: Calculemus — Let us calculate!
Addis Ethiopia Weblog 