In the last installment of this column, I promised to discuss properties of the duplicating gremlin G - a model for self-reference and recursion. In the meantime something fascinating has come up. I shall postpone the gremlin for now.
This column is devoted to a discussion of the relation between computer proof and human proof. It is a discussion of the relationship of persons and machines.
Can a computer discover the proof of a theorem in mathematics? Some would say that this is certainly possible, since the computer has only to find the right steps. After all, proving a theorem is like solving a problem in chess, and we are all aware that computers can play quite a good game of chess. On the other hand, I say that a proof is not a proof until a person is convinced by it. In fact a mathematical proof is exactly an argument that is completely convincing to a mathematician! In this sense, a computer does not, can not produce a proof.
The computer is not convinced of anything. The computer is set to search for something - a certain series of steps according to some rules. The computer can indicate the state desired by its programmers. It does not know the proof. It only finds the steps.
It is a human judgment that propels the result of the computer’s search into a statement that the computer has "found a proof". Indeed the computer has helped us and it has found something that we can examine. If we judge that to be a proof, then it is a proof (for us). How do we judge?
This last question is the real question about proof. How do we know when we have a proof? It is too big a question from many angles. One view on it will come forth as we look at a specific problem.
Quite recently a computer program at Argonne National Labs in Argonne, Illinois found a proof for a famous unsolved problem in Boolean algebra, known as the Robbins Problem. (Incidentally, Robbins is the name a mathematician Herbert Robbins, who introduced the problem. We shall not use an apostrophe on the "s" in Robbins when we say the Robbins problem). The problem can be elegantly stated, and we shall state it. But first a story:
A computer proof of the Robbins Problem was completed on October 10, 1996 by a program named "EQP". The proof was successfully verified by another program named "Otter". It was already known that it would be sufficient for the computer to deduce a certain equational pattern from the Robbins Axioms. EQP succeeded in locating this form. The computer output of the final demonstration is not long, but it contains many formulas that are exceedingly difficult for a human being to read. For example, one line of the proof reads:
~(~(~(~(~(X)+X) + ~(~(X) + X) + X+X+X+X) +~(~(~(X)+X)+X+X+X)+X)+X) = ~(~(~(X) + X)+~(~(X)+X)+X+X+X+X).
This run on the Robbins problem was initiated by William McCune, a PhD mathematician and member of a group of researchers in automated theorem proving at the Argonne Labs. The head of the group is Larry Wos. Credit for the initiative goes to Dr. McCune and to the team who set the computer on the track of the problem.
It might seem that the demonstration of the Robbins Problem by the program EQP is out of human reach. This is not so! It is possible to change the representation of the problem in such a way that a human can check the proof and even appreciate the form of reasoning used by EQP. In fact, this mode of representation creates an arena in which one can continue the investigation either by hand, or with the aid of the computer.
EQP’s human guides were asked how they knew the demonstration was correct. Their very good answer is that, along with checking it by hand, they set another program (Otter) to checking and rederiving EQP’s results and that it is confirmed. I was very curious about this and found their web page [M]. There, reproduced, were the output lists of EQP and Otter. Could a human being follow the proof? I decided to give it a try. The first part of this task, entailed a simplification and translation of the notation used by the computer. It is very difficult for a human being to keep track of nested parentheses, but not too hard to look at patterns of nested boxes. Accordingly I translated the steps in the proof into a nested box notation. I had previously worked on the Robbins problem using this notation [K].
The translation of EQP’s proof was not trivial. I had to find derivations of the statements in the EQP proof. These were not given, just the sequence of propositions leading to the final result. It is possible to humanly comprehend the EQP proof! If you are interested in the details see my web page [KW] and the article therein on Robbins Algebra.
It is quite fascinating to contemplate the present situation. EQP produced a proof that could have been inaccessible to human beings but is certainly understandable to us with a little effort in communication. EQP’s proof is much more than a calculation. The proof depends upon a successful search among a realm of possibilities and the skillful application of pattern recognition and the application of axioms. This is very close to the work of a human mathematician. EQP, being able to handle many possibilities and great depths of parentheses has an advantage over her human colleagues. I understood EQP’s proof with an enjoyment that was very much the same as the enjoyment that I get from a proof produced by a human being. Understanding a proof is like listening to a piece of music - or like improvising a piece of music from an incomplete score.
Some dark thoughts arise. In the instance of the Robbins problem, the computer demonstration is just barely comprehensible to humans. What will happen next? Should we expect proofs by computers that are forever beyond human understanding? Can such structures be legitimately considered to be proofs? What will happen to mathematics if major theorems are "proved" by machines with proofs that cannot be understood by humans? I will leave you to contemplate these questions as we enter into the structure of the Robbins problem.
In order to understand the Robbins problem it is neccessary to know about Boolean algebra. Boolean algebra was discovered/invented by George Boole [B] as an algebra for logic. Boole had the happy idea that one could use the notation of ordinary algebra, but re-interpret it to express the meanings of symbolic logic while retaining the calculating power of the algebra. I will describe this idea of Boole in modern notation.
Boolean algebra is the algebra that describes the simple properties of a single distinction. This represents the simplicity of on/off, outside/inside, true/false, present/absent. In the case of true and false, Boolean logic assumes a simplicity that idealizes our experience. I shall recall Boolean algebra by first recalling its interpretation for the logic of true and false.
In Boolean algebra
~A means "not A" while
A+B denotes "A or B" and
A*B denotes "A and B".
With this interpretation in mind, many rules of logic become identities in the algebra. For example,
~~A = A
means "Not not A is equivalent to A".
~(~A*~B) = A+B
means that the statements "It is not the case that neither A nor B" and "Either A or B" are logically equivalent.
Once one has a few identities of this sort, it is possible by algebraic substitution and rearrangement to obtain many other identities. For example, from
~(~A*~B) = A+B
we deduce that
~~(~A*~B) = ~(A+B)
by applying negation to both sides of the equation. Then, using the general rule that ~~X = X for any X, we get that
~A*~B = ~(A+B).
Then we substitute ~A for A and ~B for B, obtaining
~~A*~~B = ~(~A+~B).
Finally, we use ~~X=X again, and get
A * B = ~(~A+~B).
This reads out as: The statements "A and B" and "It is not the case that not A or not B" are logically equivalent.
The last rule is called "DeMorgan’s Law" (after the logician Augustus DeMorgan 1806-1871). It makes explicit the fact that we can express "and" in terms of the operations "not" and "or". Incidentally, we use here the inclusive or that means "A or B but not both". Exclusive or can make some claims for being the most fundamental logical operation, and we shall return to it in due time (and later columns).
There are many rules in Boolean algebra. One wants an axiom system of small size from which all the true equations can be deduced. There are many such systems of axioms. Here is a standard example:
Standard Axioms for a Boolean Algebra
0. The Boolean algebra B is a set that is endowed with a binary operation denoted "+" and a unary operation denoted "~". The set is closed under these operations. That is, given a and b in B, then a+b is in B and ã is in B.
1. The operation + is commutative and associative. That is a+b = b+a for all a and b in B, and (a+b)+c = a + (b+c) for all a, b, c in B.
2. There is a special element called "zero" and denoted by the symbol "0" such that 0+a = a for all a in B. ~0 is denoted by the symbol "1".
3. ~~a = a for all a in B.
4. ~(a + ~a) = 0 for all a in B.
5. a + ~(~b + ~c) = ~(~(a+b) + ~(a+c)) for all a, b, c in B.
From these axioms one can deduce all the other facts that are true in Boolean algrebra.
Commutativity and associativity are part of the simplification of ordinary language to the mathematics of this model. We say "scotch and sode" and we do not say "soda and scotch". In this sense ordinary language is not commutative. But in the ideal of pure logic, we imagine that it is possible to just list a set of independent propositions and to disregard their order. In this sense, the axioms of commutativity and associativity are like the assumptions of frictionless surfaces and ideal gases in physics.
For the purposes of logic, 0 means "false" and 1 means true. Axiom 3 says the familiar law of double negation: "Not not a is equivalent to a". Axiom 4 says ~(~a+a)=0. Thus Axiom 4 says that "It is false that it is not the case that either not a or a". In English this translates to the algevraic equivalent ~a + a =1: "It is thie case that either a or not a". Thus Axiom 4 is a statement that says that for every element in the Boolean algebra, either a is true or ~a is true. Again, we are in the idealization that assumes that there is no ambiguity, no statements beyond true and false in the system B.
Finally, Axiom 5 is better understood if we use the definition of "and" (as described above): a*b = ~(~a + ~b). Then Axiom 5 reads
a + (b*c) = (a*b) + (a*c):
The statement "a and either b or c" is equivalent to the statement "either it is the case that a and b or it is the case that a and c".
We tend to understand these statements of logic, once they are stated in English, by comparing them with images of familiar situations. The algebra, however, knows nothing but the rules that have been given to it. In this way the algebra acquires a life of its own. For example, it is possible to prove Axiom 3 by using the other axioms. In order to do this you must take a very formal attitude. The well-known interpretations of the algebra must not be used. The only rules that one can rely upon are the axioms themselves and the "usual" rules for substitution and replacement that apply in all algebraic situations.
The author would like to tell you, dear reader, how to derive Axiom 3 from the other axioms, but this requires careful guidance in the art of algebraic proof. We must postpone our introduction to that black art.
In making a proof we may believe that we have shown all the steps and all the reasons. There is still work for the reader. He or she has to be able to see the reason for taking a given step! In this sense every proof, as a text, is full of holes. The holes are filled in by the person who reads and comprehends the text.
How far can you simplify the axioms for a Boolean algebra? Huntington made a terrific discovery in 1933 an axiom system for Boolean algebra that uses only one axiom beyond commutativity and associativity.
Huntington’s Axioms for Boolean Algebra
0. The Boolean algebra B is a set that is endowed with a binary operation denoted "+" and a unary operation denoted "~". The set is closed under these operations. That is, given a and b in B, then a+b is in B and ~a is in B.
1. The operation + is commutative and associative. That is a+b = b+a for all a and b in B, and (a+b)+c = a+(b+c) for all a, b, c in B.
2. For all a and b in the set B, a = ~(a+b)+ ~(~a+~b).
This discovery of Huntington means that it is possible to get the whole structure of Boolean algebra from just one special axiom (plus commutativity, associativity and the conventions of one binary and one unary operation). Now things are beginning to get interesting. It is quite a puzzele to derive everything from Huntington’s special axioms. For example, the first thing that Huntington proves is that ~(a+~a) = ~(b+~b) for any a and b in B. After he shows this, he can define 0 by the equation 0=~(a+~a). He then has to work quite hard to show that 0 behaves like zero!
In the 1930’s Herbert Robbins, a Professor of Mathematics at Rutgers University in New Brunswick, New Jersey, asked the seemingly innocent question: What if we replace Huntington’s Axiom 2. by the following
Robbins Axiom 2. For all a and b in the set B, a = ~(~(a+b) + ~(a+~b)).
Does this again yield precisely Boolean algebra?! That question is the Robbins Problem.
It may seem an easy matter to decide this problem. If you think that this is so, please give it a try. Everyone who has made the attempt so far has found great difficulty. The difficulty appears at first to be notational. The big parenthesis surrounding the whole expression ~(~(a+b) + ~(a+~b)) makes it difficult to work with. Then difficulty becomes frustration and frustration despair as the problem recedes from view and the mathematician drowns in a sea of unruly paper. On top of this, the rewards seem very slim. Boolean algebra is well understood. Why should we worry about a puzzle like this?
Mathematics throws strange and magic puzzles up to its practioners. These puzzles sometimes become whole fields of study. It is hard to predict. It is rare to find a challenge that engages the mind just so. Eventually such puzzles acquire enough associations so that one can explain why they are important or interesting.
We have come to the end of this column. In the next installment we shall consider both the structure and the significance of this puzzle of Herbert Robbins.
References
[M] <http:www.mcs.anl.gov/home/mccune/ar/robbins>.
[K] L.H. Kauffman. Robbins Algebra. Proceedings of the Twentieth International Symposium on Multiple Valued Logic. 54-60, (1990), IEE Computer Society Press.
[KW] <http://zariski.math.uic.edu:80/~kauffman/>
[B] George Boole, "The Mathematical Analysis of Logic", Cambridge, 1847.
[H] E. V. Huntington, Boolean Algebra. A Correction. Trans. Amer. Math. Soc. 35 (1933), pp. 557-558.
Return to the content of this issue
Return to the Cybernetics and Human Knowing Homepage