A note about coinductively defined predicates

This is a reflection on some lectures by Andrei Popescu (2021).  I am intrigued by the idea of coinduction (which was new to me): a form of definition in terms of rules, which goes beyond inductive definition.  Popescu gives an example of a set which is defined by rules, does not admit of an inductive definition, but admits of a coinductive definition.  This is presented in the context of Isabelle, an interactive theorem prover.  But the idea of coinductive definitions is very intriguing in itself.

So I wanted to make up a simple example in normative reasoning or rule-governed behavior.  I will use the game of chess and the property of being a proper game, that is, a sequence of moves by two players which are entirely in accord with the rules of chess.

The universe U will be a set of countable sequences (finite or countably infinite) of elements of the set V of situations or stages, which are pairs <position, player>.  By a position I mean a complete specification of the pieces on the board and where they are.  A player is an item, White or Black, and for convenience I will use “*” this way:  White* = Black and Black* = White. In stage <p, X>, X is the player who has to make a move, that is, do something that transforms p into another position.

So how can we go about defining the set of proper games?  Let’s begin by aiming for a predicate, “legit” which will apply to such sequences, that is, elements of U.

Inductive definition of the predicate legit

There is one position that is special, the base position, which is the layout of the pieces at the start of the game.  A standard game begins with this.  But chess aficionados like to work on chess problems of many sorts, which begin with a specified initial position (and are meant to arrive at another position). So we will include among proper games any that are played with any chosen initial position.  The definition I propose as a first attempt has a basis clause and a generative clause.

[i] A one-member sequence b = <p, X> is legit 

[ii] if s is a legit sequence, and the last member of s is <p, X> then the result of adding <q, Y> to the end of s is also a legit sequence, provided Y = X* and q results from p by an admissible chess move by X.

[iii] that is all

This is an inductive definition of the set LI of legit sequences.  

But it isn’t good enough: all members of LI are finite.  For the basis clause introduces only finite  sequences, and all the modes of generation preserve finitude.  So by induction, all members of LI are finite.  And the defining rules of the game of chess allow in principle for never-ending games.

Note about checkmate and blocking rules:  There is no position which can result by admissible chess rules from a position in which a king is missing.  Specifically, if s is a legit sequence and <p, X> is a member of s, and a king is missing in position p, then <p, X> is the last member of s. In tournaments there are also artificial rules, like the 50 move rule or 3 repetition rule, used to curtail the length of play, but they are not part of what the game of chess is.

Never ending games of chess

There are certainly infinite sequences that should count as proper games of chess, although they will never be played in reality (cf. Stewart 1995).

So what sort of definition would work to define the set — call it LG — of proper games, which includes all the right members of U, infinite as well as finite?

First of all, what [i] and [ii] say should remain true for LG, though not [iii], and the rule of induction should not be applicable to LG in the above fashion. 

Following Popescu’s lead for this simpler example, we can put it this way.  The set LI is the smallest set of sequences such that [i] and [ii] are true of it.  More precisely:

Definition. LI is the smallest subset W of U such that:

(a) all one-member sequences b = <p, X> are in W

(b) if s is in W, and the last member of s is <p, X> then the result of adding <q, Y> to the end of s is also in W, provided Y = X* and q results from p by an admissible chess move by X.

As Popescu says, it would not do to just change “smallest” to “largest” in this formulation, for it would let in every sequence which has no last member.

What is needed instead is to select the largest class of sequences that represent games played by the rules of chess — the ones in which every stage follows legitimately upon the one before it.  (Also of course that if member e has a successor then that follows upon e by an admissible chess move.   But that is redundant, for the above would apply to e’s successor.)

So we should propose:

Definition. LG is the largest subset T of U such that: 

(a’)   all one-member sequences b = <p, X> are in T

(b’) if s is in T then for any n, if the n^th member of s is s(n) = <q, Y>, and s(n) is not the first member of s, then the (n-1)^th member of s is a couple <p, X> such that Y = X* and q results from p by an admissible chess move by X.

Note that (b’) is, as it were, backward-looking:  unlike (b) it specifies where a position comes from rather than what it leads to. 

Does LG exist?  And if it does, does it include all and only proper chess games?

The set LG, thus defined

Here are the questions that need to be answered

1. Does LG, thus defined, exist? To be precise: is there a largest set T such that (a’) and (b’) hold?
2. Is LI part of  LG? 
3. Does LG have any members other than the members of LI?

The answer to all three is positive.

For question 1, note that the set of all one-member sequences is a set T such that (a’) and (b’) hold, trivially.  Secondly, if S = {T(i): i in J} is a family  of sets such that (a’) and (b’) hold, then ∪S is also such a set, for those conditions apply to the members individually and not to any relations among members of U.   The answer to question 2 is somewhat less obvious.

Theorem 1. If s is a finite sequence in U then s is in LI if and only if it is in LG.

Argument:  

Suppose s in U has n members.  

If n = 1 then s belongs to both LI and LG by clauses (a) and (a’).

Suppose n > 1 and that T1 holds for all sequences in U of length less than n.  Then s belongs to LG if and only if s(n) = <q, Y> results from s(n-1) by an admissible chess rule, while replacing Y*by Y.  But it is also the case that s belongs to LI, if s’ = <s(1), …, s(n-1)> belongs to LI, if and only if  s(n) is related to s(n-1) in precisely that way.

Since there are examples of never-ending chess games it follows also that LG has members not in LI.

To prove a property in LG

To see how it is possible to prove things about the games in LG, going beyond what can be done for LI by mathematical induction, but in roughly the same way, I will use a specific example of a theorem about the game of chess

At any given stage in a game, a player may or may not have a winning strategy.  X wins the game exactly if a stage <p, X> is followed by stage <q, X*> and there is a king missing in position q.  Since we ignore the practical, arbitrary stopping rules applied in tournaments, there are three possibilities:  X wins, X* wins, or neither wins which is the same as that the game does not end, the representing member of U is an infinite sequence.  This is called a draw.

A player may have a winning strategy, or a strategy that forces a draw. It was Zermelo who began the mathematical study of chess in the early time of game theory.  A very basic result, connected with Zermelo’s work, is the theorem  that if a player has no winning strategy then his opponent has at least a draw-forcing strategy.  

This is not a result that we can prove by mathematical induction for the set LI.  There all games end either in a check-mate or end arbitrarily, that is, end although they could be extended.  There is no way for either player to force such an abrupt ending (assuming they are not subject to the practical limitations such as are set for a tournament).  For there is no position, except at check-mate, when the player whose turn it is, has no possible moves.

The theorem pertains therefore not to LI but to LG.  If we look at the proof, we see that it nevertheless looks very much like a proof by induction.  The theorem was proved by Kalmar in 1928:

Theorem 2.  At stage s(n) = <p, X> in member s of LG, if player X  does not have a winning strategy then X* can at least enforce a draw.

Proof.  Suppose that at stage s(n) X does not have a winning strategy.  Then whatever move X makes to yield s(n+1) = <q, X*>, X still does not have a winning strategy.  

For suppose he does; call it strategy S.  Then whatever move X* makes to produce s(n+2) = <r, X>, there is a way for X to execute that strategy so as to force a win.  But in that case, X had a winning strategy at stage s(n), namely to pursue S after transforming position p into position q.

So, generalizing, if X does not have a winning strategy at stage s(n) then X does not have a winning strategy at s(n+1).  So at s(n+1), when it is X*’s turn to move, X* can choose a position where X still does not have a winning strategy.

This implies that at this stage X* has a strategy that will prevent X from winning, namely to make such a choice at each successive stage.  This will either lead to a win for X* or will prevent the game from ever ending.

Fine.  But now we have a puzzle:  this looks like a proof by mathematical induction, but LG is not an inductively defined set.  So what is the actual form of this proof?

Koenig: “About a method of proof from the finite to the infinite”

What we have to notice about LG is that the infinite is involved in one way, but not in another: 

This should remind us of Koenig’s lemma:

the sequence representing a game may be infinite, but at each stage, there is only a finite number of possible next stages

Koenig’s Lemma. If a tree with the finite branching property has infinitely many nodes then it has an infinite branch

The proof of Koenig’s lemma requires the Axiom of Choice.  And it is Koenig’s lemma that provides the implicit assumption about an infinite sequence of rule-and-aim governed choices in the above argument.

Looking back now to the argument in the previous section, suppose that in sequence s, at stage s(n), X does not have a winning strategy.  Now consider the tree generated at s(n) by generating as stage n+1 all the different possible results of legitimate moves by X, then at stage n+2 all the possible moves by X* and so forth.  The stages in the branches are called the nodes in the tree, and each node has a rank, the number of steps it is beyond s(n).

X* will pursue the above indicated strategy, while X may pursue any strategy he likes.  

This is a finitely branching tree, because there are at any point, in any game of chess, only finitely many possible moves for the player whose turn it is.  And some or all of the branches may have a node N which is a checkmated position (a king is missing).  The property of X not having a winning position is preserved in every move in every branch, so it is a property of X at every node.  (This follows by mathematical induction: each node has a finite rank.)  Therefore the immediate predecessor of N was a position in which X did not have a winning position.  Hence the checkmate is by X*.  

If it is not the case that checkmate is reached in all branches then at every rank there is in some branch a move to a node with the next rank.  Hence there are nodes with every rank 1, 2, 3, …, so  number of nodes is not finite.  Now Koenig’s lemma rules out the idea that this could be because the tree has infinitely many finite branches of increasing length.  The  lemma establishes that the tree has an infinite branch, which counts as draw in this (infinite) game of chess.

So here is the diagnosis of the sort of reasoning about LG in our example, which looks like mathematical induction but isn’t: 

it is a combination of arguments that include a mathematical induction and also an application of Zorn’s lemma 

(which is to say, it involves an appeal to the Axiom of Choice, guaranteeing the existence of a specific, required, series of elements selected by an infinite number of choices).

NOTES

I want to thank Ali Farjami for directing me to this fascinating subject.

1) Coinduction is informally described as the dual of induction.  An inductively defined set is the smallest set closed under its defining relation, or equivalently, under its defining rules. We can think of such a definition as a procedure starting with certain members of the set and then generating all the others by applying the rules.  A coinductively defined set is the largest set of items that are produced by the defining rules from others of its members. Equivalently, a coinductive definition specifies the greatest set R consistent with given rules: every element of R can be seen as arising by applying a rule to some element of R.

2) The general form in which Koenig stated his 1927 lemma was this:

Let E₁, E₂, E₃,… be a countably infinite sequence of finite nonempty sets and let R be a binary relation with the property that for each element x_n+1 of E_n+1 there exists at least one element x_n in E_n, which stands to x_n+1 in relation R which is expressed by x_nRx_n+1. Then we can determine in each set E_n an element a_n such that a_nRa_n+1 for the infinite sequence a₁, a₂, a₃, . . . always holds (n = 1, 2, 3, . . .). 

For the exact form in which I show its application, with its proof, see Formal Semantics and Logic pp. 16-18.

3) Having come this far I can now appreciate that the subject can be presented much more elegantly by recourse to the Knaster-Tarski fixed point theorem (as Popescu remarks). 

Suppose F is the function defined by the rules in question, so that F(X) is the set of results of applying the rules to elements of X.  Then the least fixed point of F is the set  ∩{X: F(X) ⊆ X}, that is, the smallest set containing X that is closed under application of those rules — which corresponds to an inductive definition of that set.  And the greatest fixed point of F is the set ∪{X: X ⊆ F(X)}, that is, the largest set of which we can say that all its members are obtained by the rules from its members — which corresponds to a coinductive definition of that set.

But the process was not transparent to me till I had traced it out in terms more familiar to myself, at a more elementary level.

BIBLIOGRAPHY 

Christian Ewerhart  “Backward induction and the game-theoretic analysis of chess”.  Games and Economic Behavior 39 (2002): 206-214.

König, Dénes (1927), “Über eine Schlussweise aus dem Endlichen ins Unendliche”.  Acta Sci. Math. Szeged 3, 121-130 

Paul B. Larson  “Zermelo 1913”. In: Ebbinghaus HD., Fraser C., Kanamori A. (eds) Ernst Zermelo – Collected Works/Gesammelte Werke. Schriften der Mathematisch-naturwissenschaftlichen Klasse der Heidelberger Akademie der Wissenschaften, vol 21. Springer, Berlin, Heidelberg: 2010. https://doi.org/10.1007/978-3-540-79384-7_9

Lawrence C. Paulson “A fixedpoint approach to (co)inductive and (co)datatype definitions”. Cambridge computer laboratory technical report 1997.  https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-320.pdf

Andrei Popescu “Inductive and Coinductive Reasoning with Isabelle/HOL”.  Midlands Graduate School in the Foundations of Computing Science 2021.  12-16 April 2021.  https://staffwww.dcs.shef.ac.uk/people/G.Struth/mgs21.html

Ulrich Schwalbe and Paul Walker “Zermelo and the early history of game theory”.  Games and Economic Behavior 34 (2001): 123-137.

Ian Stewart “The Never Ending Chess Game”  Scientific American 273 (4): 182-183. Downloaded from ResearchGate.