A Game Theoretical Semantics for Logics of Nonsense

Logics of nonsense allow a third truth value to express propositions that are nonsense. The initial motivation behind introducing nonsensical propositions was to capture the logical behavior of semantic paradoxes that were thought to be nonsensical.

As argued by Ferguson, nonsense is “infectious” [9]: “Meaninglessness […] propagates through the language; that a subformula is meaningless entails that any complex formula in which it finds itself is likewise meaningless.” Logics of nonsense, for this reason, are intriguing.

Nonsense appears in various contexts. In mathematics, the expression “$1/x$” is considered meaningless when $x=0$. Certain approaches to truth disregard paradoxes of self-reference and exclude them as meaningless. In philosophy of science, some theories are thought to be “monsters” and are thereby excluded from research programs [15]. In computer science, software bugs often remain throughout the program run and produce an unexpected output. In all these discussions, nonsense propagates throughout the system and “infects” the other truth values.

In what follows we will employ game theoretical tools and techniques to give a broader reading of the aforementioned infectiousness. What motivates our approach is manifold. First, game theoretical semantic tools offer a very intuitive and natural approach to semantics. Moreover, they suggest computational connections between truth, proofs, programs and strategies, relating major concepts of game theory, computer science and logic to each other constructively. In this way, certain connections between how errors are handled in programs and how they propagate throughout the programs once they appear can be established. Studying logics of nonsense helps developing a substantial analysis of such situations. Second, game semantics is perhaps the most studied non-compositional semantics. It is non-compositional in the way that the truth of a complex formula is evaluated based on the truth values of some of its components. We can thus answer how “some” truth values can infect the others and computationally determine the truth value of the formula in question. Such “infections” suggest that there is a certain strategic interaction amongst the players. Third, a study of “infectiousness” helps us draw a broader picture of interactive and rational behaviour, which is a central theme in multi-agent systems, social choice and decision theories. In conclusion, a game theoretical semantic study of logics of nonsense helps us understand “infectiousness” from a variety of different but complementary perspectives.

In game semantics, the truth of a formula in a model is evaluated by playing a game. Given a model and a well-formed formula, players try to win a game in order to decide the truth value of the formula in the given model. In classical propositional logic, the semantic verification game (or “semantic game” for short) is played by two players, the verifier and the falsifier, who are often called Heloise and Abelard respectively. The verifier aims at verifying the truth of a given formula in a given model whereas the falsifier aims at falsifying it. The game is for two-players, reflecting the binary truth values of the logic.

In a semantic game, the given formula is broken into subformulas step by step. The game terminates when it reaches the propositional atoms. If the game ends with a true atom, then the verifier wins the game. Otherwise, it is a win for the falsifier. The moves and turns of the game are determined syntactically based on the shape of the formula. If the main connective is a conjunction, the falsifier makes a move. If it is disjunction, the verifier makes a move. If the main connective is a negation, the players switch roles: the verifier becomes the falsifier, the falsifier becomes the verifier. Throughout the game, players may switch their roles according to the rules as the rules are given for players’ roles not for the individual players.

We say that a player has a winning strategy if he has a set of rules that guides him throughout the play and tells him which move to make, and consequently gives him a win regardless of how the opponent plays. In classical game semantics, winning strategies necessarily determine the truth values of the formulas. In non-classical game semantics, this assumption is rejected. Because some games may have multiple winners – with multiple “winning” strategies. In that case, we need to be able to identify the winning strategy that necessarily determines the truth value of the formula in question. We call such winning strategies dominant. We will use dominant strategies to capture the infectiousness of nonsense.

Logics of nonsense and game semantics both have a long, but relatively unconnected, history.

Game semantics has been a popular research area since Jaakko Hintikka, and Helsinki School researchers produced a significant amount of work on the subject. Broad historical surveys of the subject were presented in [20, 14] with many references. Game semantics have been used to understand proofs and computation in computer science [2], and dialogical games in philosophical logic [16, 22].

The connection between non-classical logic and game semantics have not been studied so extensively. Game semantics for various many-valued logics have been presented in [11, 10]. In the context of dialogical logic, which can be seen as a variant of game semantics, the connection between semantic games and paraconsistency was explored in [21]. A recent work focused on the connection between various well-known paraconsistent logics and game semantics and offered various modifications for the games based on different logics [4, 5]. The current work attempts at following the same path yet puts more emphasis on strategies.

Logics of nonsense were first suggested by Bochvar in the 1930s and by Halldén in the 1940s [6, 13]¹¹1The translation of [6] appeared as [7].. These logics enjoy different validities as Halldén’s system preserves nonsense (along with true) under valid inferences. Bochvar’s system, however, does not. As such, Halldén’s logic is paraconsistent; Bochvar’s, dually, is paracomplete. Such systems were extended by Åqvist and Segerberg [3, 23]. Hałkowska suggested an algebra for logics of nonsense [12]. In that work, nonsense truth value was motivated by certain meaningless mathematical expressions such as $1/x$ where $x=0$.

There has been an increasing interest towards infectious logics. Ferguson examined the logics of nonsense in relation to various other non-classical containment logics, offering a broad perspective [9]. Szmuc discussed logics of nonsense within the context of some other non-classical logics, including logics of formal inconsistency and of formal underminedness. As such, he carried the issue into broader classes of logics and generated a variety of logics of nonsense [24]. Following this methodology, Ciuni et al constructed a linear order of infectious logics, extending logics of non-sense into a countably infinite family of subsystems of classical logic [8]. What they achieved in their work uses logical and semantical methods, while we arrive at similar systems using game theoretical tools in this work. Omori presented an extension of logics of nonsense by discussing them within the framework of logics of formal inconsistency [17]. Omori and Szmuc focused on the behavior of conjunction and disjunction in logics of nonsense and observe the unexpected working of disjunction [18].

The current paper is organized as follows. First, we formally define semantic games. Then, after a brief discussion of a logic of nonsense, we introduce a game semantics for it. Consequently, we prove the correctness theorem of our game semantics. We then extend our semantic games for an attempt to obtain some other logics of nonsense that extend the initial system. Finally, as a case study, we take advantage of our approach in order to obtain a more refined semantic game for a well-known paraconsistent logic, Priest’s Logic of Paradox.

The main contribution of the paper is to emphasize the role of dominant strategies in game semantics in the context of non-classical logics. By doing so, we establish a stronger connection between non-classical logics and game theory. We achieve this by showing how dominant strategies and certain truth values in game semantics work similarly.

This paper is part of a research programme on non-classical game theory. Similar to non-classical approaches to truth (and proof), it is possible to analyze strategies and wins from a non-classical perspective. This will provide a more nuanced understanding of game theory and open up a new avenue for applications for non-classical logic(s).

Throughout this work, we will use “game theoretical semantics” and “game semantics” interchangeably, assuming no confusion arises.

Non-classical logics and their game semantics allow us to study the connection between non-classical logical elements and their corresponding game theoretical properties. How does a paraconsistent game look like? Can we have a multi-player semantic game for a multi-valued logic? Whilst answering these questions, one can engineer non-classical logics using game theoretical tools as well as develop semantic games for non-classical logics. Those games can be multi-player, non-zero-sum, cooperative, non-determined and non-sequential, differing from the semantic games for classical logic.

In what follows, we focus on systems of propositional logic which allow us to reason about strategies in semantic games. This will exemplify the fact that strategies in classical semantic games are over-simplified (or degenerate) forms of strategies that appear more clearly in semantic games for some non-classical logics, such as logics of nonsense. Before presenting our results, we need to set up our system.

We define semantic games following the terminology given in [20, 4]. First, we consider the language $\mathcal{L}$ of propositional logic given as follows in the Backus–Naur form for a set of countable propositional variables $\mathbf{P}$:

where $p\in\mathbf{P}$. We define the conditional arrow as expected: $\varphi\rightarrow\psi\equiv\neg\varphi\vee\psi$.

A model for semantic games is defined as follows.

In semantic games, we have a set of players, game rules and a set of positions. Some non-classical logics, such as Priest’s LP and Strong Kleene Logic, share the same truth tables but they differ on their set of designated truth values – rendering the former paraconsistent, the latter paracomplete. In order to distinguish such systems, designated truth values²²2The set of designated truth values are used to define theorems in a particular logic. They can be viewed as non-classical extensions of the truth value True, and are preserved under valid inferences. The relation between the proof theory and semantic games is well-pronounced for certain logics, which falls outside the scope of this paper [2]. Similarly, game theoretical readings of logical consequence relation remains a curious problem. We are thankful to the anonymous referee for pointing this out. are specified – even though we will not focus on them in this work. Some games may not be sequential, thus a game-token may be used to indicate the current position of the players.

Let us start by explaining how $\Gamma$ is constructed. Players in the semantic game $\Gamma$ have interchangeable roles. A player $p_{\_}i\in\pi$ may assume different roles, thus strategies, in the game. Therefore, the game rules will be given not for the players $p_{\_}i$ but for their roles. Players, then, will follow the rules based on what roles they assume. The falsifier aims at reaching a false atom, the verifier a true atom.

The positions $\sigma$ in the game are determined by the subformulas of the given formula and the players. As such, they also include the turn function, which specifies which players are allowed to make a move at each position. Consequently, the set of positions will be composed of tuples as $(p_{\_}i,\varphi)$ for $p_{\_}i\in\pi$ and a well defined formula $\varphi$. The tuple $(p_{\_}i,\varphi)$ will read “it is player $p_{\_}i$’s turn at $\varphi$”. The set $\sigma_{\_}{p_{\_}i}$ will denote the set of positions for player $p_{\_}i\in\pi$, and will be defined as $\sigma_{\_}{p_{\_}i}=\{(p_{\_}i,\varphi):(p_{\_}i,\varphi)\in\sigma\text{ for a fixed player }p_{\_}i\}$. For simplicity, we will include the empty set in $\sigma$.

The set $\sigma$ is not sufficient by itself to describe which positions are concurrent and played simultaneously. In semantic games for classical logic, $\tau$ is the set of singletons as there is no concurrent or parallel play. In games, where two players are allowed to make moves at the same time, we will have $\{(p_{\_}1,\varphi),(p_{\_}2,\psi)\}\in\tau$, which reads “player $p_{\_}1$ plays at $\varphi$ and player $p_{\_}2$ plays at $\psi$ simultaneously”.

Designated truth values $\delta$ determine the theorems in a logic. In order to distinguish different logics, we specify $\delta$. Yet, we will not focus on proof theory in this work.

The rules $\rho$ of semantic games are defined inductively as (partial) transformations from a game position $(p_{\_}i,\varphi)$ to a set of game positions $\{(p_{\_}j,\psi)\}_{\_}{j\in I}$ for $p_{\_}i,p_{\_}j\in\pi$, $I\subseteq\pi$, well-defined formula $\varphi$ and a subformula $\psi$ of $\varphi$, defined in the standard way. As such, game rules do not change if a position is a concurrent or not since they are defined per position. For simplicity reasons, we do not include a turn function to determine which players are supposed to make a move at any position. Game rules and positions specify the turn. If player $p_{\_}i$ is not supposed to make a move at position $(p_{\_}i,\varphi)$ then, the game rule $\rho_{\_}j$ will return $\rho_{\_}j((p_{\_}i,\varphi))=\emptyset$ where $\emptyset\in\sigma$.

A run (or play) is a sequence of sets from $\tau$ which starts with $\{\{p_{\_}i,\varphi\}\}$ and ends with a set that contains a position with an atom, where $\varphi$ is the initially given formula. In semantic games for classical propositional logic, for example, a run is a sequence of singletons from $\tau$.

The semantic game $\Gamma$ for a model $M$ and a well-defined formula $\varphi\in\mathcal{L}$ is denoted by $\Gamma(M,\varphi)$.

In semantic games, logical behavior is described using game theoretical tools and concepts. Strategies are perhaps the most important of such tools. In semantic games for classical logic, having winning strategies necessarily determines the truth value of the formula in question, and vice versa. This is a very intuitive and fundamental idea. Yet, it fails to translate into various non-classical logics as having a winning strategy for a semantic game does not necessarily determine the truth value of the formula in question. For that reason, we need a stronger concept.

In other words, in $\Gamma(M,\varphi)$ if a player $p_{\_}i$ admits a dominant winning strategy $\Sigma$ and if $p_{\_}i$ plays $\Sigma$, then $\varphi$ has the truth value that $p_{\_}i$ forces. If $p_{\_}i$ admits a winning strategy, on the other hand, then $\varphi$ may have the truth value that $p_{\_}i$ forces, depending on other players and conditions. However, if $p_{\_}i$ does not admit a winning strategy nor a dominant winning strategy, she cannot determine the truth value of $\varphi$. Naturally, in classical logic, every winning strategy is dominant. In non-classical logics, they are not.

Notice that what Definition 2.3 describes is rather different than what most readers may be familiar in classical game theory about strategy dominance.³³3We are thankful to the anonymous referee for pointing this out. The standard game theoretical definitions discuss pay-offs and higher pay-offs, whereas we focus on determining truth-values [19]. There is, however, a philosophical connection. Higher-payoffs with dominant strategies help a player win a game in competitive games, dominant winning strategies help a player to determine the truth value of a formula in semantic games.

Bochvar–Halldén Logic introduces an additional truth value $N$, called nonsense, which intuitively stands for sentences which are nonsensical or meaningless. As we argued earlier, Bochvar–Halldén logics are actually two distinct logics with the same truth table. In Bochvar’s system, the designated truth value is $T$ whereas in Halldén’s it is $\{T,N\}$. For our semantic considerations, we treat them together and call this formalism the Bochvar–Halldén Logic (BH3, for short) with the following truth table.

In a semantic game for BH3, we need three players to force the three truth values. In addition to the classical players Verifier and Falsifier, we introduce a third player which we call “Dominator”. Dominator forces the game to a nonsense proposition. As such, he is allowed to make moves along other players. We also stipulate that Dominator’s strategy is dominant – his wins determine the truth value.

We denote the semantic game for BH3 by GTS^BH3 and propose the following rules for GTS^BH3.

Let us now briefly explain the game. First, the set of positions $\sigma$ is constructed inductively. Atomic formulas are associated with all players as they all need to check whether they win. At negated formulas, players reshuffle their roles and the game continues with the players based on the next formula’s syntactic form, which is determined inductively. For conjunctions and disjunctions, the next position is determined based on the main connective of conjuncts and disjuncts, respectively. Two players are allowed to make moves at the same time but independently at conjunctions and disjunction, as specified by $\tau$: conjunctions are for Falsifier and Dominator, disjunctions are for Verifier and Dominator. The set of available moves for those players are specified further in the game rules $\rho$.

We stipulate that Dominator’s strategy dominates the others and his role does not change throughout the game, even under negation, which reflects the truth table for BH3 given in Figure 1. The strategies of Verifier and Falsifier, however, do not dominate each other or any other strategy, by default.

The following example illustrates how BH3 semantic games are structured and played.

Let us now start with noting that Dominator is the only dominant player.

Dominant winning strategies and game rules allow us to establish the following correctness theorem for the game semantics for BH3.

It is important to note that in Theorem 3.5, Verifier or Falsifier can only have a dominant strategy if Dominator does not have one.

Using the idea of dominant strategies, we can engineer some semantic games without first considering their possible semantics. This is an interesting methodology which develops logics (and truth tables) which are solely generated by semantic games.

In what follows, we extend the BH3 games to four players, where we call the forth player Dictator. Dominator’s strategy dominates Falsifier’s and Verifier’s, whereas Dictator’s strategy dominates them all. For simplicity, we call the truth value that is forced by Dictator as super and denote it by $S$. Thus, Dictator’s role is to force the semantic game to an end with an atom with the truth value super.

We propose the following rules for the extended game $\Gamma(M,\varphi)$ with respect to players’ roles.

• ($\rho^{\prime}_{\_}p$)

  If $\varphi$ is atomic, the game terminates, and Verifier wins if $\varphi$ is true, Falsifier wins if $\varphi$ is false, Dominator wins if $\varphi$ is nonsense, and Dictator wins if $\varphi$ is super,

• ($\rho^{\prime}_{\_}\neg$)

  if $\varphi=\neg\psi$, Falsifier and Verifier switch roles, Dominator and Dictator keep their roles, and the game continues as $\Gamma(M,\psi)$,

• ($\rho^{\prime}_{\_}\wedge$)

  if $\varphi=\chi\wedge\psi$, Falsifier, Dominator and Dictator choose between $\chi$ and $\psi$ simultaneously,

• ($\rho^{\prime}_{\_}\vee$)

  if $\varphi=\chi\vee\psi$, Verifier, Dominator and Dictator choose between $\chi$ and $\psi$ simultaneously.

• ($\rho^{\prime}_{\_}s$)

  Dominator’s strategy strictly dominates Verifier’s and Falsifier’s, and Dictator’s strategy strictly dominates them all.

These rules give raise to a logic. We call this system BH4. We can then construct a truth table for BH4 that corresponds to the given game rules in Figure 2.⁴⁴4It turns out that this logic has been suggested in [24, 8].

Let us start by making an observation regarding the strategy configuration in the game.

Similar to what we have shown for BH3, we present the correctness theorem for BH4 as follows.

Following our methodology, different combinations of the above game rules can be constructed, yielding different logics with more or different infectious truth values. Furthermore, similar to what is suggested in [8], additional truth values, thus players, beyond the fourth can be introduced in a way that the dominant winning strategies form a linear order: Dominator dominates the classical players; Dictator dominates Dominator; a fifth player, say King, dominates Dictator and the rest etc. This procedure is rather straight-forward for countably many players. The semantic games seem to get more interesting once ${>}\omega$-many players are considered with a linear or branching order of dominant strategies.

In an earlier work, a game theoretical semantics for Graham Priest’s Logic of Paradox (LP, for short) was given [4]. In that work, the semantic games employed concurrent plays. At certain nodes, players engaged in concurrent plays where none were assumed to have dominant winning strategies. Consequently, those game rules produced significantly weaker correctness theorems for the game semantics for LP. It is then a natural question whether a game semantics for LP can be given using dominant strategies and if they entail a stronger correctness theorem. This would complement our overall aim of focusing on strategic dominance in game semantics for non-classical logics, and, at the same time, provide yet another game semantics for LP. This is our goal in this section.

The logic of paradox introduces a third truth value which was intended to represent paradoxical statements. The third truth value $P$ is called paradoxical and requires its own player, which was called Astrolabe [4]. Astrolabe forces the game to an end with the truth value $P$, so he is the paradoxifier. In semantic games for LP, conjunctions are for Falsifier and Paradoxifier and disjunctions are for Verifier and Paradoxifier. At negations, similar to BH3 games, Verifier and Falsifier switch roles, and Paradoxifier keeps his role. We reproduce the truth table for LP in the following.

Notice that the very same game would work for the Strong Kleene System with minimal alterations as Strong Kleene and LP differ only on their designated truth values.

In [4], a game semantics for LP was suggested by allocating Astrolabe as the parallel player. He made moves, just as Dictator in BH3 games, along with Verifier or Falsifier. However, as the strategies and their strength were not properly considered in the aforementioned, the correctness theorems were not as strong.

These two theorems –especially the third bullet point in Theorem 5.2– seem to allude to some hierarchy between the player’s strategies. In the sequel, we remedy this issue by imposing an order of domination over strategies.

We now give the new game rules for GTS^LP games as follows for $\Gamma_{\_}{\mathrm{LP}}(M,\varphi)$ with respect to players’ roles.

• ($\rho^{\mathrm{LP}}_{\_}p$)

  If $\varphi$ is atomic, the game terminates, and Verifier wins if $\varphi$ is true, Falsifier wins if $\varphi$ is false, and Paradoxifier wins if $\varphi$ is paradoxical,

• ($\rho^{\mathrm{LP}}_{\_}\neg$)

  if $\varphi=\neg\psi$, Verifier and Falsifier switch roles, Paradoxifier keeps his role, and the game continues as $\Gamma_{\_}{\mathrm{LP}}(M,\psi)$,

• ($\rho^{\mathrm{LP}}_{\_}\wedge$)

  if $\varphi=\chi\wedge\psi$, Falsifier and Paradoxifier choose between $\chi$ and $\psi$ simultaneously,

• ($\rho^{\mathrm{LP}}_{\_}\vee$)

  if $\varphi=\chi\vee\psi$, Verifier and Paradoxifier choose between $\chi$ and $\psi$ simultaneously,

• ($\rho^{\mathrm{LP}}_{\_}s$)

  Paradoxifier’s strategy is strictly dominated by Verifier’s and Falsifier’s.

Similar to the case of BH3, Verifier and Falsifier will never have conflicting strategies. If either Verifier or Falsifier may have some conflicting strategy, it can only be with Paradoxifier where the pardoxifier’s strategy is strictly dominated by them.

It is important to notice that the difference in the truth tables for BH3 and LP (given in Figures 1 and 3), can be accounted by the difference between the strategic dominance of players, as specified by game rules ($\rho_{\_}s$) and ($\rho^{\mathrm{LP}}_{\_}s$). Therefore, the only (game theoretical) difference between BH3 games and the LP games are whether the third player is the strictly dominant or the strictly dominated player. The following theorems summarizes our findings.

Compared to Theorem 5.2, Theorem 5.4 makes it precise what game theoretically corresponds to the condition that “only paradoxifier has a winning strategy”. We replaced this condition by dominated strategies. As such, the above result complements what has been presented in [4]. It furthermore suggests that certain combinations of strategy dominance amongst the players may result in various interesting logical ideas. For example, in our work strategies strictly dominate some others. What is then the logic of those semantic games where strategies weakly dominate? In the context of semantic games, weak strategy domination is an interesting issue.⁵⁵5We are thankful to the anonymous referee for pointing this out. It may mean that the correctness theorems work only on one direction, failing to provide a bidirectional stronger result. We refer the interested reader to [4].

Similar to the questions we raised for BH3/BH4, can we extend LP game theoretically to a four-valued paraconsistent system? Such questions point out to various future work possibilities.

In this paper, we showed how non-classical game theory helps us understand the nuances of non-classical logics as well as certain game theoretical concepts.

To the best of our knowledge, this is the first game theoretical semantics suggested for Bochvar–Halldén logics and infectious logics in general, relating infectiousness to strategy dominance. This proves that studying various combinations of dominant and dominated strategies is a fruitful direction to develop various new logics and study their model theory. A linear order of strategy dominance relates directly to certain solution concepts in game theory. Then the next question is to study a branching order of strategy dominance and how they relate to truth-coalitions in game semantics.

Conversely, it is possible to inquire the opposite direction and develop logical methods for some other solution concepts and equilibria computation in game theory. Computing game theoretical equilibria is an important research direction in computer science. Incorporating logical elements to this methodology will certainly have immediate impact in aforementioned fields.