One of the best known hard problems in computer science is the halting problem. In fact, it's widely thought^[1] that you cannot write a program that will, for any arbitrary program as input, tell you correctly whether or not it will terminate. This is written from the framing of computers, though: can we do better with a human in the loop?

It turns out, we can. And we can use a method that's generalizable, which many people can follow for many problems. Not everyone can use the method, which you'll see why in a bit. But lots of people can apply this proof technique. Let's get started.

We'll start by formalizing what we're talking about, just a little bit. I'm not going to give the full formal proof—that will be reserved for when this is submitted to a prestigious conference next year.

We will call the set of all programs P. We want to answer, for any p in P, whether or not p will eventually halt. We will call this h(p) and h(p) = true if p eventually finished and false otherwise.

Actually, scratch that. Let's simplify it and just say that yes, every program does halt eventually, so h(p) = true for all p. That makes our lives easier.

Now we need to get from our starting assumptions, the world of logic we live in, to the truth of our statement. We'll call our goal, that h(p) = true for all p, the statement H. Now let's start with some facts.

Fact one: I think it's always an appropriate time to play the saxophone. *honk*!

Fact two: My wife thinks that it's sometimes inappropriate to play the saxophone, such as when it's "time for bed" or "I was in the middle of a sentence!^[2]

We'll give the statement "It's always an appropriate time to play the saxophone" the name A. We know that I believe A is true. And my wife believes that A is false. So now we run into the snag:

Fact three: The wife is always right.

This is a truism in American culture, useful for settling debates. It's also useful here for solving major problems in computer science because, babe, we're both the wife. We're both right!

So now that we're both right, we know that A and !A are both true. And we're in luck, we can apply a whole lot of fancy classical logic here. Since A and !A we know that A is true and we also know that !A is true. From A being true, we can conclude that A or H is true. And then we can apply disjunctive syllogism^[3] which says that if A or H is true and !A is true, then H must be true. This makes sense, because if you've excluded one possibility then the other must be true. And we do have !A, so that means: H is true!

There we have it. We've proved our proposition, H, which says that for any program p, p will eventually halt. The previous logic is, mostly, sound. It uses the principle of explosion, though I prefer to call it "proof by married lesbian."

Of course, we know that this is wrong. It falls apart with our assumptions. We built the system on contradictory assumptions to begin with, and this is something we avoid in logic^[4]. If we allow contradictions, then we can prove truly anything. I could have also proved (by married lesbian) that no program will terminate.

This has been a silly traipse through logic. If you want a good journey through logic, I'd recommend Hillel Wayne's Logic for Programmers. I'm sure that, after reading it, you'll find absolutely no flaws in my logic here.

After all, I'm the wife, so I'm always right.

1. It's widely thought because it's true, but we don't have to let that keep us from a good time. ↩

2. I fact checked this with her, and she does indeed hold this belief. ↩

3. I had to look this up, my uni logic class was a long time ago. ↩

4. The real conclusion to draw is that, because of proof by contradiction, it's certainly not true that the wife is always right. Proved that one via married lesbians having arguments. Or maybe gay relationships are always magical and happy and everyone lives happily ever after, who knows. ↩