A long time ago (but I can't remember when), I was introduced to the (pedagogical) concept of writing a proof as giving a winning strategy for a game. Basically, given a statement $\forall x\exists y \forall z\exists w P(x,y,z,w)$ (or similar), there is a corresponding game, where one player is $\forall$ (sometimes pronounced $\forall$belard or $\forall$dversary), the other player is $\exists$ (sometimes pronounced $\exists$loise, which is apparently hilarious if you know French).
Anyway, the objective of $\forall$ is to make $P$ false; the objective of $\exists$ is to make $P$ true. They take turns playing (turn order defined by quantifier order) and the statement is true if and only if $\exists$ has a winning strategy.
Of course you'd have to prove this makes sense, but the above can be made a theorem and proven. However, I'm teaching a course on proof, and can't for the life of me find a citation for any of this for my students to read. Not the applications of this into model theory, etc., but just the explanation of this as a metaphor.
Is this familiar to anyone? And can you remember where you saw it before? I'm trying to find something tangible I can give to my students.
Wikipedia has an article about this although it isn't very good, but it does have many other references you could consult.
The idea is crucial to understanding why the strategies of so many games are PSPACE-complete. This is because the central PSPACE-complete problem, analogous to SAT for NP-complete problems, is the satisfiability problem for quantified boolean formulas, and asserting that $P_1$ wins some game can be understood as claiming that there exists a $P_1$ move such that for all $P_2$ moves there exists a $P_1$ move… etc.