Gödel's Lost Letter and P=NP

Peter Andrews is a Professor of Mathematics, Emeritus at Carnegie Mellon University (CMU) in Pittsburgh, Pennsylvania. He has studied logic his whole life—he is a logician.

I always loved formal logic, but was never an expert on why study logic? I did take his logic class when I was a graduate student at CMU. I enjoyed it very much.

Peter was, as we just mentioned, a student of Alonzo Church. His thesis appeared in book form, A Transfinite Type Theory with Type Variables.

Saying “transfinite” sounds rarefied. However, transfinite systems still keep one finite foot on the ground, in that all descending chains are finite. Peter extended his and other work with Church to develop systems including that can be expressly programmed. became a backbone of the Theorem Proving System (TPS) designed by Andrews and colleagues.

From Peter the Author

Peter wrote a textbook in 2002 that makes these advanced logic systems accessible to students. It is titled An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Never mind that Kurt Gödel showed respects in which proof must fall short of truth—proof remains our most reliable guide to truth. The essence of the book and the educational wing ETPS of TPS is to use proof for learning and discovery.

Here is what the textbook’s description says about the application of type theory:

The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem’s Paradox about countable models of set theory.

Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.

Peter expressed a motivation for learning and employing powerful logic implementations in his 2003 Herbrand Award acceptance speech.

We need very sophisticated methods of thinking about complex problems. Our technology and scientific knowledge progress steadily, but are we any better at thinking than Socrates or Pythagoras?

He continued into how one needs to base work in a system that is built around a simple core:

Church’s type theory is much simpler, and is at the same time a richer, more expressive language [than Principia Mathematica], since it recognizes functions as first-class objects which do not have to be regarded as sets of ordered -tuples. … A simple introduction to type theory can be found in the last three chapters of my book.

His speech finished by observing how “serious efforts to mechanize logic” have made progress unmatched in the 2,500+ year study of logic.

From Logic Puzzles to Reasoning About Knowledge

Another student of Church was Raymond Smullyan, and his work enters Andrews’s story as well. We featured him before and after our memorial on his passing at age 98. He was best known popularly for numerous books on logic puzzles.

Among the most difficult logic puzzles are those that concern logical inference about others’ state of knowledge. One such puzzle is called “The King’s Advisor.” Here is a statement (edited by us):

A king wants an advisor and comes to ask the 3 wisest sages. He blindfolds them and put hats on their heads. Afterwards, the king takes off their blindfolds. He tells them that their hat is either blue or white. He tells them that whoever can deduce the color of their hat will be his next advisor. Also he tells them that at least one of the sages will be wearing a blue hat.

The sages can all see each other’s hats except of course, their own. Sage A sees that the other 2 are wearing blue hats. For hours no one speaks, then Sage A stands up and tells the king the color of his hat. What color is it and how does he know?

Wikipedia illustrates its page on common-knowledge logic puzzles with what many consider the hardest of this kind, the “blue-eyed islander” puzzle. It has an xkcd page. I (Ken filling in material here) thought we had written about this puzzle on this blog, but it turns out to be a memory from Terry Tao’s blog.

Quantifying the possible gain of knowledge is integral to the analysis of many modern cryptographic protocols. Four logician friends of ours stepped in with an even broader approach.

Here is what Ronald Fagin, Joseph Halpern, Yoram Moses, and Moshe Vardi say about their book, Reasoning About Knowledge.

Reasoning about knowledge—particularly the knowledge of agents who reason about the world and each other’s knowledge—was once the exclusive province of philosophers and puzzle solvers.

More recently, this type of reasoning has been shown to play a key role in a surprising number of contexts, from understanding conversations to the analysis of distributed computer algorithms. [Our book] brings eight years of work by the authors into a cohesive framework for understanding and analyzing reasoning about knowledge that is intuitive, mathematically well founded, useful in practice, and widely applicable.

A crisp way to boil down their advice on “why study logic?”—and logic about others’ logic in particular—is that more walks of life are “going meta” in the near future—in ways that existing protocols have also started to mechanize.

Logic Has A World Day

Here is another indicator on why logic is important: It has an official world day. A nice article in the Guardian a year ago explained why the date 14 January was chosen:

The date was chosen since it is both the day Gödel died, in 1978, and the day the logician Alfred Tarski was born, in 1901.

The article gives a wonderful puzzle by Smullyan that illustrates Gödel’s first incompleteness theorem.

The world day was proclaimed by UNESCO in November 2019. The Director-General of UNESCO since 2017 is Audrey Azoulay.

A reason why she is a perfect spokesperson for logic emerges on her Wikipedia page:

Her father, André Azoulay, is the current advisor to King Mohammed VI of Morocco, having previously been the advisor to his predecessor Hassan II from 1991 to 1999.

It is clear that her father wears several hats. Whether she had to deal with knights who tell the truth and knaves who lie in the royal palaces of her childhood is immaterial, as she doubtless encountered plenty of both in her prior career in politics. She gave further remarks at the first observance, in January 2020:

“In the twenty-first century—indeed, now more than ever—the discipline of logic is a particularly timely one, utterly vital to our societies and economies. Computer science and information and communications technology, for example, are rooted in logical and algorithmic reasoning.”

The 2020 World Logic Day really was marked by events around the world. Here is a rundown on what happened earlier this month, in 2023.

Open Problems

So why is logic important? What do you say?

The article linked under “why study logic?” in our intro illustrates its 5 reasons with some weirdly-chosen photographs. One with a woman under her car hood while her toddler son watches has more going on—with matching colors and all—than the paragraph relates. Two other photos are of a scarecrow and Spock wielding a giant Vulcan shovel. Our “meta” logic puzzle is, what was the author thinking?