Is there a three valued logic whose game semantics corresponds to potentially infinite games?

Question

Consider game trees with the following properties:

• Each node in the tree is one of the following:
  • Verifier Choice: Has one or more children
  • Falsifier Choice: Has one or more children
  • No Choice: Has exactly one child, which is always selected (could be represented by a Verifier or Falsifier Choice, but is considered a separate type of node for clarity)
  • Verifier Victory: Is a leaf
  • Falsifier Victory: Is a leaf
• The branches of the tree may be infinitely long (i.e. the tree is not necessarily well founded)

These game trees represent perfect information two player extensive-form games. A game is said to represent a true statement if Verifier has a winning strategy, a false statement if Falsifier has a winning strategy, or an indeterminate statement if neither has a winning strategy. It is clear that only a non-well founded game tree can represent an indeterminate statement.

Is if there is a logic whose game semantics correspond to the games considered above?

---

If there is such a logic, it would contain Kleene logic. Kleene logic does not have quantifiers, however, so we would need something more complex.

It seems that the denotational semantics of recursive programs is related, if we interpret truth values as potentially undefined Boolean values.

An interesting example of an indeterminate statement would likely be $\{x : x \notin x\} \in \{x : x \notin x\}$ in naive set theory. In classical logic, this would result in Russell's paradox. If there is a logic discussed above, however, it would not. Rather, the statement would consist of an infinite line of no choice nodes, and so would have an indeterminate truth value. The same applies to $\{x : x \in x\} \in \{x : x \in x\}$. The statement "the set of all sets contains the set of all sets" would be true, however, consisting of a single Verifier victory node. More interesting examples crop up when you have sets defined using quantifiers (which will involve Verifier choice and Falsifier choice nodes).

Answer 1

Why doesn't Kleene's 3-valued logic (with quantifiers) correspond to such games? It already does! A $∀x\ ( Q(x) )$ node goes to an $∃x\ ( ¬Q(x) )$ opponent node, and an $∃x\ ( Q(x) )$ node goes to one $Q(c)$ same-player node for each $c$ in the domain.

Russell's paradox can indeed be resolved using 3-valued logic easily. For $R := \{ x : x∉x \}$, we have $R∈R ≡ ¬R∈R ≡ null$ in every model. The game semantics for such a set theory are trivial; an $E ∈ \{ x : Q(x) \}$ node goes to a $Q(E)$ same-player node. But your last claim about "$\{ x : x∈X \}$" makes no sense. Obviously, both the $\{ x : x∉x \} ∈ \{ x : x∉x \}$ node and the $\{ x : x∈x \} ∈ \{ x : x∈x \}$ lead to an infinite path, so both will be $null$ in any model. Note that if you want to have completely unrestricted specification (every formula defines a type), then not only you need a non-classical logic like 3-valued logic, but also you must treat "$∀x∈S\ ( Q(x) )$" as an abbreviation for "$∀x\ ( x∈S ⇒ Q(x) )$", with the 3-valued semantics for "$⇒$".