From semantic games to provability: the case of Gödel logic (Q2118973)

The game-theoretic interpretation of logics is well known, when a formula is true if and only if in the game between the \textit{proponent} P (who defends it) and the \textit{opponent} O (who opposes it) P has a winning strategy. For example, if we know the truth values of the Boolean variables \(v_i\) used in a propositional formula \(F\), then we can set up a natural game to decide whether \(F\) is true for these values. For example, when the formula has the form \(A\,\&\,B\), the opponent selects either \(A\) or \(B\) and asks P to prove the selected subformula; when the formula is \(A\vee B\), the proponent selects \(A\) or \(B\) and asks O to disprove the selected subformula. These steps eventually lead to atomic formulas, and the game ends. This paper considers a similar idea for the so-called \textit{Gödel fuzzy logic}, in which, to every variable \(v_i\), a truth value \(t(v_i)\) from the interval \([0,1]\) is assigned, and this assignment is extended to more complex formulas as follows: \(t(A\,\&\,B)=\min(t(A),t(B))\), \(t(A\vee B)=\max(t(A),t(B))\), \(t(A\to B)=1\) if \(t(A)\le t(B)\) and \(t(B)\) otherwise, and \(t(\neg A)=t(A\to 0)\). For this logic, the truth value of each propositional formula \(F\) is equal either to the truth value \(t(v_i)\) of one of its variables \(v_i\), or to 0 or 1 -- and to which one depends only on the order between the values \(t(v_i)\). Thus, once we know all the truth values \(t(v_i)\), we can determine the truth value of a given formula if we know whether statements \(t(F)\le t(v_i)\) hold. Each such statement can be reduced to statements about simpler formulas: e.g., \(t(A\,\&\,B)\le t(v_i)\) if and only if either \(t(A)\le t(v_i)\) or \(t(B)\le t(v_i)\). Thus, the above idea can be naturally applied to form a game semantics for this logic. A somewhat more complex situation is when we are interested in whether a propositional formula \(F\) is valid for all possible values \(t(v_i)\). In this case, on each stage of the game, instead of generating a single formula, P and O generate a finite set of formulas -- i.e., in effect, they simultaneously play several games -- and \(F\) is valid if and only if there is a strategy allowing P to win in all these simultaneous games. Of course, there are infinitely many different combinations of truth values \(t(v_i)\), but since the validity of \(F\) only depends on the order between these truth values (and 0 and 1), it is sufficient to consider finitely many cases corresponding to finitely many possible orders. The paper then extends both games to the case when we supplement Gödel logic with (1) an additional negation \(-A\) for which \(-(-A)=A\) and (2) constants \(c_1,\ldots,c_m\). In this case, the value \(t(F)\) is also limited to a finite set: we just add values \(-t(v_i)\), \(c_j\), and \(-c_j\). Also, validity of \(F\) depends only on the order between the values 0, 1, \(t(v_i)\), \(-t(v_i)\), \(c_j\), and \(-c_j\). So, such game extension is possible.