“And you, Sarah. How are you enjoying my labyrinth?” “It’s a piece of cake!”

First, thanks to the readers who have commented on my first post or let me know on Twitter or via e-mail that they’re following this series. That’s enormously gratifying, and makes the writing and the research that goes into it a lot more fun.

One thing I’ve been reminded of in receiving this feedback is that relatively few people have had any exposure to formal logic, so blithely diving right into ε-δ proofs from an analysis text is going to leave an awful lot of people behind. So I have to back up and talk a little bit about logic. For most purposes, I expect to draw from Logical Labyrinths (hence the section title) and Logic and Structure, but might occasionally touch on material from other sources that I’ll call out as necessary.

What is Logic?

To answer that question, I’ll turn to van Dalen:

Traditionally, logic is said to be the art (or study) of reasoning; so in order to describe logic in this tradition, we have to know what “reasoning” is. According to some traditional views reasoning consists of the building of chains of linguistic entities by means of a certain relation “… follows from …”, a view which is good enough for our present purpose. The linguistic entities occurring in this kind of reasoning are taken to be sentences, i.e. entities that express a complete thought, or state of affairs.

These sentences are generally called “propositions.” The defining characteristic of propositions is that they are, at least in principle, either true or false. You might not know whether any given proposition is true or false—if you did, you wouldn’t need either deduction or induction to deal with it—but a truth value can be ascribed to it. To borrow examples from my previous post, “Christopher Columbus discovered America in 1492” is a proposition, as is “It will rain today.” Each can be ascribed a truth value, true or false. How to ascribe truth values to each of them might be rather mysterious in practice. By “discovered,” do we mean “was the first human being to sight or set foot on” or do we only mean “was unaware of the existence of prior to arriving?” By the former definition, it seems a reasonable person would ascribe the truth value “false” to “Christopher Columbus discovered America in 1492” (millenia after the Native Americans did!) whereas by the latter definition the same reasonable person would likely ascribe the truth value “true” to the proposition.

The “It will rain today” case is even trickier. So much so that I won’t talk further about its truth value, but I will talk, as is usual for weather, about its probability in a future post.

So what are the rules that allow us to infer that “… follows from …?” In a stroke of originality, they’re called “inference rules.” They have traditional names, such as the one I mentioned in my first post of the series, modus ponens: $$(P \Rightarrow Q) \land P \Rightarrow Q$$ Here, the uppercase variables refer to propositions, the funny tent reads as “and,” and the double-shafted right arrow reads as “implies.” So this rule literally says “If you know both that P implies Q and also P, then you can infer Q.” It might seem a little silly to spell this out in such detail, and in some ways it is—Lewis Carroll famously poked fun at this spelling-out in What the Tortoise Said to Achilles—but remember, the point is to be very sure of the soundness of our reasoning. We generally have to start with some information that is sufficiently simple and clear to be accepted as true without proof, called “axioms,” as I also referred to in my first post in this series. A statement we wish to prove is called a “theorem,” and in the process of proving it we may also prove some subsidiary results that can be used in the larger proof, called “lemmas.”

But all this terminology can make logic sound atomistic, dry, and boring, to which Logical Labyrinths is a nice antidote. It begins as a puzzle book, but eventually covers propositional and predicate logic, infinity, etc. formally, so it’s an appealing source for my work here. Let’s begin at the beginning. Smullyan’s protagonist, Abercrombie, is visiting the Island of Knights and Knaves, where knights always tell the truth and knaves always lie:

PROBLEM 1.1 (A CLASSIC CASE). On the day of his arrival, Abercrombie came across three inhabitants, whom we will call A, B, and C. He asked A: “Are you a knight or a knave?” A answered, but so indistinctly that Abercrombie could not understand what he said. He then asked B: “What did he say?” B replied: “He said that he is a knave.” At this point, C piped up and said: “Don’t believe that; it is a lie!”
Was C a knight or a knave?

The first challenge might be believing it’s possible to answer the question! But let me assure you it is. I’m not going to just give the answer, at least not yet. Think about it, discuss it in the comments, buy the book, etc. Eventually I’ll probably work through it. The point I want to make right now is just that it’s a logic puzzle and fun to reason through. But while it’s true that logic is fun, it’s also true that it’s serious business, with some proofs of important theorems coming centuries after the question was first posed, and with proof automation playing a crucial role.

Which brings us to Coq.

I Promise Coq Isn’t Foul

Coq is a “proof assistant,” or “interactive theorem prover.” The problem with automating logic, essentially, is: you can’t, at least not for any interesting logic, at least not completely. What you can do is help the human logician construct a proof of a theorem, provide partial automation support where possible, and—here’s the kicker—check the proof when it’s done. Finding the proof may be undecidable or at least take a long time. Checking it is cheap and relatively fast. Coq is a formidable tool, having been used to construct the proofs of the four-color map theorem and Fermat’s last theorem, but I’m going to try to keep its use simple in this series, striking a balance between spelling proofs out to help build intuition and taking advantage of automation when the details are just too much. Being an old EMACS user, I’ll also use Proof General, an EMACS-based UI, for interacting with Coq.

First, lets’s show off how easy Coq can be.

As soon as I type the carriage return after the period (the way I have Proof General configured), I get another window in EMACS that says:

1 subgoal
  
  ============================
   1 + 1 = 2

I’ve told Coq I want to prove that 1 + 1 = 2. Don’t laugh; it took Russell and Whitehead over 400 pages across two volumes to do so. When you tell Coq you want to prove something, it helpfully tells you what your current subgoal is and lets you tell it what to do in order to prove it. The space above the double line is the “context,” and can have facts, hypothesis, etc. relevant to the current goal. For this problem, we don’t have any, just the goal.

Thankfully, for Coq, this problem is

In the other window, Coq happily tells me:

Proof completed.

And now I can join professors the world over and say

Coq’s reaction to that is:

one_and_one_is_two is defined

This means I could use this important theorem in constructing other proofs, if I so desired.

But what happened? What did it mean when I typed “trivial.”? How did Coq just decide that proves 1 + 1 = 2 when it took Russell and Whitehead those 400+ pages to do the same thing?

“trivial” is called a “tactic,” and Coq belongs to the family of tactics-based proof assistants. The combination of context and subgoal I described is called a “proof state.” Tactics try to simplify a proof state, with the simplest possible proof state, of course, being one with no subgoal. You can think of a tactic as being a little program that tries to change the proof state to be “closer” the goal, and in fact that’s exactly what they are. You can even write your own in Coq’s Ltac tactic language or in OCaml, the language Coq is written in.

Coq has a rather sophisticated notion of computation built into it, which I won’t go into any detail on here. Suffice it to say that Coq interprets “1” and “2” as natural numbers by default and can do computation with them in a way that it knows to be logically sound. When I said “trivial,” one of the things Coq did was to actually add 1 + 1 soundly according to the Peano axioms for the natural numbers. Then it noticed that I had essentially asked for a proof that 2 = 2, which it was able to discharge based on the reflexivity of equality. This ability of Coq’s to blend computational operations and logical ones will come in quite handy later on.

But I’m getting ahead of myself again. Back to the basics! Propositions! I propose to continue discussing propositional logic in Coq in my next post.