Recently I’ve been thinking a lot about a certain model of a rational agent: a proof-based agent which is triggered to act when it finds certain proofs in Peano arithmetic (PA). Back when MIRI had an agent foundations team, they found they could derive what these agents would do using provability logic, a modal logic in which the necessity box represents the provability predicate in PA. As a fun example, they ran a “modal combat” tournament in which “modal agents”, a special case of proof-based agents, faced each other in prisoner’s dilemmas. Resolving these matches becomes an exercise in modal logic.

I’ve been trying out these matches on paper, and I like the way I do modal logic better than the way the rest of you do it on LessWrong. You all do step-by-step proofs. “Natural deduction” I guess, since the formal version is called a “natural deduction system”.

I answer modal logic questions using the semantics: Kripke frames, directed graphs of possible worlds. I’ve tried to convince you that if you look at the Kripke frames in “modal combat”, they make sense and provide insight. One possible world looks like the real world, another looks like my simulation of my opponent, and another looks like my simulated opponent simulating me. They’re like thought-bubble worlds.

But the way I come up with these semantic arguments is actually with a formal system: the tableau method, which is a kind of tree-structured formal proof. To think through modal combat matchups I was writing out tableaus tableaux on paper. Then, I read those as arguments about Kripke frames, and wrote those arguments in English for my post.

In the future I would sometimes like to just post the tableau, so I’m going to try to teach you how to read them. I’m not going to teach you how to write them, which I learned from Graham Priest’s Introduction to Non-Classical Logic. But just to read a tableau as an argument that uses the semantics of the logic—maybe we can get that far in a blog post.

Example 1: propositional logic

Truth table

If you don’t know what I mean by semantics, let’s consider an example I hope you’re already familiar with: truth tables.

Suppose I want to prove the disjunctive syllogism is valid in propositional logic. That’s an argument where the premises are and , and the conclusion is .

Let’s negate the conclusion and do a kind of proof by contradiction. With a truth table, we can show that it is impossible to simultaneously satisfy , , and :

No row with all ’s for these three sentences.

In propositional logic, a model is a row in the truth table. By a model, I mean, the kind of thing that a sentence can be true or false of. A model, a row in the truth table, is a valuation of all the sentences of propositional logic, constrained by consistency rules (“ and have the value True iff does” etc.).

We showed there can’t be a model satisfying the premises that also satisfies , thus proving that the premises entail . This was an appeal to the semantics of propositional logic.

Tableau

Now, making the same argument with a tableau. We begin by listing our premises and our negated conclusion. Then, the disjunction splits the tableau into two branches, where we separately consider the case and the case:

We write a to close a branch once we can find a contradiction by tracing upwards. If all the branches close, that means we can’t satisfy the sentences we started with.

The relationship between the tableau and the truth table might be more clear if I start the tableau with just the premises of the disjunctive syllogism:

From the open branch you can read off the model, the third row of the truth table.

By the way, the tableau stops there because there are no more rules to apply. We don’t have the “lengthening” rules you would have available in a natural deduction system. For example, we don’t have disjunction introduction (which takes you from to ). This gives tableaux a pleasing mechanical feel: you just apply whatever rules you can until you run out.

Example 2: modal logic

Tableaux get more interesting in modal logic, but as before, let’s start with the semantics. To build a model of a sentence of modal logic, we start with a Kripke frame. A Kripke frame consists of a set of possible worlds, and a relation on this set, which I’ll call the “visibility” relation, following the Arbital page. I write this relation as an arrow, which is why I said earlier that a Kripke frame is a directed graph. A Kripke model is a Kripke frame, plus, for each possible world, a valuation of all the sentences. Valuations have new consistency conditions beyond the ones from propositional logic, corresponding to the new modal operators, but I’ll explain those as they come up.

In the tableau method for modal logic, we index sentences according to what world they’re true in. A line like means is true in world . And a line like means is visible from .

Tableau and model

As an example where we can see the tableau branch, let’s consider the disjunction :

Corresponding to the two branches of the tableau, we have two Kripke models:

and are possible worlds, an arrow means visibility, and means is true in world .

Some technicalities: if we want to be sure these two models are distinct from each other, we would need to replace with . And since we haven’t fully specified the valuations at each world, these are really two classes of Kripke models.

The consistency rules for valuations make some additional sentences implicit. is true in a world iff is true in a visible world. So we could also have written:

In this case, the sentences I’ve added were also in the tableau, so I could have read them off from there. What I explicitly annotate on the model is a matter of taste. It’s like adding columns to a truth table.

Semantic argument

Anyway, I want to show you an example of an actual proof. Let’s show that our premise entails the conclusion .

First, let’s see that this conclusion is implicitly true at in both of our models. One of the consistency conditions we inherited from propositional logic means we implicitly have disjunctions at :

By our consistency condition for , the disjunction is possible at . That’s one way to make the semantic argument.

But to do a proof by contradiction, we’re going to negate the conclusion, yielding , or equivalently, . The consistency condition for is that the sentence must be true in all visible worlds. So we can’t put that at , because that would require at , contradicting both Kripke models. That’s our proof of .

Tableau proof

With a tableau proof, we can do the semantic proof by contradiction automatically. We start with our premise and negated conclusion, and end up closing both branches:

It looks big, but it’s mostly just the tableau we had before. Our negated conclusion adds a bit to each branch: an assertion of in world , leading to a contradiction.

Example 3: a branched Kripke frame

One last thing: I want to make clear to you something that I wish someone had made clear to me. Tableaux branch. Kripke frames, as directed graphs, can also branch. These are totally different.

Our tableau from the previous example branched because we split the proof into cases. Semantically, this meant we had two Kripke models, one for each case. The Kripke frames themselves were linear, with no branches.

You can get branched Kripke frames. For example, instead of considering a disjunction as before, let’s consider a conjunction: . The tableau looks like this:

Reading off a Kripke model:

See? The branched Kripke frame was represented in the tableau as the lines and . Not by a branched tableau.

Where I’m going with this

Sometimes I just want to show you a tableau without walking through all the logic.

In my previous post on modal combat, after neatly interpreting each world in the Kripke frame, I had to admit that the semantic perspective doesn’t actually work out that nicely for the original modal combat paper. That the paper’s FairBot cooperates with itself is a Henkin sentence—that is, a sentence asserting its own provability, as I explained previously. I mentioned in the post that I did prove the Henkin sentence, but the proof took me all the way down to . What I was referring to was this tableau:

Now can you see why cooperation with Payor’s lemma was a revelation to me? The Payorian FairBot has a more complicated-looking definition, but Kripke semantics reveal a simple and intuitive underlying mechanism—the opposite of what I found with the original FairBot.

I hope that if you’ve made it this far I can show you a tableau like that and it means a little something more to you than just a big messy diagram you have to scroll past to get back to reading the post. Even if my point is just “look how awful this is”.

Oh, and if you want to make your own tableau diagrams in TeX, you can see my code at the GitHub repo for this post.