Proving the rules of a complicated game are well defined

Question

What strategy could one use to formally model a game and prove that the rules do not lead to any self contradiction?

A major example that comes to mind is Magic the Gathering. The card interactions can get so complicated that there are several levels of judges in competition whose major role is in clarifying card interactions that come up. Now, as far as I know there has never been a situation that could not be decided (to the extent that the rules had to be altered), but how would one prove this could not occur?

A milder example is Go. This game is (I believe) fully self consistent, at least under the Chinese Scoring system. However, if you read the Wikipedia article on Go I believe the rules are underspecified in that they don't fully settle what happens when people are stubborn in territory disputes (namely how to decide if a stone is dead) after both players pass: https://en.wikipedia.org/wiki/Rules_of_go In this link user 'Andy' gives what I think is a well defined specification of the rules of Go: https://boardgamegeek.com/thread/457202/rules-about-end-game-dead-stones/page/2 In summary, what I am looking for is a general method of converting rules of popular games to a formal model which we can check is self consistent.

I ask this question here rather than card/board game Stackexchange because I think it is really a mathematical modelling question.

Answer 1

"In summary, what I am looking for is a general method of converting rules of popular games to a formal model which we can check is self consistent."

This depends on how you have set up the game, and what you want to know about it. For example, in Go, questions like "whose turn is it" or "is the game over" are usually straightforward, questions like "does this ruleset ensure that games don't go on forever" may take a bit more work to answer (and the answer is "no" for many Go rulesets), and "does this ruleset provide an explicit algorithm to determine the ending score?" (the answer is "no" for a few popular rulesets and "yes" for many others).

In Magic: The Gathering, things are much more complicated, as there are million different flavors of questions of the form "is this a legal move", and presumably you want to know "does this rulebook answer this question in exactly one clear way in every situation" or something.

However, if you ignore the practical matters of the complexity of Magic, the mathematician's attack would be the same. Formalize the definition of game states, formalize the rules, and try to write a proof that they do what you want them to (e.g. that the rules don't reach a contradiction as to what state transitions are allowed, etc.). I can't get into significantly more detail to handle your full general question. Some discussion of the issues with various Go rulesets are included in the book "Mathematical Go".

Answer 2

The question is straightforward or impossible depending on what you mean by Consistent.

Games that consist of a sequence of "moves" that update a finite amount of discrete state information have the same generality as computer programs and their analysis is subject to the same limitations.

Questions about consistency in a higher sense such as "given this rule set, is there a position where no player has a valid move" are not mechanically resolvable by any automatic procedure. They are analogous to generally unsolvable questions about programs, like correctness or halting. And when they are resolvable in principle, due to a finite search space (like playing perfect 8x8 chess) they are usually not feasible in practice due to the number and complexity of possibilities to be considered.

Questions about consistency in a simpler sense, such as "does this ruleset define a game" are analogous to judgements of syntactic correctness, like "does this program compile in that Java compiler". That can be done, by having a relatively general specification language for games that is implemented on a computer. Then

is this game well-defined

becomes the question of whether the game can be written as a compilable program in the specification language. If presentation as a specification is one's definition of even having a precise game to talk about, then the question is answered simply, by running the compiler and seeing if it accepts the spec.