Logic as Minecraft (Part 1)

Introduction

This blog post is intended to be the first in a series where I try out an alternative approach to teaching formal logic and proofs, using a crafting/resource management game as a vehicle. I will be taking liberal inspiration and examples from the wonderful Minecraft video game.

The reason I wanted to try something new is that, although I’ve always found logic fascinating, it has a reputation for being quite abstract and challenging in classroom settings.¹ I hope it’ll make learning logic not only fun and intuitive through (literal) Minecraft gameplay, but also interactive by later incorporating a live coding environment called an interactive theorem prover², which will allow us to play logic as a (surprisingly addictive) game with real-time feedback.

Hopefully, the series is accessible to those who have seen a bit of Boolean logic (like conjunction ∧ and implication →), but other than that, no background in formal logic or proof techniques is assumed.

Without further ado, let’s dive in.

Ground rules

Let’s play a game of construction, where we will be making or crafting things out of other things. It’s a game that you have probably played before, in many different contexts:

• If you like cooking or baking, you may have made a dish out of ingredients, e.g., a cake out of flour, sugar, eggs, and butter.
• If you took a chemistry class, you learned that the water molecule (H₂O) can be made out of hydrogen (H₂) and oxygen (O₂).

Keep those intuitions in mind, because they will serve you well in the game we are about to play.

Our game will be played as follows:

• There will be items which can be made, or used to make other items.
• As the game designer, I will prescribe a set of actions that combine existing items to make new items.
• At any point in time, the game is in a certain state, which consists of an inventory of items that we currently have, and a single goal item that we are trying to make.
• We win the game if we make the goal item. That is, if in the current state, the goal item is right there in our inventory!

We will visualize a game that transitions from one state to another as follows:

Here’s how to read this diagram:

1. Initially on the left, our inventory contains items A, B and D, and we are trying to make item G. We will use the horizontal line to separate the inventory from the goal.
2. We then apply the action A, B -> C, which consumes items A and B from our inventory and produces item C.
3. After this action, we are now in a new state where our inventory contains item C. Both inventory item D and goal item G remain unaffected by this action.

I haven’t told you what the items are and what actions are available to us yet. Let me introduce them now, all inspired by… Minecraft!

Let’s play Minecraft

Here are the only items in our game, for now:

• wood
• charcoal
• stick
• ore
• iron
• axe

The actions we can take are as follows:

1. burn : wood → charcoal
2. chop : wood → stick
3. smelt : ore , charcoal → iron
4. assemble : stick , iron → axe

I hope that even if you haven’t played Minecraft before, you can intuitively understand what these actions mean, based on real-world analogies:³

1. burn : You can burn a piece of wood to make charcoal.
2. chop : You can chop a piece of wood to make a stick.
3. smelt : You can smelt a piece of ore with charcoal to make iron.
4. assemble : You can assemble a stick and iron to make an axe.

To familiarize ourselves with the game, let’s play a few rounds, shall we? Say the initial state of our game is as follows:

That is, assume that we already have a piece of wood and a piece of ore in our inventory, and our goal is to make an axe, which is marked with an open goal tag since the goal item is not yet in our inventory.

Exercise: Take a pause, and think about how you would play this game. What action would you take first?

We might reason like this: “Well, we eventually need an axe, and to make an axe, the assemble action says we need a stick and iron…”

Good! Let’s pause right there and focus on the stick first. Since we have a piece of wood, we can use the chop action to make a stick. Let’s see that in action by clicking the NEXT button:

Now, let’s focus on the iron. To make iron, we need to use the smelt action, which requires ore and charcoal. We already have ore, but we don’t have charcoal yet. How can we get charcoal? Well, we can use the burn action on wood to make charcoal…

Wait, we don’t have any wood left in our inventory! We just used it to make a stick, which means we’re technically stuck, unless we started with more wood in our inventory.

Honorable cheating

As a kind game designer, I want to make our life a little easier: let’s NOT worry about how many copies of each item we have in our inventory. Instead, I will introduce a “cheat-code” action called dup , whose effect is captured by the following diagram:⁴

That is, for any item A, dup allows us to make a copy of A in our inventory.

Intuitively, what this cheat code says is that possessing one copy of an item is as good as having infinitely many copies of that item. In other words, we don’t have to worry about running out of items in our inventory, since we can always keep duplicating them.⁵

I also want to bring your attention to another interesting aspect of this action, which differs from the other four actions (burn , chop , smelt , assemble ) in an important way: the item A involved in the action is generic. That is, item A is just a placeholder for any item in our game. We can specialize dup to duplicate wood, charcoal, iron, and so on, by replacing the generic placeholder A with a specific item (as long as the thing we are duplicating is already in our inventory). Heck, the exact name of the placeholder A is not important, and we could have named it X or FireInTheHole. In contrast, the other four actions are specific to the items involved in them. For example, burn is specific to wood and charcoal, and we can’t use it to burn ore into iron.

We will follow the convention that placeholders are capital letters A, B, C, etc., while specific items are lowercase letters like wood, charcoal, stick, etc.

With our new cheat code in hand, we can now finish our previous game!

Recall that the reason we couldn’t fully make an axe before was that we needed two pieces of wood (one for the stick, and one for the charcoal to help smelt iron), but we started with only one. Let’s just use dup on wood, after which we play the game as before:

In the last state, the goal item axe is in our inventory, so we have successfully completed the game. Nice.

Alternative thinking

You may have noticed that how the game state evolves in the above diagram runs counter to the way we initially reasoned about the game (and arguably the more “natural” way of thinking). Previously, our reasoning started with the eventual goal item axe, and we worked backwards to figure out what we needed to make it (namely, a stick and iron); then we recursively broke down those “sub-goals” to figure out further items we need.

But when we actually played the game by drawing the state transition diagram, we started with the items in our inventory in the initial state (namely, wood and ore) and reasoned forward to figure out what we could make with them, eventually leading us to the goal item axe.

Forward reasoning means that we always focus on what’s above the line—items we already have. When reasoning forward, we always have the risk of making something that we don’t need eventually, or spending a resource that we should have saved for something else, meaning we always have to cross our fingers and pray that we’re indeed making progress.

Instead, can we shift our focus onto what’s below the line—our ultimate goal—and progressively decompose it into smaller sub-goals that are hopefully easier to tackle? This way, we know that every step we take is a step that we must take towards our ultimate goal, and we won’t waste any resources on things that don’t help us get there.

This is indeed possible. Backward reasoning is a very effective strategy that complements forward reasoning. In backward reasoning, we always focus on the goal item and ask ourselves: “What do we need to achieve this goal?” Then we recursively break down the sub-goals until we reach items that are already in our inventory.

Let’s instead apply backward reasoning to play the same game. The initial state of the game is the same as before. This time, we simply ignore the inventory part, instead focusing on the goal item axe. We ask ourselves: “What do we need to make an axe?” The answer is given by the assemble action: we need a stick and iron, which means we can decompose our goal into two sub-goals: 1) make a stick and 2) make an iron. Let’s write that down:

Observe that, using backward reasoning, the diagram is no longer a linear sequence. The initial state is “forked” into two independent branches, one for each sub-goal. We will tackle each sub-goal separately, which may further fork into more sub-goals, and so on. Our diagram will eventually grow into a tree, whose root, the initial state, is on the left and the tree grows towards the right. (Note that we also switch the direction of the arrow to indicate that we are applying the assemble action right-to-left.)

Look closely at what happened to the inventory when we forked. Rather than dividing wood and ore between the two branches, we handed both items to both branches. In other words, each branch inherits the same inventory as the state it came from. At first glance, this should look like daylight robbery. We started with one wood and one ore, and now, apparently out of thin air, we have two of each.

Exercise: Why is it justified for both branches to inherit the whole inventory?

Exercise: Can you play the game using backward reasoning, without using any explicit dup actions?

Back and forth

In summary, here’s how backward reasoning works more generally:

• If we have an action f : A, B -> C, and our current goal is to make C, then we can apply f backwards to fork the game state into two branches, one whose goal is A and one whose goal is B. The inventory of each branch is identical to the original inventory.

Diagrammatically, we can represent backward reasoning as follows:

Importantly, each branch inherits the same inventory (?1) as the original state, because we don’t want to worry about inserting dup actions at the right places all the time, which also makes the diagram much cleaner and easier to read.

Let’s also compare backward reasoning to the forward reasoning diagram:

The following slogans help us remember the difference between forward and backward reasoning:

• Forward reasoning looks at the inventory (what we have).
• Backward reasoning looks at the goal (what we want).

Exercise: Can you complete the following game using a mix of forward and backward reasoning? Is there an order of mixing forward and backward reasoning that takes the fewest number of actions? Is there an order that you find the most intuitive?

Whew!

That was a lot of ground covered. We learned the rules of a game of construction and two different ways of playing it: forward and backward.

Next up, we will introduce new designs to the game to make it a LOT more interesting, making a truly “open-world” game. Our new designs will allow a player to create arbitrarily complex contraptions that even the game designer might not have anticipated. Importantly, though, we will see that what we have been building all along is—believe it or not—logic⁷!