One of our undergrad students recently finished his B.Sc. thesis on a serious game intended to teach the player to apply maths to real-world problems (this is probably going to be worth its own blog post, once the paper is publicly available somewhere), which got me thinking about other ways to teach math using video games. It occurred to me, that magic systems in RPGs might be one way to do this.

Components of magic systems in video games may contain any of the following:

- Magic spells need to be learned,
- they might take magic ingredients to be cast,
- they might require a specific sequence of actions to be performed during/when casting spells (gestures, magic words etc.),
- more powerful spells require more powerful ingredients that are harder to come by.

So I got the idea, that it might be possible to use formal logic to come up with a new magic system for RPGs – the idea being (and these are only very superficial thoughts):

*Magic ingredients*might correspond to*symbols*of a formal syntax,*spells*might correspond to*propositions*of the logic,*gestures / magic words*needed to cast / activate a spell might correspond to*inference rules*– a spell is*activated*by performing the right sequence of gestures / magic words, which corresponds to*proving the associated proposition*.

If one manages to spin these analogies further – i.e. give **a full RPG magic semantics to the syntax and proof theory** of some logical system – this might be a way to coerce and teach the player to actually **think mathematically without them even noticing** that’s what they’re doing. In an unrealistically ideal world, one could even imagine that giving rise to new interesting theorems and proofs (think of things like Foldit, Quantum Moves and similar crowdsourcing research games).

Progress in the game might be coupled with guiding the player to learn new spells/theorems needed to finish storyline quests. Once a spell/theorem has been activated/proven, they would only need the required ingredients/symbols to cast it again (you don’t want to force people to prove the same thing over and over again).

The most difficult part would be (I imagine), to assign *actual effects* to the spells (i.e. theorems) in such a way, that there’s incentive to continually come up with *new* proofs/spells and such that more advanced proofs correspond to more powerful spells. Ideally, the more *interesting* or *meaningful* a proposition in the logical system is, the more useful the corresponding spell should be – but you don’t want to only do that for predefined propositions – ideally, you want the player to be able to come up with their own as well. There certainly isn’t an* ideal* solution to that problem (it seems like an AI complete problem to me), but there might be a partial solution that’s *“good enough”*. For example, different metrics (length of a proposition in some normal form, number of logical connectives, quantifier switches in prenex form etc.) could conceivably correspond to strengths of different effects (fire/cold damage, healing, shield, stun enemy…)

So, I’ve started an Authorea document here to collect thoughts, ideas etc. Do you have something to contribute? Are there already projects in that direction? Do you have ideas? Please share any thoughts and ideas directly there. Maybe we can actually manage to come up with a useful system 🙂