About six years ago on this blog, I started thinking about trying to make a web-based game based around high-school algebra, and ended up using Scratch to write a short but playable puzzle game in which one solves linear equations for an unknown using a restricted set of moves. (At almost the same time, there were a number of more professionally made games released along similar lines, most notably Dragonbox.)

Since then, I have thought a couple times about whether there were other parts of mathematics which could be gamified in a similar fashion. Shortly after my first blog posts on this topic, I experimented with a similar gamification of Lewis Carroll’s classic list of logic puzzles, but the results were quite clunky, and I was never satisfied with the results.

Over the last few weeks I returned to this topic though, thinking in particular about how to gamify the rules of inference of propositional logic, in a manner that at least vaguely resembles how mathematicians actually go about making logical arguments (e.g., splitting into cases, arguing by contradiction, using previous result as lemmas to help with subsequent ones, and so forth). The rules of inference are a list of a dozen or so deductive rules concerning propositional sentences (things like “( AND ) OR (NOT )”, where are some formulas). A typical such rule is Modus Ponens: if the sentence is known to be true, and the implication “ IMPLIES ” is also known to be true, then one can deduce that is also true. Furthermore, in this deductive calculus it is possible to temporarily introduce some unproven statements as an assumption, only to discharge them later. In particular, we have the deduction theorem: if, after making an assumption , one is able to derive the statement , then one can conclude that the implication “ IMPLIES ” is true without any further assumption.

It took a while for me to come up with a workable game-like graphical interface for all of this, but I finally managed to set one up, now using Javascript instead of Scratch (which would be hopelessly inadequate for this task); indeed, part of the motivation of this project was to finally learn how to program in Javascript, which turned out to be not as formidable as I had feared (certainly having experience with other C-like languages like C++, Java, or lua, as well as some prior knowledge of HTML, was very helpful). The main code for this project is available here. Using this code, I have created an interactive textbook in the style of a computer game, which I have titled “QED”. This text contains thirty-odd exercises arranged in twelve sections that function as game “levels”, in which one has to use a given set of rules of inference, together with a given set of hypotheses, to reach a desired conclusion. The set of available rules increases as one advances through the text; in particular, each new section gives one or more rules, and additionally each exercise one solves automatically becomes a new deduction rule one can exploit in later levels, much as lemmas and propositions are used in actual mathematics to prove more difficult theorems. The text automatically tries to match available deduction rules to the sentences one clicks on or drags, to try to minimise the amount of manual input one needs to actually make a deduction.

Most of one’s proof activity takes place in a “root environment” of statements that are known to be true (under the given hypothesis), but for more advanced exercises one has to also work in sub-environments in which additional assumptions are made. I found the graphical metaphor of nested boxes to be useful to depict this tree of sub-environments, and it seems to combine well with the drag-and-drop interface.

The text also logs one’s moves in a more traditional proof format, which shows how the mechanics of the game correspond to a traditional mathematical argument. My hope is that this will give students a way to understand the underlying concept of forming a proof in a manner that is more difficult to achieve using traditional, non-interactive textbooks.

I have tried to organise the exercises in a game-like progression in which one first works with easy levels that train the player on a small number of moves, and then introduce more advanced moves one at a time. As such, the order in which the rules of inference are introduced is a little idiosyncratic. The most powerful rule (the law of the excluded middle, which is what separates classical logic from intuitionistic logic) is saved for the final section of the text.

Anyway, I am now satisfied enough with the state of the code and the interactive text that I am willing to make both available (and open source; I selected a CC-BY licence for both), and would be happy to receive feedback on any aspect of the either. In principle one could extend the game mechanics to other mathematical topics than the propositional calculus – the rules of inference for first-order logic being an obvious next candidate – but it seems to make sense to focus just on propositional logic for now.

## 130 comments

Comments feed for this article

1 August, 2018 at 5:33 am

Åsa-NietzscheThank you so much for making this, it’s a blast!

At the current version, when I get to 3.1(a) (where formulas are introduced) I can’t seem to drag the formulas to the root environment. I am also not able to create new formulas from the existing ones (however I can’t seem to recall if this is possible yet at this stage in the “game”).

I’ve noticed this after resetting my progress, and I’ve tested this in both chrome and firefox with the same result. Are you able to reproduce this error, or am I just missing something?

Once again, such a great learning tool!

1 August, 2018 at 8:11 am

Terence TaoImplication introduction (dragging formulas to the root environment) is only unlocked in Section 4; combining formulas using logical connectives is unlocked (for AND and OR) in Section 5, and for the remaining logical connectives in the subsequent sections in which they are introduced.

1 August, 2018 at 11:09 am

Åsa-NietzscheI’m terribly sorry (and possibly a bit thick), but the exercise text states “To use one of these laws, drag a formula from the Formulas window to a sentence in the Root environment window.” after introducing formulas. Am I stuck in some cached state that resists cache invalidation? At least for me, Exercise 3.1 (a) (‘Given A, formula “B”, formula “C”: deduce C OR (A OR B).’) also has the headline “Section 1: Disjunction introduction”, where I would suspect it to say “Section 3: …”. Am I right to suspect it is mixed up in some weird state for me?

I’ve tried resetting, refreshing without cache and changing browser but nothing quiet seems to work, whereas I was able to complete the exercise in an earlier version. I’m at Version 1.6.2.

If it is of any importance, I’ve been resetting since I’ve had trouble getting Disjunction Introduction to work properly for later exercises.

1 August, 2018 at 11:44 am

Terence TaoYou need to drag the formula to a sentence in an environment, rather than to just the environment. (The section numbering was a typo, now fixed.)

1 August, 2018 at 12:27 pm

Åsa-NietzscheI’m an idiot. Thank you so much for your time and have a great week!

1 August, 2018 at 1:55 pm

Melissa TacyA fun thing to play around with! I wonder about the possibilities of making such things more “beginner friendly”. I guess I’m thinking of a gamification where you start by getting some of the proof and need to fill in gaps with the available objects, at higher levels the gaps would get larger.

1 August, 2018 at 6:59 pm

Jacob H.🤔 although I think some of the “fun” is in figuring out the “trick” to different kinds of proofs. It makes the occasional hours-long struggle worth it, and you definitely don’t forget after a struggle like that

1 August, 2018 at 7:53 pm

Melissa TacyTrue, the best problem is always one that’s a little out of reach. However having a beginner level doesn’t prevent anyone from enjoying more advanced levels, just opens it up to a wider range of people.

2 August, 2018 at 3:03 am

MaxVery nice. (Consider also Smullyan’s logic puzzles.) For easier use in Mobile devices it would be great to be able to “fold away” subsections. (The exercise list already takes up more than a whole screen full.) Maybe the exercise list could also be a in a drop down menu (easy to do with CSS).

2 August, 2018 at 4:51 am

L SpiceTwo more possible UI tweaks, both to do with commutativity. First, is there a reason to have the options available when combining two propositions depend on the order? (I find myself unable to remember whether, for example, I drag NOT A to A OR B, or whether I draw A OR B to NOT A, and it’s not clear to me that the requirement to remember (or, as I do, just try both) is improving the game or my understanding of propositional logic.) Second, if I use the REVERSE DEDUCTION THEOREM to deduce B [ assuming A ] from A IMPLIES B, and if I then use IMPLICATION INTRODUCTION to deduce A [ assuming A ] from formula “A”, then I have two separate “assuming A” environments, with no obvious way to combine them; whereas, if I *first* use IMPLICATION INTRODUCTION, then the two environments are combined. Since it is almost always the latter that I want, maybe it could be made the behaviour in both cases?

2 August, 2018 at 10:49 am

Terence TaoI have now implemented the first suggestion. However, I cannot duplicate the splitting of assumption windows reported in your second suggestion (which should not be the outcome of the code as currently written). Is there an exact sequence of steps you have found that can produce this error?

2 August, 2018 at 6:59 pm

L SpiceI also cannot duplicate the splitting of assumption windows. Either I imagined it in the first place, or it has since been fixed. Thank you!

2 August, 2018 at 9:30 am

Roy DongWhen I was in undergrad, I took a metalogic class that used Barwise & Etchemendy’s “Language, Proof, and Logic”. It came with software that reminds me of this game. (It’s called “Fitch”.) I think it’s definitely worth checking out; it looks like you and B&E had similar goals, but came to different UI implementations for them. It’s really interesting to me how the implementations are different, and, also, I think one or the other would be more effective depending on the type of learner playing the games.

(They also have a software “Tarski’s World” for some very basic model theory, which, in retrospect, helped me greatly in conceptualizing the semantic metamathematics courses I took several years later.)

2 August, 2018 at 2:36 pm

Aaron ChenGreat game/exercises! Three comments:

– Not sure if this was intended, but exercises 12.2a through 13.1a are unlocked together, which means that upon clicking on 13.1a, the formulas TRUE and FALSE show up in the section 12 exercises.

– On a couple of occasions, I had to go back to redo some exercises for them to become usable (refreshing/merely clicking on them didn’t work).

– A UX suggestion would be to allow CTRL to select two (or even multiple [for future additions]) formulas at a time instead of dragging a formula onto another one (an even fancier idea would be to have it so that once a tentative move has been made, to allow selection of the action via hotkeys rather than clicking).

2 August, 2018 at 4:34 pm

Terence TaoI’ve now added ctrl-click and hotkey functionality. (In particular, it is now possible to apply exercises that involve three or more hypotheses, which was not previously possible, using ctrl-click. Thanks for the suggestion!)

The unlocking order is as intended. For a beginner it is best to do the exercises in sequential order, in particular finishing an entire section completely before moving on to the next one, but if one just wants to unlock the sections as fast as possible one just has to do the first exercise of each section. Once this is unlocked, earlier exercises will acquire the tools unlocked by later ones (in particular, once 13.1(a) is unlocked one gains access to TRUE and FALSE, though this is not actually all that helpful for any exercise before Section 13).

Some of the unlocking quirks may be due to version updates between refreshes. If it is a persistent problem, please let me know of a specific way to reproduce the issue and I can try to debug it.

4 August, 2018 at 5:10 pm

Mauricio de OliveiraHello Tao :), the conjunction introduction hyperlink is redirecting to https://en.wikipedia.org/wiki/Conjunction_introduction_target%3D

instead of https://en.wikipedia.org/wiki/Conjunction_introduction

[Fixed in latest version -T.]5 August, 2018 at 9:02 pm

arch1Thanks for doing this! Potential [[deletes]] & [adds] to the Ex. 1.1 explanatory bullets:

• If one drags one [[hypothesis]] [true statement] to another, the Available deductions window below will show what conclusions one can draw [from those statements] using the available deduction rules …

• For instance, to solve this level one drags the B statement onto the A statement (or vice versa), clicks on the button marked “B AND A” [to add that statement to the root environment], drags [[that]] [the new “B AND A” statement] [on]to the B statement ….

• The exercise is completed when you have managed to obtain the desired conclusion (in this case, (B AND A)[ AND B]) …

[Suggestions incorporated into latest version, thanks -T.]6 August, 2018 at 11:31 pm

Brian SlesinskyI’m wondering if 14.1 is supposed to work yet? I tried dragging P(x) and Q(x) to the predefined root and child environments in that exercise and nothing happened. It’s also unclear if I can make a new environment.

—

I also tried redoing 13.1a. The first two steps worked fine:

Deduce A [assuming A]. [IMPLICATION INTRODUCTION]

Deduce TRUE [assuming A]. [TRUE]

I then tried dragging A to TRUE and I don’t get offered “A AND True (assuming A)” as a choice. Instead I’m offered two more complicated choices:

“(TRUE AND A) AND TRUE (assuming A)”

“(A AND TRUE) AND TRUE (assuming A)”

I think the last time I played, it was version 1.8, and I had finished all the exercises.

[This should now be fixed, but if conjunction introduction is still unavailable, try clicking on Exercise 1.1 again. -T]7 August, 2018 at 12:39 am

MichaelIn the current UI it is very hard to guess (I failed) how to prove 7.1 in an optimal way. I need to create an environment with assumption B (inside the environment with assumption A), but I don’t need B inside that environment — how to do it? If I agree to put B inside, an extra (unused) step in the proof is created…

[Fair enough – new version has an alternate push functionality that does not require the unused step. -T]8 August, 2018 at 9:58 am

Terence TaoI am running into some trouble getting a desired layout to occur and am hoping that there are some CSS or layout experts here that can help me.

Right now there are four main windows to create proofs: the “Root environment” window, the “Formulas” window, the “Available deductions” window, and the “Terms” window. (The “Formulas” and “Terms” windows are hidden initially, and are only unlocked in later sections.) There will also be a fourth window (“Predicates/Operators”) to be implemented in the future. I would like a layout in which the location of the “Root”, “Formulas”, “Terms”, and “Predicates/Operators” windows are fairly stable, but in which the “Available deductions” window can become rather long, but in which all five windows can be visible on a single screen if at all possible. (The text has other windows like the Exercises, Proofs, Achievements, and Notifications windows, but it is less essential that these also be visible on a single screen.) The format I currently am implementing is a fixed width 2 x 3 grid

A B C

D E F

in which the root environment occupies position A, formulas occupies position B, terms occupies position D, the future Predicates/Operators window occupies position E, and Available deductions occupies columns C and F. This layout is sort of close to what I would like, except for the behaviour of the height of the elements. Namely, in the event that the available deductions window gets too lengthy, I would like it to keep flowing downwards without resizing the A,B,D,E windows as well. Currently it seems that the A and B windows are stretching to match the available deductions window, which is thus stuck in C and never flows down to F, let alone beyond F.

Probably the better thing to do is to put the root, formulas, terms, and predicates/operators window in a separate element occupying 2/3 of the screen width, and the available deductions in an element occupying 1/3 of the screen width, but I have been having some trouble making such a layout behave properly.

Another issue is that the grid display I am using does not seem to be compatible with IE and Edge, so a solution that is supported by these browsers would be preferable.

8 August, 2018 at 12:20 pm

Maths studentDear Prof. Tao,

I think there are several ways to do this, as so often.

My personal philosophy on webdesign is to use as little div (or similar block) elements as possible, since each increases rendering time. (On slower computers, eg. your website is pretty slow because of this. No offence.)

A solution that would match that paradigm would be to use display:inline-block and float:right (where one would have to set the width accordingly). The right bar would have to precede the others in the HTML code. (I hope I’m not messing up the syntax now, but the specs are easily googlable and w3schools is the link one should click.)

This should be compatible with IE (especially since the new versions ought to have fixed the old box model issue), but maybe the margins are defaulted in a different way in IE, so that they would have to be manually set to zero in order to avoid unwanted linebreaks.

If my solution should not work, you could always use nested divs; eg. you could put ABDE in one div and CF in another and have them display side by side using position:absolute (which positions with respect to the next-higher level block element, not the screen).

8 August, 2018 at 12:36 pm

Maths studentSpeaking of margins, let alone paddings, positions, font-sizes, borders, etc.

(Regarding your blog, I’ve still got my CMS very much on the agenda. At the about section, I had an inquiry regarding that…)

In principle, I could also program the layout and send you a copy of the source per email.

8 August, 2018 at 1:59 pm

redblobgamesFor .deductions change grid-row: 1/2 to grid-row: 1/3. I believe it’s a half-open interval, so 1/2 is only one row and 1/3 is two rows. (I am new to css grid and was expecting it to be a closed interval)

CanIUse says Edge should support css grid https://caniuse.com/#feat=css-grid and the grid seems to be working for me in Edge.

8 August, 2018 at 3:35 pm

Terence TaoThanks! Setting grid-row to 1/4 actually gave the behaviour I wanted, namely that lengthening the deductions window had no impact on the placing of the other windows. Perhaps there is a leaner and more elegant solution, but this seems “good enough” for now.

Currently the page is not working on Edge, but the problem was not the grid as I had thought, there seems to be a bug in Edge regarding how localStorage is handled https://developer.microsoft.com/en-us/microsoft-edge/platform/issues/14930573/ . I assume this will get patched eventually so I am not sure whether it is worth trying to make a workaround for it now.

[UPDATE: weirdly, the edge localStorage bug only shows up for my local copy of the code, not the one on the web page, so actually it’s a bug that only affects me! ]9 August, 2018 at 12:10 am

Corentin LouboutinHi, thank you for the website, it’s very interesting and I have a lot of fun doing the exercises, however, since the last update, I’m facing a interface bug. See : https://i29.servimg.com/u/f29/19/02/08/32/screen10.png

I’m using firefox with fedora (I think its 22 but I’m not sure).

I hope you can solve

9 August, 2018 at 7:29 am

Terence TaoIt seems that the grid layout I am using is supported from version 54 of Firefox onwards; I encountered the same issue with an older version of Firefox when testing just now, but the problem resolved once I updated to the latest version.

9 August, 2018 at 8:50 am

Corentin LouboutinOk, thank you very much !

12 August, 2018 at 12:22 pm

curiousDoes propositional logic help extract grammar from scenes in vision?

16 August, 2018 at 1:34 am

Antoine DeleforgeHello,

It looks like starting from section 14, most exercises are not reusable once they are solved. The only exceptions are 15.2(a-c), 18.2(b), 19.2(a-b) and 21.1, which are all re-usable. But I am not able to reuse, for instance, exercises 17.2, 18.2(a), 18.4, 18.5, 18.6, 20.1, 22.2, 22.3(a-b), though they could all be helpful in shortening some subsequent proofs. Is it due to a bug occuring on my side or is it intended?

Thanks !

16 August, 2018 at 6:05 am

Terence TaoI haven’t been able to come up with a good general matching algorithm yet for exercises that involve predicates, for two reasons. One is non-unique matching: for instance, if one wants to express in the form , then one could choose and , or and , or and equal to any variable other than . the other problem, potentially more serious, is the need to carefully check side conditions. For instance, right now, given “THERE EXISTS X: A”, one can deduce “FOR ALL X: A”, by pulling A (which does not depend on x) out of a “setting x” environment and then pushing it into a “let x be arbitrary” environment. However, if one then tries to use this deduction with A replaced by something that involves X, then one gets an invalid deduction: for instance, given “THERE EXISTS X=0”, one cannot deduce “FOR ALL X: X=0”. So to reuse this exercise, the code has to somehow know that A must remain independent of X. [In some cases I was able to prevent this by requiring that the conclusion be well-formed (e.g. does not use any free variables that are not introduced in the ambient environment, but the above example is the first instance where the well-formed requirement is insufficient.)

For certain key laws and exercises I have been implementing the matching by hand, writing special code for each such law. But this isn’t really a scaleable solution (and I’m finding that a lot of bugs can be introduced by this). So I’m not sure how to proceed in general.

18 August, 2018 at 3:15 pm

QED version 2.0: an interactive text in first-order logic | What's new[…] readers who have followed my previous post will know, I have been spending the last few weeks extending my previous interactive text on […]

18 August, 2018 at 3:21 pm

Terence TaoAs the number of comments to this post is getting rather large, I recommend people wishing to report bugs, make suggestions, or offer other feedback use the new blog post for QED: https://terrytao.wordpress.com/2018/08/18/qed-version-2-0-an-interactive-text-in-first-order-logic/

1 September, 2018 at 1:46 am

Resumen de lecturas compartidas durante julio de 2018 | Vestigium[…] Gamifying propositional logic: QED, an interactive textbook. ~ Terence Tao #Teaching #Logic […]

20 December, 2019 at 2:28 pm

יומיות 02.08.2018: הקונגרס למתמטיקה 2018 התחיל, וכבר הוענקו מדליות פילדס | ניימן 3.0[…] בפינה מבדחת. טרנס טאו, אולי המתמטיקאי הגדול של זמננו, הכין משחק מחשב כיפי שאמור ללמד […]