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.

## 124 comments

Comments feed for this article

28 July, 2018 at 7:00 pm

AlexiThanks for making this! I always get so excited to see math education forward progress, and I would count a truly interactive text as part of what we should head toward. I’ll need to try this on a computing device other than my iPhone.

28 July, 2018 at 7:13 pm

jrThis is awesome! It reminds me of edukera.com, a platform that teaches formal logic in a similar way (first order logic works really well too; and they seem to have ambitions of going beyond logic; they have an experimental calculus module for instance).

28 July, 2018 at 9:03 pm

Jacob H.What a great little app. minor erratum: exercise 6.1(a) says “(or the condiional)”

[Corrected, thanks – T.]28 July, 2018 at 10:10 pm

Stuart Errol AndersonAt high school, one my math teachers introduced us to WFF’N PROOF. A WFF is a well formed formula. In the game, students must be able to recognize a WFF and use seven different Rules of logic to manipulate those WFFs into a proof. Games are played in groups of two or three. The first player rolls the cubes and sets a WFF as a Goal. The goal is the conclusion

of a proof. Each student then tries to construct a proof that ends with

the goal. The Solution to the goal is the premises which they started their proof with, and the rules they used to get to the goal.

https://www.oercommons.org/authoring/1364-basic-wff-n-proof-a-teaching-guide/view

28 July, 2018 at 11:33 pm

BrianHow do I move on from Ex 1.1?

28 July, 2018 at 11:39 pm

BrianOK got it

29 July, 2018 at 12:34 am

Brahadeesh SankarnarayananCan you let me know how you got it? I’m stuck on Ex 1.1.

29 July, 2018 at 1:07 am

Brahadeesh SankarnarayananAaand, now I feel foolish. Never mind.

29 July, 2018 at 4:35 am

DaveOK, why not let us foolish people in on the secret so we won’t have to keep asking it over and over? :)

It doesn’t seem to work in Internet Explorer 11: dragging the A box over the B box does not result in A AND B.

In Firefox 52.9ESR I get a box labeled A AND B; clicking on that box adds the A AND B proof step, but I see nothing relevant to click on from that point.

29 July, 2018 at 6:40 am

Terence TaoHmm, you’re right about Internet Explorer 11. I guess something in the javascropt is not supported on that browser (presumably relating to a drop event listener), will try to pin it down. Works in Edge 42 and Chrome 67 though.

For Firefox, this is the correct behaviour if one drags A to B. Try also dragging B to A.

Browser issues aside, though, it does seem though that Exercise 1.1 (which was intended as a “tutorial” exercise) is not sufficiently self-explanatory. I would appreciate any suggestions to make it more so.

29 July, 2018 at 7:02 am

Terence TaoAh, I think I found the IE problem: I was assuming that the browser supported local storage (to save progress between sessions), but it seems that some browsers do not. I’ll update the code to disable the local storage features if they are not available.

29 July, 2018 at 8:12 am

Terence TaoI’ve now updated the code so that it runs in browsers such as IE and Opera that do not support local storage. (Of course, with such browsers, your progress will not be saved between sessions.) I’ve also now displayed all the exercises that have not yet been unlocked as disabled (red) buttons. (This clutters the screen a bit, unfortunately, but it now gives a sense of how much of the text one has already completed.) Incidentally, I would be happy to accept any suggestions on how to improve the graphical layout of the text (I do not have any formal design or GUI experience).

29 July, 2018 at 4:27 pm

ihendersonOne nice UI improvement would be to highlight the “drop target” as you’re dragging a statement over another compatible statement (to emphasize the fact that the two statements will interact when you release the mouse button).

29 July, 2018 at 12:59 am

TimoGreat idea, thank you, Terry!

If you are interested in it historically, there were many forms of logic games and interactive logic, especially in the middle ages, most prominently a practice called “obligatio”. This short paper introduces it quite well: http://apcz.umk.pl/czasopisma/index.php/LLP/article/view/LLP.2012.020

Best wishes.

29 July, 2018 at 2:28 am

Marvin MeyerUnfortunately I am stuck on Exercise 1.1 as well. How to proceed, what is to do? From the explanations it is not clear to me what the content of the exercisr is.

31 July, 2018 at 4:01 am

Hugodragging the B box over the A box result in B AND A.

29 July, 2018 at 3:14 am

AnonymousIs it possible to describe each proposition as a vertex of some (abstract) graph such that any proposition is connected by some directed(!) edges to some other propositions (represented by some vertices) from which it can be deduced?

Is it possible (for some simple inference problems), to prove that some proposition follows from others just “by inspection” that the new proposition is connected (via some edges) to the other propositions?

Using available advanced graph theory tools, it seems that such graph theoretic approach (with possible combination of “deep learning” tools) may lead to some nontrivial mathematical discoveries.

29 July, 2018 at 4:32 am

DmitriyFun game, thanks!

I’m confused though. According to the description, “this text contains thirty-odd exercises arranged in twelve sections”, but I’m only able to access 13 exercises in 7 sections. After completing exercise 7.1 I got a congratulatory message implying I’ve reached the end, and no further exercises are available.

29 July, 2018 at 5:25 am

VassilyDoes anyone know of anything similar to: http://www.math.ucla.edu/~tao/QED/QED.html It was a great fun but it ended in 5 minutes unfortunately.

29 July, 2018 at 8:12 am

Anton Trunov (@Anton_A_Trunov)Hi! You might like http://logitext.mit.edu/main or already mentioned https://www.edukera.com. There is also “Introduction to Logic” course on Coursera by Mike Genesereth (https://www.coursera.org/learn/logic-introduction/. Also, proof assistants (e.g. Coq) are pretty fun too :)

29 July, 2018 at 12:28 pm

Antony Karl BartlettThe Incredible Proof Machine? http://incredible.pm/

29 July, 2018 at 5:43 am

Luis IgnacioEr… Tao, i think there is an error: “var Exercise72 = new Exercise(“EXERCISE 7.2”, “DOUBLE PUSH”, [A, environmentcontext([B,C])], assuming(assuming(A,C),B));

Exercise72.unlockedBy(Exercise71);

Exercise72.notes = ‘This is an easy consequence of the push law, but turns out to be convenient in some subsequent exercises.’

“

29 July, 2018 at 5:43 am

Luis IgnacioUncaught ReferenceError: environmentcontext is not defined

at QED.html:158

29 July, 2018 at 6:28 am

Terence TaoGah! The “c” in context should have been capitalised. Fixed now. (Unfortunately, anyone who has gotten to that exercise or the one preceding it may need to reset the text in order to be able to unlock this exercise and the subsequent ones.)

29 July, 2018 at 11:06 am

zrabelThis is great! I wonder if this could be useful next time I teach discrete math. Minor typo: In the statement of 7.2, I believe “[assuming B,C]” should only appear in the deduction, not the given. Also, 12.4b is possible in 13 lines!

29 July, 2018 at 12:44 pm

Joerg GrandeThanks for the nice diversion.

There is a typo in the popup box after exercise 1.1: “quad” should be “quod”.

[Corrected, thanks – T.]29 July, 2018 at 12:51 pm

ahartelThanks for this very nice game. I like the idea very much.

There is a minor suggestion for improvement I have: When (accidentally) clicking twice on one of the available deductions then that same deduction gets added twice to the proof list and the root environment. This will also happen when the proof is already complete (in which case two extra lines get added for each click, namely the deduction itself and another QED). When this first happened to me accidentally I found it a bit annoying because it made my score (number of proof lines) look bad. But in general it didn’t decrease the fun of the game too much :)

[Thanks for the idea! Now implemented – T.]29 July, 2018 at 2:00 pm

coryThis was fun. I believe there is a mistake at 12.1(c) – if we assume B and get a contradiction how could we deduce B? At 12.4(b), does the caveat “not using anything at this exercise” suppose to prevent us from using the deduction of (NOT(NOT(A))) from A? (otherwise it is possible to solve it with 7 lines and 12.5(d) seems to be solvable with 9 lines)

[Now corrected, thanks. Also thanks for pointing out the shorter proofs. – T.]29 July, 2018 at 2:41 pm

Anton FarmarIt’s worth noting that there are an awful lot of logic ‘games’ in the same vein as this, such asThe incredible proof machine (http://incredible.pm/) and Logitext (http://logitext.mit.edu/main). I’m really glad you find this interesting, as I personally really love this sort of puzzle!

29 July, 2018 at 2:45 pm

Marisa KirisameI am getting undefined… see https://imgur.com/a/w3jrecw

[Now corrected, thanks – T.]29 July, 2018 at 3:25 pm

Crusttypo in 2.2(a): (such as A or B can -> (such as A or B) can

[Now corrected, thanks – T.]29 July, 2018 at 3:53 pm

New top story on Hacker News: Gamifying propositional logic: QED, an interactive textbook – World Best News[…] Gamifying propositional logic: QED, an interactive textbook 5 by robinhouston | 0 comments on Hacker News. […]

29 July, 2018 at 3:56 pm

New top story on Hacker News: Gamifying propositional logic: QED, an interactive textbook – News about world[…] Gamifying propositional logic: QED, an interactive textbook 6 by robinhouston | 0 comments on Hacker News. […]

29 July, 2018 at 3:57 pm

New top story on Hacker News: Gamifying propositional logic: QED, an interactive textbook – Tech + Hckr News[…] Gamifying propositional logic: QED, an interactive textbook 6 by robinhouston | 0 comments on Hacker News. […]

29 July, 2018 at 3:58 pm

New top story on Hacker News: Gamifying propositional logic: QED, an interactive textbook – Latest news[…] Gamifying propositional logic: QED, an interactive textbook 6 by robinhouston | 0 comments on Hacker News. […]

29 July, 2018 at 4:30 pm

Terence TaoThanks for all the feedback! The new version has corrected the errors pointed out and also implemented the no-double-click feature. Also I have moved the achievements and notifications windows to be side-by-side, and have the achievements go from newest to oldest rather than vice versa. One or two more exercises have also been added (but if you want to access them, you may need to reset the text which will mean that you will have to redo the exercises.)

I have also now indicated below each exercise the shortest length of proof I can find using the tools provided up to that exercise. (These exercises will tend to get much shorter proofs though after the exercise is solved, in particular one can often use the exercise to solve itself in a handful of lines.) If anyone can improve upon any of these lengths, please let me know and I will acknowledge your contribution in the next version of the game.

29 July, 2018 at 4:45 pm

Gamifying propositional logic: QED, an interactive textbook – TARIAN LIMITED[…] 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 …Read More […]

29 July, 2018 at 5:17 pm

Brian SlesinskyI’m stuck at exercise 5.2. This exercise is about creating nested assumption boxes, but I don’t see a way to do so in the UI. (I can separately assume any of {A,B,A AND B} at top level, but don’t see a way to nest, combine, or split assumptions.)

29 July, 2018 at 5:24 pm

Brian SlesinskyIt turns out this was because I had forgotten the UI interaction used to solve 4.1. (After solving it once, you don’t technically need it again.) Maybe repeat the directions for drag and drop?

[Thanks for the suggestion, I have added a line to the text for Exercise 5.2. -T]29 July, 2018 at 5:21 pm

Adam Nemecek (@a_nemecek)Are you aware of linear logic, aka the gamified version of classical logic? It’s a fascinating formalism, basically it’s classical logic with two players. I see some deep connections between QED and linear logic (the fact that QED is a game of sorts is only the beginning). I’m also strongly convinced that it’s a superior logic for mathematics, as for example all optimization falls outside of classical logic but linear logic can handle it.

The wikipedia entry is actually pretty good https://en.wikipedia.org/wiki/Linear_logic

29 July, 2018 at 5:39 pm

Fred Johnsenhttps://en.wikipedia.org/wiki/Tarski%27s_World

29 July, 2018 at 8:22 pm

Nazgand8.1(b) should not be provable with less than 3 lines. I am not seeing the notification for matching the shortest known proof.

EXERCISE 8.1(b) was reproved in 3 lines.

EXERCISE 8.2 was reproved in 7 lines.

You matched the record for the shortest known proof!

29 July, 2018 at 8:39 pm

NazgandPerhaps the buttons which would result in circular proofs should be a different color so the player knows that clicking them would not count toward breaking records. Similarly, if the colored buttons are used, the following popup should not appear.

EXERCISE 8.4(a) was reproved in 3 lines. A new personal best!

You

beatthe record for the shortest known proof! If your proof was non-circular (that is, it did not use the current exercise, or any rules obtained subsequently to this exercise), please send it to me at tao@math.ucla.edu and I will update the record (with an acknowledgment) in the next version of the text.29 July, 2018 at 8:56 pm

NazgandA IMPLIES (B IMPLIES C). [given]

Deduce A AND B [assuming A AND B]. [IMPLICATION INTRODUCTION]

From A IMPLIES (B IMPLIES C): deduce A IMPLIES (B IMPLIES C) [assuming A AND B]. [PUSH]

From A AND B [assuming A AND B]: deduce A [assuming A AND B]. [CONJUNCTION ELIMINATION (left)]

From A [assuming A AND B], A IMPLIES (B IMPLIES C) [assuming A AND B]: deduce B IMPLIES C [assuming A AND B]. [MODUS PONENS]

From A AND B [assuming A AND B]: deduce B [assuming A AND B]. [CONJUNCTION ELIMINATION (right)]

From B [assuming A AND B], B IMPLIES C [assuming A AND B]: deduce C [assuming A AND B]. [MODUS PONENS]

From C [assuming A AND B]: deduce (A AND B) IMPLIES C. [DEDUCTION THEOREM]

QED! (again)

The shortest non-circular proof I can see for EXERCISE 8.4(a) is the 9 lines above, yet a record of 8 lines is claimed to be the shortest known.

I thus request an answer key containing a record shortest known proof for each exercise.

29 July, 2018 at 8:32 pm

Gamifying propositional logic: QED, an interactive textbook | Terry Tao - Nevin Manimala's Blog[…] by /u/tick_tock_clock [link] […]

29 July, 2018 at 10:20 pm

Gamifying propositional logic: QED, an interactive textbook | Infozonic[…] Read More […]

29 July, 2018 at 10:56 pm

redblobgamesCool! If you’re looking for any suggestions for styling, I made some minor changes here: https://www.redblobgames.com/x/1830-terence-tao-qed-textbook/ (made locked exercises less bright so that the eye is drawn towards the currently active ones; replaced some borders with box-shadow; set mouse pointer; added mouseover effect; added contrast inside root and formula windows)

29 July, 2018 at 11:50 pm

Terence TaoThanks for the suggestions and code! This is now implemented in the latest version, together with a feature to view completed proofs in the notification window.

29 July, 2018 at 11:10 pm

Brian SlesinskyI noticed that clicking on any hyperlink causes you to lose any work in progress on the current proof when you go back. Perhaps links should open a new tab instead? (Apparently will do this.)

Also, I noticed that after reloading the page, it remembers which exercises were completed, but not their proofs. (At one point I wanted to go back and look at how I did a previous proof since I had forgotten how I did it.)

[The latest version now stores proofs in the notifications window, though you may have to reset the game first to make this feature available, unfortunately, -T]30 July, 2018 at 12:20 am

New top story on Hacker News: Gamifying propositional logic: QED, an interactive textbook – ÇlusterAssets Inc.,[…] Gamifying propositional logic: QED, an interactive textbook 105 by robinhouston | 7 comments on Hacker News. […]

30 July, 2018 at 1:06 am

Roger Joseph WitteYou need to play with Coq, a logic game for professional homotpists ;)

30 July, 2018 at 1:10 am

LukeAfter completing Exercise 7.1, it says that I am a Master in propositional logic! Well done, Luke, well done!! ;)

30 July, 2018 at 1:24 am

Hamish ToddThis is cool! You may be aware that there is a whole community of us making “Explorable explanations” http://explorabl.es

One of my favourites, on special relativity, is this one https://www.youtube.com/watch?v=RQGa0DPwes0

30 July, 2018 at 3:18 am

L SpiceOn Mobile Safari (at least on my iPad), dragging one item onto another is frequently dodgy: for exercise 1.1, dragging B onto A would usually just give me “From B, …” rather than “From B and A, …”. (I tried it quite a few times. Once it happened, it would keep happening, but occasionally a refresh fixed it.) It works flawlessly on Desktop Safari, so I’m not sure what could be happening.

30 July, 2018 at 3:24 am

L SpiceAlso, is it possible to abandon a proof in progress (to try a different approach) without resetting the game entirely?

[Click on the exercise button again to restart a proof in progress; alternatively, refresh the page. -T]30 July, 2018 at 3:28 am

Adriano ArceTypo in the 5th bullet of Exercise 11.1: “A OR (NOT A)” should instead be “A AND (NOT A)”.

[Corrected, thanks – T.]30 July, 2018 at 3:53 am

John MangualThere are a number of user interface issues. There are even people who only study human-computer interaction. Here, perhaps you’d like to make all the exercise tiles the same width? (height is already the same).

Logic is really good for situations where common sense fails. In a newspaper article, it might be fun to replace the named entities with variables and the various relationships with arrows.

30 July, 2018 at 5:13 am

L SpiceOne more request. Would it be possible to have exercises to which I have found a shortest known solution appear in a different colour from ones for which I have found a, but not a shortest known, solution? (I also amend a previous request. I discovered that clicking again on an exercise will reset the proof; can I *backtrack* in the proof without resetting?)

30 July, 2018 at 5:25 am

AnonymousSome minor feedback from an unintelligent person, if it is of any use to you: Exercise 7.1 states “If a statement is known without an assumption, then it can be “pushed” into an enviroment with that assumption”. However, in order to solve the exercise, you are required to assume A. Perhaps confusion may be avoided if you were to either reword that statement, or to put A in the root environment for this exercise?

[Another line of explanation added. -T]30 July, 2018 at 10:45 am

JairThis is excellent! I wish I had had a tool like this when I was teaching (or learning) logic.

– Jair

30 July, 2018 at 11:54 am

Terence TaoNew features for Version 1.4:

* Exercises now organised by section.

* “Immediate undo” button that can undo a deduction if it is selected immediately after the deduction was made, and if the deduction did not solve the problem.

* Exercises that were proven are now either green or blue, depending on whether the shortest known length was attained (or surpassed) or not.

30 July, 2018 at 4:45 pm

Terence TaoVersion 1.5:

* Once one completes all the exercises, each exercise will contain a button that one can click on to expand out the shortest known non-circular proof for that exercise. (While coding this, I found out that some of the shortest lengths claimed were not correct; they are now adjusted.)

* As per Brian’s suggestion, a new exercise (4.2) has been added to give alternate functionality to implication introduction (at least at the root level; to use implication introduction in sub-environments, one still needs to use drag-and-drop).

30 July, 2018 at 6:56 pm

L SpiceYour responsiveness and the rapid evolution are great. The new changes make the whole much improved (and a refresh captures them without requiring to reset QED, too). Thank you!

31 July, 2018 at 6:42 pm

Terence TaoVersion 1.6:

* Laws that appear in the text at or after a given exercise can still be used in proofs, but have an asterisk next to them, and proofs using such laws do not qualify for shortest length records.

* New boolean connectives, TRUE and FALSE, and a new section (Section 13) to test out these connectives. Also two more exercises added to Section 9.

2 August, 2018 at 10:46 am

Terence TaoVersion 1.7:

* Dragging is now symmetric: dragging X to Y will also check for laws previously available by dragging Y to X. (As a consequence, though, Exercise 1.1 had to be changed as it was now redundant, and so legacy players may artificially have a world record on this exercise.)

* Many windows of the game are now collapsed by default.

* A number of “invisible” code changes in preparation for extension to first-order logic. These should not affect the gameplay thus far, however there is the possibility that some unusual new bugs may have been created by these changes.

3 August, 2018 at 12:57 pm

Terence TaoVersion 1.8:

* A “restart exercise” button added (functionally equivalent to clicking on the button of the current exercise again)

* This change is a bit technical. There are some laws and exercises which do not specify a target environment, so their conclusion is produced by default in the root environment. In those cases, an alternate version of the law has now been added with an additional input of the target environment, in particular allowing for insertion into an arbitrary environment (not just the root) without the need for any additional PUSH type law. For instance, if the law was previously activated by clicking on a formula, it can now also be activated by dragging the formula to an environment. (In some cases there may now be three hypotheses, and the ctrl-click functionality of the previous version would be needed to use this form of the law.) This change will be needed in the upcoming expansion to predicate logic, because there are certain tautologies (involving free variables) which will not be legal sentences in the root environment, but only in sub-environments where certain variables are defined. One consequence of this change is that Exercise 4.2 became completely redundant and has thus been deleted.

* More “invisible” code changes (basically generalising the notion of an environment, and setting up the constructors etc. for free variables and the like). As usual, please report any new bugs you discover here.

4 August, 2018 at 7:55 pm

Terence TaoVersion 1.9:

* Environments are now clickable (this is important for laws that involve three or more inputs, one of which is an environment)

* More hotkeys: “u” for undo, “r” for reset exercise.

* Bugfixes: bad HTML link repaired, and variants of laws that take an extra environment input are now no longer automatically considered circular to use.

* Alpha introduction of some predicate logic in Sections 14 and 15 (still very preliminary so far). Ordinarily I would wait until a more complete predicate logic component of the text is fully developed and then releasing a beta version, but given the current level of interest, I’ll try a strategy of adding features incrementally instead and releasing for playtesting. Currently only two components of predicate logic are implemented: free variable environments, and pushing into such environments. More to come…

5 August, 2018 at 8:22 pm

Terence TaoVersion 1.10:

* Another alpha section, Section 16, introducing the ability to introduce free variables into an environment by dragging in from a new Term window (which also has a button to create as many free variables as are needed).

* code.js file split into two smaller files as it was becoming unwieldy (also this may help make the code more modular in the future).

7 August, 2018 at 8:31 am

Terence TaoVersion 1.11:

* Some bugs that led to some deductions not being available have been fixed. However, there may be issues with game states from legacy versions. If a law you are expecting (e.g. conjunction introduction) is still unavailable, try clicking on the relevant exercise that introduces that law (this will be the first exercise in a section). If all else fails, reset the text.

* Alternate push functionality added: one can push into an assumption by dragging the sentence to a formula containing the assumption, rather than the assumption itself. This saves a step in Exercises 7.1 and 7.2 (and possibly other exercises as well).

* Alpha version of new section: Section 17, introducing universal quantification and bound variables.

7 August, 2018 at 3:11 pm

Terence TaoVersion 1.12:

* Alpha version of new section: Section 18, introducing universal specification and primitive terms, and a couple of exercises.

7 August, 2018 at 9:10 pm

Terence TaoVersion 1.13:

* Alpha version of Section 19, introducing the existential quantifier and the law of existential instantiation, which also introduces a new type of subenvironment (where a free variable is set, rather than ranging arbitrarily).

* Section 10 reorganised with the addition of a new helper exercise (Exercise 10.3) that shortens the proofs of various later exercises involving IFF. Legacy players may have to redo some of the Section 10 material to restore the laws unlocked in this section properly.

* New hotkeys: ‘n’ for first available unsolved exercise, and ‘N’ for last available unsolved exercise.

9 August, 2018 at 1:09 pm

Terence TaoVersion 1.14:

* Deductions resulting in non-well-formed formulas will still be listed, but greyed out and unavailable for selection.

* New helper exercises in Sections 13, 15 (and some renumbering in Section 13; unfortunately this means that legacy players may have to redo some of these exercises).

* Main windows of text now organised in a grid layout, as per other comments in this thread.

* An important omission in the law of universal specification (from FOR ALL : and a term , deduce ) that I had overlooked has been corrected: it is essential that the term not contain any bound variables! Otherwise we could have absurdities such as this: starting from the true statement FOR ALL : THERE EXISTS : in the natural numbers, one could “specify” to equal the term to conclude the false statement THERE EXISTS : .

* Alpha versions of new sections: 20 and 21. Section 20 introduces a “PULL” law that allows one to pull statements out of “setting s.t. ” environments (providing that does not depend on ). Section 21 introduces the “EXISTENCE” law, that asserts that at least one object in the domain of discourse exists (i.e., we are not working in a free logic).

11 August, 2018 at 9:41 pm

Terence TaoVersion 1.15:

* Fixed a bug with universal specification.

* Section and exercise layout has been revamped.

* Alpha version of Section 22, introducing the law of existential introduction, and a number of exercises including most of the classical syllogisms.

* some helper exercises added to shorten proofs, but more should be done in this regard. (Many of the exercises in Section 22 are a little tedious right now, in part because most exercises at this point cannot be reused to prove later ones because I have not been able to come up with a good general matching algorithm that covers all cases. Instead, I have been coding matching for the key laws (e.g. existential introduction) by hand.)

* various technical changes to data structures. Hopefully all bugs caused by this have been squashed, but it is possible that some functionality that was previously correct could be glitchy right now.

* Experiencing a weird visual bug where occasionally clicking on a button will temporarily blank some screen elements. The bug is sporadic and I have not yet been able to track down the cause (a memory leak?).

13 August, 2018 at 10:47 pm

Terence TaoVersion 1.16:

* Alpha version of Section 23, introducing the predicates and operators window that can be used to create compound terms and predicates.

* Various bug fixes, mostly to do with matching. Some new exercises.

3 August, 2018 at 11:27 pm

AndreThis is a reply to Version 1.8, Firefox 61.0.1, Exercise 7.1 is broken,

Step 1 create Assume A env

Step 2 inside Assume A env create B env

Step 3 (push A down to B) doesn’t work for me

4 August, 2018 at 8:39 am

Terence TaoThanks for finding this bug! It was a consequence of some of the “invisible” code changes I had made in which I was generalising the notion of an assumption. I think it’s fixed now.

7 August, 2018 at 4:15 am

Antoine DeleforgeThanks a lot for this!

Exercise 14.1 does not work for me. When I try to drag P(x) or Q(x) on the “let x be arbitrary” environment, I only get “No available deductions can be formed from this selection.” I use Chrome on Windows 10. As I started the game on an early version I tried to reset QED and redo the exercises until 14.1, but it didn’t help.

[Should hopefully be fixed now, though another reset may possibly be required, or at least clicking again on all the exercises that introduce laws. -T]8 August, 2018 at 3:23 am

Antoine DeleforgeYes, it works now, thanks a lot. I immediately became addicted to this game, and not being able to progress was quite frustrating! I am wondering what will be your next step after 1st order logic.

8 August, 2018 at 4:20 am

Antoine DeleforgeIn Exercise 19.1: The hyperlink for “existential quantifier” appears to span 3 lines. Similarly, the last 3 lines of text are in bold.

A suggestion for Exercise 15.2: introducing “DOUBLE PUSH (for free variables)”, which would be convenient for subsequent exercises.

[Now implemented in latest update – T.]12 August, 2018 at 4:03 am

AndreThis is a reply to Version 1.15, Firefox 61.0.1, Exercise 16.1 is broken

(having solved all previous exercises in an unreproducible order)

If I would like to drag the free variable x to the root env, all I get is

“letting y be arbitrary”

12 August, 2018 at 9:14 am

Terence TaoThanks for this! This should now be fixed (but you may need to force refresh your web page).

12 August, 2018 at 12:58 pm

AndreThis is a reply to Version 1.15.1, Firefox 61.0.1, Exercise 21.1 seems to be broken

(having solved all of 1-8, 9.1a, 10.1a, 11.1, 12.1a, 13.1a, 14-20)

So now I see a

Environment “Set x s.t. TRUE” and inside

“TRUE”, “FOR ALL X: A”

if I drag ‘x’ or ‘X’ onto the “FOR ALL X: A” statement, I get both times a “Universal Specification” deduction which isn’t selectable

[This bug is fixed as of version 1.15.2. -T]30 July, 2018 at 3:43 pm

Brian SlesinskyA UI suggestion: after clicking on any formula, show a button to assume that formula at top level. (As an alternative to the drag and drop gesture.)

This seems better because it seems a bit odd to show a button that says “A and A [assuming A]” but not “A [assuming A]”, which is the more common action?

31 July, 2018 at 6:13 am

L SpiceFor Exercise 9.1(a) in Safari, I proved B OR A [assuming A OR B]. However, if I (1) try to drag A OR B onto B OR A [assuming A OR B] to apply modus ponens, or (2) try to drag B OR A [assuming A OR B] to the root environment (to deduce that (A OR B) IMPLIES (B OR A)), then I am told that no deductions are available from the given selections. This problem survives a refresh (and re-doing the same proof). The same proof in Firefox works fine, so this seems to be a bug.

31 July, 2018 at 7:48 am

Terence TaoWhen performing (1) or (2), what is listed in the “From” line above the notification that no deductions are available?

31 July, 2018 at 5:15 pm

L SpiceFor (1), “From A OR B, B OR A [assuming A OR B]”. For (2), “From B OR A [assuming A OR B], [root environment]”. I took screenshots if it helps, though I can’t imagine how it would. Could this have been caused by my starting with Version 1.3, and then continuing after the update to Version 1.5?

31 July, 2018 at 6:40 pm

Terence TaoSounds like the modus ponens and deduction theorem was lost through the version update (probably because of a slight name change having to do with adding HTML to the name of the law). This should presumably be verifiable through inspection of the Achievements window. You can try clicking on the exercises which supply these laws (6.1(a) and 8.1(a)) which should restore these laws. (If not, then there is always the reset button…)

31 July, 2018 at 6:40 pm

L SpiceI think that my issue was the same as that of @AntonyKarlBartlett. Once I re-solved Exercise 8.1(a), I was able to use MODUS PONENS as expected.

31 July, 2018 at 7:21 am

Antony Karl BartlettProgress is indeed saved between sessions, but upon returning to the latest exercise the tools needed to complete it might not be unlocked (I had to click through all the previous exercises to unlock what I needed for the next exercise).

31 July, 2018 at 7:46 am

Terence TaoI am not able to duplicate this phenomenon (it may have been caused by the text being replaced by a new version between the previous session and the current one). If you can find a reliable way to produce the bug (e.g., by performing a specific sequence of exercises, refreshing, and then noticing that certain rules of inference are missing), please let me know.

31 July, 2018 at 7:53 am

Antony Karl BartlettYes, probably happened because I was between versions, because I can’t duplicate this phenomenon now either. Thanks.

31 July, 2018 at 12:35 pm

Paul DancstepIn terms of “gamifying” math learning, the Exploratorium is working on something in a similar spirit for exploring arithmetic:

The Digital Abacus

1 August, 2018 at 3:49 am

L SpiceIf a rule is proven multiple times, then it appears multiple times whenever applicable. For example, I have proven DOUBLE PUSH twice in an attempt to find the shortest proof; and now, when solving Exercise 8.4(b), I get “From (A AND B) IMPLIES C, [assuming A, B]: DOUBLE PUSH: (A AND B) IMPLIES C [assuming A, B]; DOUBLE PUSH: (A AND B) IMPLIES C [assuming A, B]”.

1 August, 2018 at 8:10 am

Terence TaoDuplicate unlocking of laws has now been prevented in the latest version, thanks for pointing out the issue.

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.