On Semantic Gamification

Abstract

The purpose of this essay is to study the extent in which the semantics for different logical systems can be represented game theoretically. I will begin by considering different definitions of what it means to gamify a semantics, and show completeness and limitative results. In particular, I will argue that under a proper definition of gamification, all finitely algebraizable logics can be gamified, as well as some infinitely algebraizable ones (like Łukasiewicz) and some non-algebraizable (like intuitionistic and van Fraassen supervaluation logic).

A Appendix: Proofs

Success for Strong Kleene. The proof of this proposition is by induction, and it is analogous to the traditional proof of Proposition 1. The atomic case is trivial and guaranteed by the definition of $\mathcal{V}$ in labeled and unlabeled terminal nodes [i.e. literals]. For complex expressions, assuming by Induction Hypothesis that Proposition 2 holds for all the subformulas, we need to ensure that: (a) $\mathcal{V}(G_{\lnot \phi })=\lnot ^\mathbf{{K_3}}\mathcal{V}(G_{\phi })$; (b) $\mathcal{V}(G_{\phi \vee \psi })=\mathcal{V}(G_{\phi })\vee ^\mathbf{{K_3}}\mathcal{V}(G_{\psi })$; and (c) $\mathcal{V}(G_{\phi \wedge \psi })=\mathcal{V}(G_{\phi })\wedge ^\mathbf{{K_3}}\mathcal{V}(G_{\psi })$.

In the case of binary connectives we get the identity easily, since the Nash Equilibria are obtained by the Backward Induction procedure and the player’s payoffs are such that Verifier prefers maximizing between $\mathcal{V}(G_{\phi })$ and $\mathcal{V}(G_{\psi })$, and Falsifier prefers minimizing between those two alternatives. The case for negation requires an observation:

Observation 1

(Mirroring of Pure Strategies and NE). If $s_V$ is a pure strategy for Verifier in $G_{\phi }$, then $s_V$ is a pure strategy for Falsifier in $G_{\lnot \phi }$ [and vice versa]. Furthermore, given some payoff assignment $\mathcal{V}$ to the terminal nodes, if $<s_V,s_F>$ is a Nash Equilibrium in $G_{\phi }$, then $<s_F,s_V>$ is a Nash Equilibrium in $G_{\lnot \phi }$.

A short proof of the observation is the following. Any pure strategy profile $<s_V,s_F>$ in $G_{\phi }$ is associated with a terminal node, the one that is reached by the path indicated by the strategies, with some payoffs $(x,1-x)$ for Verifier and Falsifier respectively. Also, $<s_F,s_V>$ in $G_{\lnot \phi }$ leads to the same node, but now with payoffs $(1-x,x)$. Notice that in $G_{\lnot \phi }$ there was a turn switch; so $<s_F,s_V>$ is the profile where Verifier plays $s_F$ and Falsifier plays $s_V$. If the second profile $<s_F,s_V>$ in game $G_{\lnot \phi }$ is not a Nash Equilibrium, then at least one player, say Falsifier, can change the strategy to $s_V'$ so that $<s_F,s_V'>$ terminates in a node with payoff $y>x$ for him [leaving $s_F$ fixed]. But then Verifier can change her strategy in $G_{\phi }$ to also obtain a better payoff. Obviously, the argument is symmetric, and hence one profile is a Nash Equilibrium if and only if the other is.

With this observation, we get that $\mathcal{V}(G_{\lnot \phi })=1-\mathcal{V}(G_{\phi })$, which is what we needed.    $\square$

Success for Post. It is easy to see that Post’s negation does not satisfy De Morgan’s properties in general. Yet, a weaker (partial) form of De Morgan’s is satisfied:

Observation 2

(Partial De Morgan’s for Post’s Logic).

• $h(\sim (\phi \vee \psi ))=\left\{ \begin{array}{l l} h(\sim \phi \wedge \sim \psi ) &{} \quad \text { if } h(\phi )=0\ne h(\psi ) \text { or } h(\phi )=0\ne h(\psi ) \\ h(\sim \phi \vee \sim \psi ) &{} \quad \text { if otherwise} \end{array} \right.$

• $h(\sim (\phi \wedge \psi ))=\left\{ \begin{array}{l l} h(\sim \phi \vee \sim \psi ) &{} \quad \text { if } h(\phi )=0\ne h(\psi ) \text { or } h(\phi )=0\ne h(\psi )\\ h(\sim \phi \wedge \sim \psi ) &{} \quad \text { if otherwise} \end{array} \right.$

For simplicity, I avoid this proof here.

Providing a game semantics for Post requires a slight change in methodology. In all the cases presented here, the function $\mathbf{game}:\mathcal {L_{\sim }}\rightarrow \mathcal{A}$ was defined independently of the evaluation function $\mathcal{V}$ for the games. In this way we had game forms. For disjunctions and conjunctions, nothing different is needed. Yet, in order to provide a game that corresponds to a formula that involves Post’s negation, it is necessary to look at the truth values of the components. Notice then that for formulas $\phi$ not involving Post negation, we can rely in the success lemmas already shown, so that $h(\phi )=\mathcal{V}\circ \mathbf{game}(\phi )$. Hence in when defining game we can use this fact. Se we only need to show that the success holds for formulas that involve the negation. $\mathbf{game}(\sim \phi )$ is $\mathbf{game}(\phi )$ transformed inductively in the following way:

For terminal nodes, we need to generalize the $\overline{x}$ function that we had before because now ’bars’ are cummulative. So we have a function in the exponent that tracks the amount of times terminal nodes were negated. Non negated terminal nodes $<p_i>$ are now replaced by $<p_i^0>$. Give $\mathbf{game}(\phi )$, we start by replacing each terminal node $<p_i^k>$ with $<p_i^{k+1}>$. As expected, we stipulate that $\mathcal{V}(G_{p_i^k})=[h(p_i)-k](mod\;n+1)=h(\sim ...\sim (p_i))$ where the negation is iterated k times. If $<\psi>$ is a non-terminal node and has children $<\alpha>$ and $<\beta>$, and if $h(\alpha )=n\ne h(\beta )$ or $h(\beta )=n\ne h(\alpha )$:

$turn(<\psi>)=\left\{ \begin{array}{l l} \mathbf{V} &{} \quad \text { if } turn(<\psi>)=\mathbf{F}\\ \mathbf{F} &{} \quad \text { if } turn(<\psi >)=\mathbf{V}\\ \end{array} \right.$

Otherwise, turns are not changed.

The only thing that is really needed now is to show the case for Post-negated formulas, i.e. that $\mathcal{V}(\mathbf{game}(\sim \phi ))=[\mathcal{V}(\mathbf{game}(\phi ))-1](mod\;n+1)$. In order to do this we need an observation. Notice that the tree corresponding to $\mathbf{game}(\sim \phi )$ and the tree coresponding to $\mathbf{game}(\phi )$ are the same, but the games are different in that turn assignments to non-terminal nodes and exponential markings in terminal nodes might have changed.

Observation 3

Given trees $\mathbf{game}(\sim \phi )$ and $\mathbf{game}(\phi )$, for any node $<\psi >_{\lnot \phi }$ in the former corresponding to a node $<\psi >_{\phi }$ in the latter we have that $\mathcal{V}\circ \mathbf{game}(\psi _{\lnot \phi })=[\mathcal{V}\circ \mathbf{game}(\psi _{\phi })-1](mod\;n+1)$.

The proof is by (Backwards) Induction. If $<p_i^k>$ is terminal, then the observation follows by definition. Say $<\psi>$ is a non-terminal node and has children $<\alpha>$ and $<\beta>$ such that $\mathcal{V}\circ \mathbf{game}(\alpha _{\lnot \phi })=[\mathcal{V}\circ \mathbf{game}(\alpha _{\phi })-1](mod\;n+1)$ and $\mathcal{V}\circ \mathbf{game}(\beta _{\lnot \phi })=[\mathcal{V}\circ \mathbf{game}(\beta _{\phi })-1](mod\;n+1)$.

Case 1: $\mathcal{V}\circ \mathbf{game}(\alpha _{\lnot \phi })=n\ne \mathcal{V}\circ \mathbf{game}(\beta _{\lnot \phi })$ or $\mathcal{V}\circ \mathbf{game}(\beta _{\lnot \phi })=n\ne \mathcal{V}\circ \mathbf{game}(\alpha _{\lnot \phi })$. Suppose the former, the latter case is symmetrical. By inductive hypothesis, $\mathcal{V}\circ \mathbf{game}(\alpha _{\phi })=0\ne \mathcal{V}\circ \mathbf{game}(\beta _{\phi })$. If $turn(<\alpha >_{\phi })=\mathbf{V}$, $\mathcal{V}\circ \mathbf{game}(\psi _{\phi })=max\{\mathcal{V}\circ \mathbf{game}(\alpha _{\phi }),\mathcal{V}\circ \mathbf{game}(\beta _{\phi })\}=\mathcal{V}\circ \mathbf{game}(\beta _{\phi })$. Also, by definition, $turn(<\alpha >_{\lnot \phi })=\mathbf{F}$, and then $\mathcal{V}\circ \mathbf{game}(\psi _{\lnot \phi })=min\{\mathcal{V}\circ \mathbf{game}(\alpha _{\lnot \phi }),\mathcal{V}\circ \mathbf{game}(\beta _{\lnot \phi })\}=min\{n,\mathcal{V}\circ \mathbf{game}(\beta _{\phi })-1(mod\;n+1)\}=\mathcal{V}\circ \mathbf{game}(\beta _{\phi })-1(mod\;n+1)$. So $\mathcal{V}\circ \mathbf{game}(\psi _{\lnot \phi })=[\mathcal{V}\circ \mathbf{game}(\psi _{\phi })-1](mod\;n+1)$. If $turn(<\alpha >_{\phi })=\mathbf{F}$, $\mathcal{V}\circ \mathbf{game}(\psi _{\phi })=min\{\mathcal{V}\circ \mathbf{game}(\alpha _{\phi }),\mathcal{V}\circ \mathbf{game}(\beta _{\phi })\}=0=\mathcal{V}\circ \mathbf{game}(\alpha _{\phi })$. Also, by definition, $turn(<\alpha >_{\lnot \phi })=\mathbf{V}$, and then $\mathcal{V}\circ \mathbf{game}(\psi _{\lnot \phi })=max\{\mathcal{V}\circ \mathbf{game}(\alpha _{\lnot \phi }),\mathcal{V}\circ \mathbf{game}(\beta _{\lnot \phi })\}=max\{n,\mathcal{V}\circ \mathbf{game}(\beta _{\lnot \phi })\}=n=\mathcal{V}\circ \mathbf{game}(\alpha _{\lnot \phi })=[\mathcal{V}\circ \mathbf{game}(\alpha _{\phi })-1](mod\;n+1)$.

Case 2: Otherwise. Either (i) $\mathcal{V}\circ \mathbf{game}(\alpha _{\lnot \phi })=\mathcal{V}\circ \mathbf{game}(\beta _{\lnot \phi })=n$ or (ii) $\mathcal{V}\circ \mathbf{game}(\alpha _{\lnot \phi })\ne n\ne \mathcal{V}\circ \mathbf{game}(\beta _{\lnot \phi })$. This proof is left to the reader for its simplicity.    $\square$

Success for Supervaluationism. The main consideration here is to translate each formula and assignment pair $(\phi ,h)$ to a set of classical games. This is done in two steps. First, map each formula $\phi$ to its game form without any specified payoffs, using the original translation method. Second, consider in order the propositional letters $p_i$ that appears in the game form and the value that h assigns to $p_i$. If $h(p_i)\in \{0,1\}$, then assign the corresponding payoff to $p_i$ and move to the next. If $h(p_i)=\frac{1}{2}$, then split the game into two games, one in which the payoff of $p_i$ is (1,0) and another in which it is (0,1). Continue the procedure with all the games that were generated in the steps before.

It should be clear to the reader that the set of games obtained are the games corresponding to all of the classical extensions of h. Then the proposition follows by mere definition.    $\square$

Success for Intuitionism. Begin with a Kripke structure $\mathbf {K}$ of partially ordered nodes $\{k_i\}_{i\in I}$. Recall that this proof is just for the propositional case; nothing conceptually different is added for the first order case.

There is an atomic forcing relation defined for all nodes k such that for all propositional letters $p_i$, either k forces $p_i$ [i.e. k makes $p_i$ true, or the forcing relation is not defined for that node and propositional letter. This atomic forcing relation is subject to the constrain that if $k\leqslant k'$ and k forces $p_i$, then $k'$ forces $p_i$. The extensio of the forcing relation to all formulas is the following: (a) A node k forces $\phi \wedge \psi$ if it forces $\phi$ and $\psi$; (b) A node k hforces $\phi \vee \psi$ if it forces $\phi$ or $\psi$; (c) A node k forces $\phi \rightarrow \psi$ if, for every $k'\geqslant k$, if $k'$ forces $\phi$ then $k'$ forces $\psi$; and (d) A node k forces $\lnot \phi$ if, for $\mathbf {no}$ $k'\geqslant k$ does $k'$ forces $\phi$.

Given a formula and a node k in a Kripke structure $\mathbf {K}$, the translation functions are the following: (a) The game corresponding to $(p_i,k)$ is a one node game with payoffs (1, 0) if k forces $p_i$ and (0, 1) otherwise; (b) The game corresponding to $(\phi \wedge \psi ,k)$, $G_{(\phi \wedge \psi ,k)}$, consists of a root node for Falsifier with two subgames,$G_{(\phi ,k)}$ and $G_{(\psi ,k)}$; (c) The one corresponding to disjunction is as expected; (d) The game corresponding to $(\phi \rightarrow \psi , k)$, $G_{(\phi \rightarrow \psi , k)}$, has a root node that is a move for Falsifier whose children are the games $G_{(\sim \phi \vee \psi ,k')}$, for all $k'\geqslant k$; and (e) The game corresponding to $(\lnot \phi , k)$, $G_{(\lnot \phi , k)}$ has a root node that is a move for Falsifier whose children are the games $\overline{G_{(\phi ,k')}}$, for all $k'\geqslant k$. Here $\overline{G_{(\phi ,k')}}$ is just like $G_{(\phi ,k')}$ but with roles and payoffs switched [just like in the classical negation clause].

To show the result is sufficies to show that for any pair $(\phi ,k)$, k forces $\phi$ if and only if Verifier has a winning strategy in $G_{(\phi ,k)}$. The atomic case is trivial. So are the cases for conjunction, disjunction and classical negation. This is just the same proof as for classical logic. The case for the conditional is slightly more complicated. It is worth noticing is that here $\sim$ refers to classical negation, and hence $\sim \phi \vee \psi$ is just code for the material conditional. We begin with $(\phi \rightarrow \psi , k)$, and suppose k forces $\phi \rightarrow \psi$. Then, in a nutshell, for every $k'\geqslant k$, $k'$ forces $\sim \phi \vee \psi$. But then, by inductive hypothesis, Verifier has a winning strategy in every such $G_{(\sim \phi \vee \psi ,k')}$. So it has a winning strategy in $G_{(\phi \rightarrow \psi , k)}$. Suppose Verifier has a winning strategy in $G_{(\phi \rightarrow \psi , k)}$. Then whichever choice Falsifier makes at the root node, Verifier still has a winning strategy. That means that for all $k'\geqslant k$, Verifier has a winning strategy in $G_{(\sim \phi \vee \psi ,k')}$. By inductive hypothesis this just means that for every $k'\geqslant k$, if $k'$ forces $\phi$ then $k'$ forces $\psi$. Consider $(\lnot \phi , k)$. Suppose k forces $\lnot \phi$. Then there is $\mathbf {no}$ $k'\geqslant k$ such that $k'$ forces $\phi$. The game $G_{(\lnot \phi , k)}$ has a root node that is a move for Falsifier whose children are the games $\overline{G_{(\phi ,k')}}$, for all $k'\geqslant k$. Now, by (a minor extension of) Observation 2 - Mirroring of pure strategies and Nash Equilibria -, we know that for all such $k'$ Falsifier has a winning strategy in $\overline{G_{(\phi ,k')}}$ if and only if Verifier has a winning strategy in $G_{(\phi ,k')}$, and viceversa. We also know, by inductive hypothesis, that Verifier has a winning strategy in $G_{(\phi ,k')}$ if and only if $k'$ forces $\phi$. Since k forces $\lnot \phi$, there is no $k'\geqslant k$ such that Verifier has a winning strategy in $G_{(\phi ,k')}$. But all of the $G_{(\phi ,k')}$ are two-player perfect information games, and therefore are determined. Ergo, Falsifier has a winning strategy in all those $G_{(\phi ,k')}$. By Observation 2, Verifier has a winning strategy in all the $\overline{G_{(\phi ,k')}}$. Hence, whichever move Falsifier makes in the root node of $G_{(\lnot \phi , k)}$, it leads to a game won by Verifier. To conclude, Verifier has a winning strategy for $G_{(\lnot \phi , k)}$. Now for the converse. Suppose Verifier has a winning strategy for $G_{(\lnot \phi , k)}$. This just means that whatever $\overline{G_{(\phi ,k')}}$ Falsifier chooses at the root node, Verifier has a winning strategy there. Therefore, again by Observation 2, Falsifier has a winning strategy in all the $G_{(\phi ,k')}$ with $k'\geqslant k$. By inductive hypothesis, this just means that there is no $k'\geqslant k$ such that $k'$ forces $\phi$.    $\square$