I think a rule which makes it difficult to label boards as red or green is almost always a bad rule. So yes, I was thinking more along the lines of a problem like those board coloring problems, but in this case it would come up a bit more “organically”.
For a finite board and a rule which can be quickly checked for each case, I’m pretty sure there are no undecideable conjectures 
(of course with appropritate conditions on what qualifies as a “conjecture about the rule”, I can’t just take some unrelated conjecture and throw it at the rulemaker)
More precisely: Every claim of the form “Is there an example of X?” can theoretically be checked by going through all possible board positions.
These things are so counterintuitive, so I’m afraid I’m making some embarassing mistake here… It always baffles me the sort of simple questions that can turn out to be undecideable. But I think when everything is finite and bounded, we should be fine.
4 Likes
No, you’re 100% correct. 
This is my field of study, I really want to write about 5 paragraphs about this, but I’m too tired to do so (and I just fell asleep halfway through my attempt)
Maybe tomorrow
2 Likes
A hidden rule and a conjecture are essentially like algorithms, implicit descriptions of the function that maps from board positions to labels.
However, the rule and conjecture may be worded very differently using disparate logical constructs. Even if the two implied functions are equivalent, and both are relatively simple to check (and hence each are individually decidable), I think it could be very difficult to determine that they are in fact equivalent.
Given that we are dealing with finite problems (the domain of the function is limited to a finite set of board positions), it should always be decidable, by simply testing across all possibilities, but whether it is easy to logically determine the equivalence of two rules is another issue.
1 Like
Yes, of course, you’re right. I completely overlooked that in haste.
Examples of such rules could be stated in the form:
A board is green if and only if there are at least X chains where each has exactly Y liberties.
Your sleep schedule really confuses me, how long have you been awake for? ^^
This is a bit weird, but I’ll take this opportunity to mention it since it’s not often I get to talk about this sort of stuff: I wrote my bachelors thesis about a problem which is undecideable in PA but decideable in ZF, available here if anyone is interested (no original research, it’s intended to be an introduction accessible to someone quite new to logic).
8 Likes
?
Wait Martin is offline,
It’s ok if people need to sleep sometimes you know 
6 Likes
Actually I’m here right now, but I’ll go to sleep soon.
1 Like
I wouldn’t really expect him to be on for an hour waiting for someone to post.
3 Likes
This does not have to be played as a live game. After all, it’s a web forum, where everything is saved by default, and maybe a correspondence pace would be more comfortable.
We might all do better sleeping on the information and seeing if we have fresh ideas in the morning.
1 Like
The impatient among us (and I’ll admit I should probably count myself to that group) should be happy I didn’t go with the original plan for this game 
5 Likes
Maybe we should call this “Blitzdo”
3 Likes
Yeah, there’s not much “Zen” about it… I think a quicker pace is good while learning the game though
3 Likes
Best name ever!
It is a game.
Yesterday, I think I had been awake for 21 hours at that point. My sleep “schedule” is a bit difficult to describe. I think my biological clock thinks a day should last for 26 hours, and thus my bed time naturally drifts towards late at night, to early in the morning, to late in the morning, until it becomes difficult to combine sleeping with family dinner. Usually at that point I choose to sleep after dinner, essentially skipping a day, and I’m back at a more or less normal bed time. Yesterday was one of those skipping days.
My slightly off-topic reply about undecidable problems with rules
As an example of something difficult to check: consider playing zendo on finite planar graphs, where the vertices are coloured by, say, five different colours (currently, we’re essentially playing an easier game, where we only consider gobans as our planar graphs, and only use three colours, black, white and empty). Then the rule “no edge can connect two vertices of the same colour” is very easy to check. If someone were to ask “every green koan can be recoloured with only four colours (and stay green)”, then this check would be equivalent to the famous four-colour theorem, which was only proved in 1976 after countless of failed earlier attempts. In 1975, the Master would’ve had a very hard task trying to give a counter example.
Suppose we’d play zendo, but the boards are finite computer programs (for simplicity’s sake, let’s say they’re programmed on a Turing machine). There are only countably many such programs. If the Master now chooses the rule “a koan is good if its program does not get stuck in an infinite computation”, then no finite computer program can be made to decide for every possible koan whether it is green or red, since this is equivalent to the halting problem. We would need a Master capable of something that no finite computer program could (i.e. the Master needs to live in a higher Turing degree)
Thus, even if the boards we play on are finite, but there are countably many boards, there are undecidable problems. If we’d write rules not just for a fixed board size, but for any arbitrary NxN goban, then it is possible to formulate rules that are undecidable, in that no algorithm could colour all koans.
Similarly a question could be asked to the Master that has no counter examples, yet it is impossible to prove that there are no counter examples.
When there are finitely many possible koans, such as with our Zendo game with fixed board size, we cannot abuse the kind of self-referential problems that the halting problem and Gödel’s first incompleteness theorem have, but we can still create artificial ways to introduce it into our system.
For example, the rule “all boards, except the empty board, are green and the empty board is red if and only if ZFC is consistent”. If it is agreed on that the Master can only use the theory of ZFC as tool to determine whether a board is red or green, then the Master would be unable to give an example of a red koan, but also unable to prove that all koans are green.
Of course it is well-known that Zen Masters are very inaccessible, thus they’d have no problem with providing the empty board as a red koan in this case
If, however, the rule is computable, then there is no problem and the Master should be able to give any counter examples whenever they exist, or else prove the nonexistence of them, indeed by going through all the examples one by one. This could of course take too long in practice; e.g. the optimal winning strategy for Go is computable, yet we can be certain that we will never find it by going through all possible Go games (although there are only finitely many of them).
If we have a countably infinite set of koans, the Master can still decide for any given koan whether it is green or red, but may be unable to prove a general statement about an infinite subset of boards.
6 Likes
As much as I like discussing about fascinating mathematical and logistical topics, I would like to bring the subject back to the game. As a motivation I present you a Koan:
