The Limit of Logic and The Rise of The Computer

Why hasn’t intuition received as much attention as logic for the twenty five centuries since Aristotle? Intuition is elusive, hard to define and quantify, and sometimes deceiving. As a matter of fact, there are even different kinds of intuition. Intuition is the beacon shining over the darkness according to Aristotle; however, it also appears like a searchlight pointing at the wrong spots in darkness most of the time. On the other hand, logic, with which mathematics can be demonstrated rigorously, is precise and certain until you get back down to the first principles.

Poincaré: Using Logic to Demonstrate and Intuition to Invent

Henri Poincaré (1854–1921), a French mathematician and physicist, recognized that our intuition could be misleading, yet primarily responsible for mathematical development. Logical reasoning, according to Poincaré, is for the final demonstration of the result from the intuitive exploration. He classified great mathematicians into two categories, analysts who follow logic and are incapable of “seeing in space” and geometers who follow intuition and are “quickly tired of long calculation and become perplexed”. According to Poincaré,

Logic, which alone can give certainty, is the instrument of demonstration; intuition is the instrument of invention” (Poincare, 1969).

Imagine in an elementary geometry class, there is a student, Amy, who uses both intuition and logic to learn geometry. Intuition is used to inspect diagrams and search for proof strategies. Logic is then used to lay down a proof step by step. Amy is given the following problem:

Amy immediately recalled that 180 degrees has a nickname, the flat angle. So, she thinks: The problem must have something to do with a straight line. Since there is none, I’ll just draw a straight line somewhere. I was taught to draw an auxiliary line when necessary. There is no other choice but to draw one touching one of the vertices. So I’ll arbitrarily pick C. How should the line be oriented? One obvious choice is to make it parallel to the line AB. I look at the diagram with the auxiliary line and find that angles a and d, as well as e and b look equal, but of course I’m not supposed to count on the diagram or my drawing’s accuracy. However, I do remember that something from the parallel postulate that they are indeed equal! Voila! a+b+c=e+d+c=180.

At this point, all her ideas for solving this problem come from guesses and spontaneous judgment from what she has been taught in the class. She is more an intuitive guesser than a logical reasoner. Next, she will switch to her logical reasoning skills to connect the dots and demonstrate a proof to her geometry teacher. Even with this trivial example, Amy epitomizes how a typical mathematician uses intuition to invent and logic to demonstrate.

Russell: Games that Don’t Need Meanings

Rather than abandoning Frege’s work and changing direction, Russell and his colleagues continued Frege’s unfinished work. However, the harder mathematicians tried to avoid the kinds of paradoxes that Frege contronted, the more subtle and profound were those that emerged.

Russell gave an illustrative version of his paradox called the barber paradox:

A barber shaves all those and only those who do not shave themselves. Does the barber shave himself?

If the barber shaves himself, he, the barber, does not shave him. A contradiction. On the other hand, if the barber does not shave himself, he would be shaved by the barber. Also a contradiction.

Unlike Frege, Russell gave up the idea that axioms need to be self-evident, as long as they could be shown to develop mathematical knowledge without contradictions. He was quoted, “Mathematics may be defined as the subject in which we never know what we are talking about, nor whether what we are saying is true”. Any prior knowledge, no matter how self-evident it feels, is forbidden, and there should be no place for human intuition in mathematical development. It should not be surprising that it took 362 pages to derive1+1=2 in Russell’s Principia Mathematica.

Hilbert: Games that Don’t Need Players

David Hilbert (1862–1943), a German mathematician, extended Frege and Russell’s work, and proposed the famous Hilbert’s program, that any branch of mathematics could be reformulated as a formal theory, and he asked if there were positive answers to the following 3 questions:

1. Can the consistency of a formal theory, in which no contradiction can be derived from the axioms, be proved within the theory itself?
2. Can a formal theory prove to be complete, in that it includes any true mathematical statement in the specific branch that it is intended to embody?
3. Is there a purely mechanical procedure, which I refer to as a universal proof mechanism, that determines if any given mathematical statement is true or false. This question was referred to as the decision problem, or Entscheidungsproblem, in German.

Hilbert expected the answers to all his questions to be positive, which would have totally eliminated the necessity of intuition, and made mathematics intuition-free. Implied in his optimism for formal theories was his positivism, the belief that all mathematical problems could be solved. His famous saying “Wir müssen wissen, wir werden wissen” (We must know, we will know) was inscribed on his tomb in Gottingen, Germany. Hilbert and his colleagues were referred to as the “formalists”.

Hilbert believed that by starting with a set of consistent axioms, a formal theory could be complete, self-checkable, and self-discoverable. Since a formal theory was not meant to be appreciated or interpreted by humans, but consumed by machines, it is referred to as a formal “system”. Referring to such a system as “formal” implied that previous treatments of the same subject were “informal”, which reflected their use of intuition. Regarding his formal theory of Euclidean geometry, Hilbert once remarked that instead of points, lines and planes, one might just as well talk of tables, chairs and beer mugs.

While Russell considered mathematics to be symbolic games with no meaning, Hilbert wanted the games to play by themselves. If Hilbert’s grand vision had been right, a formal system would have summed up the past and sealed the future of mathematics. Ironically, Hibert might have been misguided by his intuition in this regard.

Gödel: The Return of Mathematicians

Kurt Gödel (1906–1978), an Austrian-American logician, was a champion in Hilbert’s program before he brought it down. He made Hilbert’s program look promising by proving in his completeness theorem that the symbolic rules of first-order logic cover all valid logical inferences. However, Gödel’s incompleteness theorems would devastate the program. He found that with a numbering scheme later named after him, he could represent the mathematical statements making up a formal system of numbers as numbers themselves. This way, a formal system of numbers, which was supposed to prove facts about numbers, could prove facts about itself. Under Gödel’s numbering, a formal system of numbers becomes self-referential as demonstrated below:

Furthermore, the theory also includes the statements about whether the theory itself is provable. With this insight, Gödel ingeniously constructed a modified version of the liar’s paradox as shown below:

This sentence is called Gödel’s sentence. If it is true, then it is not provable in the theory, according to what it says. If it is false, then what it says must be false, which means it is provable in the theory, and therefore it must be true. So, we have a true mathematical statement that can be neither proved nor disproved in the theory. A formal system for a mathematical theory, even as elementary as number theory , is only an approximation.

Turing: The Rise of Programmers

What is computable?

Even if we settle for an incomplete formal system, does a universal proof mechanism exist to solve the decision problem? Before diving deeper into the question, we need to answer what exactly a “purely mechanical procedure” is. Alan Turing (1912–1954), an English mathematician, defined a mathematical model of a “purely mechanical procedure”, inspired by a patient and rule-following human computer (usually a woman) doing her job using pencil and paper. A machine defined in the model scans a hypothetical tape divided into squares. Following a table of rules and its own internal state, it next writes a symbol on the square, and then either stays put, or moves one square to the right or left. This machine model was later referred to as the Turing machine, which he used to make mathematical arguments, instead of making a real computer. It is generally believed that everything in the universe is computable if and only if it can be reduced to a Turing machine. This is referred to as the Church-Turing Hypothesis. The table of rules mentioned above is now referred to as a “computer program”.

The Halting Problem

With the Turing machine defined, Turing proceeded to prove the nonexistence of Hilbert’s universal proof mechanism. Inspired by Gödel’s numbering scheme, Turing encoded machines as numbers so that machines could be studied as numbers, which could be taken as inputs to other machines. Now Turing could ask the halting problem: was there a machine, called the halting oracle, that could decide if any machine halted on a given input or loop forever. Turing ingeniously avoided the necessity of explaining the details of such an absurdly powerful machine by showing that its mere existence would lead to a contradiction.

Turing assumed there was a special machine M that does exactly the opposite of what the halting oracle does. If the halting oracle decides a machine halts when taking itself as the input, M will loop forever. On the other hand, if the halting oracle decides a machine loops forever, M will halt in this case. This way, you can say M is designed to purposely sabotage the halting oracle. Now the question is: does the special machine M halt when it takes itself as input?

1. If M halts on M, M will loop forever by the definition of M: A contradiction
2. If M loops forever on M, M will halt. Another contradiction

This self-referential paradox is illustrated below:

Therefore, the halting oracle cannot exist. The halting problem cannot be solved, or technically speaking, it is undecidable.

Now we can go back to Hilbert’s decision problem. If the universal proof mechanism existed, we could make it the halting oracle by formulating any query for the halting oracle as a mathematical statement. However, the halting oracle does not exist, neither does the universal proof mechanism. On the other hand, if the halting oracle did indeed exist, we could implement the universal proof mechanism in the following straightforward way: first, write a program to search infinitely for all possible proofs for a mathematical statement, and halt when it finds one; next, we ask the halting oracle if such a searching program halts. Hence, the unsolvability of the halting problem implies that of the decision problem, and vice versa.

Imagining the halting oracle existed, we would easily solve many difficult or open number-theoretic problems. For example, we could prove Goldbach’s conjecture, which states that every even number greater than 2 is a sum of two prime numbers. We could simply write a program to loop over all even numbers starting from 4 and check if each is indeed a sum of two prime numbers. Then we would prove the conjecture by feeding the program to the halting oracle and asking if it halts. In reality, this problem remains unsolved.

Another way to describe the non-existing halting oracle and universal proof mechanism is to say that they are not “computable,” according to the Church-Turing Hypothesis. In Gödel’s own words, his results

Do not establish any bounds for the powers of human reason, but rather for the potentialities of pure formalism in mathematics.

In other words, what Gödel and Turing have shown was a limitation of logical reasoning without using intuition. They actually substantiated Poincaré’s point that in spite of its rigor and certainty, logic is only a demonstration tool, and needs to be complemented by intuition.

In the absence of a “meta-mathematical” solution to prove “all” mathematical problems, the area of “automatic theorem proving,” with less ambitious, yet more pragmatic scope than Hilbert’s program, has been active and thriving. Hilbert’s formal theories turned out to be approximations to mathematical knowledge. Just as the physical reality of the universe is still a mystery calling physicists to solve it, the frontier of mathematical knowledge remains elusive to mathematicians. Now, mathematicians and their intuition were back in the games.

The Birth of the Computer and The Rise of Programmers

In the proof for the halting problem, there must be a way for M, the hypothetical machine, to run the halting oracle itself in order to sabotage it. To achieve this, Turing created the universal machine that can read the encoding of any Turing machine, and act on behalf of it. From outside, you would not be able to tell whether it is the universal machine or the specific machine that does the work. Modern computers are based on the universal machine, which is often described as “powerful” enough to be able do everything imaginable. But, where does its power come from? It is really an empty shell designed to run other Turing machines, which must have been written by someone, not through logical reasoning but with creativity, insights, judgments and many other aspects of our mental efforts, which can be collectively referred to as intuition . From this perspective, Turing not only invented the computer, but also created the role of programmers, who are responsible for harnessing the “expressive power” of the universal machine to program it. Instead of an all-powerful logic machine that locks itself in an ivory tower, we have the all-purpose computer that touches almost every aspect of our daily lives!

Bibliography

• Aaronson, S. (2016). P=?NP. In Open Problems in Mathematics. Springer.
• Aristotle ‘On Rhetoric’: A Theory of Civic Discourse (G. A. Kenndy, Trans.). (1991). Oxford University Press.
• Bansal, K., Loos, S., Rabe, M., Szegedy, C., & Wilcox, S. (2019).HOList: An Environment for Machine Learning of Higher-Order Theorem Proving. Proceedings of the 36th Conference on Machine Learning.
• Bansal, K., Szegedy, C., Rabe, M. N., Loos, S. M., & Toman, V. (2020). Learning to Reason in Large Theories without Imitation. https://arxiv.org/pdf/1905.10501.pdf
• Borel, E. (1962). Probabilities and Life. Dover Publications, Inc.
• Copland, J. B., Posy, C. J., & Shagrir, O. (2013). Computability: Turing, Gödel, Church, and Beyond (Kindle ed.). The MIT Press.
• Heule, M. J. H., Kullmann, O., & Marek, V. W. (2016). Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. In Lecture Notes in Computer Science (pp. 228–245). Springer International Publishing. 10.1007/978–3–319–40970–2_15
• Poincare, H. (1969). INTUITION and LOGIC in Mathematics. The Mathematics Teacher, 62(3), 205–212.
• Polu, S., & Sutskever, I. (2020). Generative Language Modeling for Automated THeorem Proving. arxiv.org. https://arxiv.org/abs/2009.03393
• Polya, G. (1954). Induction and Analogy in Mathematics.
• Polya, G. (1954). Mathematics and Plausible Reasoning. Martino Publishing.
• Polya, G. (1973). How to Solve It (Second ed.). Princeton University Press.
• Selsam, D., Lamm, M., Bunz, B., Liang, P., Dill, D. L., & de Moura, L. (2019). Learning a SAT Solver from Single-Bit Supervision. https://arxiv.org/abs/1802.03685