I had another long plane flight recently, so I decided to try making another game, to explore exactly what types of mathematical reasoning might be amenable to gamification.  I decided to start with one of the simplest types of logical argument (and one of the few that avoids the disjunction problem mentioned in the previous post), namely the Aristotlean logic of syllogistic reasoning, most famously exemplified by the classic syllogism:

• Major premise: All men are mortal.
• Minor premise: Socrates is a man.
• Conclusion: Socrates is a mortal.

There is a classic collection of logic puzzles of Lewis Carroll (from his book on symbolic logic), in which he presents a set of premises and asks to derive a conclusion using all of the premises.  Here are four examples of such sets:

• Babies are illogical;
• Nobody is despised who can manage a crocodile;
• Illogical persons are despised.

• My saucepans are the only things that I have that are made of tin;
• I find all your presents very useful;
• None of my saucepans are of the slightest use.

• No  potatoes of mine, that are new, have been boiled;
• All of my potatoes in this dish are fit to eat;
• No unboiled potatoes of mine are fit to eat.

• No ducks waltz;
• No officers ever decline to waltz;
• All my poultry are ducks.

After a certain amount of effort, I was able to gamify the solution process to these sort of puzzles in a Scratch game, although I am not fully satisfied with the results (in part due to the inherent technical limitations of the Scratch software, but also because I have not yet found a smooth user interface for this process).   In order to not have to build a natural language parser, I modified Lewis Carroll’s sentences somewhat in order to be machine-readable.  Here is a typical screenshot:

Unfortunately, the gameplay is somewhat clunkier than in the algebra game, basically because one needs three or four clicks and a keyboard press in order to make a move, whereas in the algebra game each click corresponded to one move. This is in part due to Scratch not having an easy way to have drag-and-drop or right-click commands, but even with a fully featured GUI, I am unsure how to make an interface that would make the process of performing a deduction easy; one may need a “smart” interface that is able to guess some possible intended moves from a minimal amount of input from the user, and then suggest these choices (somewhat similarly to the “auto-complete” feature in a search box).   This would require more effort than I could expend on a plane trip, though (as well as the use of a more powerful language than Scratch).

There are of course several existing proof assistants one could try to use as a model (Coq, Isabelle, etc.), but my impression is that the syntax for such assistants would only be easily mastered by someone who already is quite experienced with computer languages as well as proof writing, which would defeat the purpose of the games I have in mind.  But perhaps it is possible to create a proof assistant for a very restricted logic (such as one without disjunction) that can be easily used by non-experts…