Chris Dams's proof:From: Chris Dams <chr...@wn5.nospamplease.nl>
Newsgroups: rec.games.go
Subject: Re: Model for the World Amateur Go Championship Rules
Date: Wed, 12 Apr 2006 20:56:06 +0000 (UTC)
Message-ID: <e1jph6$13q$1@wnnews.sci.kun.nl>
References: <p67q32p0mo82bm1c2h5gpolhs93hncpu52@4ax.com> <e1j9jn$pla$1@wnnews.sci.kun.nl> <27gq32p0vhdvn6j0e5o1fneud7erkaas4a@4ax.com>
Dear Robert,
Robert Jasiek <jas...@snafu.de> writes:
>On Wed, 12 Apr 2006 16:24:23 +0000 (UTC), Chris Dams
><chr...@wn5.nospamplease.nl> wrote:
>>> In a position, a string of a player is _two-eye-alive_ if the
>>>opponent cannot force no intersection of the string with a
>>>two-eye-formation on.
>>
>>> _J2003-alive_ is defined like in J2003 as either uncapturable,
>>>capturable-1, or capturable-2.
>>
>>> In a position, a string is _WAGC-alive-in-seki_ if it is
>>>J2003-alive and not two-eye-alive.
>>
>>> In a position, a string is _WAGC-alive_ if it is either
>>>two-eye-alive or WAGC-alive-in-seki.
>>
>>From these definitions it follows that WAGC-alive is identical to
>>J2003-alive.
>I doubt this. If you claim it, then please present a formal proof!
I have to admit that I, at first, interpreted "either" as "or" in the definition of WAGC-alive. However, I think the identity of J2003-alive and WAGC-alive is still provable. Proof is given below.
Let us denote
> In a position, a string is _WAGC-alive-in-seki_ if it is
> J2003-alive and not two-eye-alive.
as
WAGC-alive-in-seki == J2003-alive && (!two-eye-alive)
In the same notation we also have from
> In a position, a string is _WAGC-alive_ if it is either
> two-eye-alive or WAGC-alive-in-seki.
WAGC-alive == two-eye-alive ^^ WAGC-alive-in-seki.
Substituting the former into the latter expression, we find
WAGC-alive == two-eye-alive ^^ (J2003-alive && (!two-eye-alive)).
In propositional calculus this reduces to
WAGC-alive == J2003-alive || two-eye-alive.
If we now also have the implication two-eye-alive -> J2003-alive if follows that
WAGC-alive == J2003-alive.
For the implication two-eye-alive->J2003-alive, imagine that a string is two-eye-alive. The string can either be uncapturable or not uncapturable.
(1) The string is uncapturable -> It is J2003-alive
(2) It is not uncapturable -> The string is either capturable-1 or not capturable-1
(2a) It is capturable-1 -> It is J2003-alive
(2b) It is not capturable-1 -> Because the string is two-eye-alive there is in every hypothetical-strategy of its opponent a hypothetical-sequence in which we reach a two-eye-formation that includes one of its intersections. For every hypothetical-strategy H of the opponent, we choose a hypothetical-sequence S(H) in it where the oponent reaches a two-eye-formation and subsequently only passes. Because the two-eye-formation cannot be capture by only moves of its opponent, it consists of permanent stones. In S(H) the two-eye-formation that is formed on the captured string has either a stone on local-1 of the string or it does not have a stone on local-1 of the string
(2b1) If it has a stone on local-1 of the string, it is also on local-2.
(2b2) If it does not have a stone on local-1 of the string, then local-1 of the string consists of the one or both of the empty intersections of the two-eye-formation. Actually, it consists of one of the intersections since if it would consist of both, these would have to be adjacent to each other which contradicts the definition of a two-eye-formation. So, local-1 of the string consists of one intersection and during S(H) it becomes one of the the empty points of a two-eye-formation. This implies that this two-eye formation includes strings that occupy the intersections adjacent to local-1. Because local-1 consists of one intersections these adjacent intersections where empty or occupied by opposing stones. Hence, these intersections belong to local-2 of the string.
In both (2b1) and (2b2) we see that the two-eye-formation that is formed in S(H) has permanent stones on local-2 of the string. Hence, if every hypothetical-strategy of the opponent of the string there is a hypothetical-sequence where a permanent-stone is played on local-2. Hence, the opponent cannot force both caputre of the string and no local-2 permanent stone. Hence, the string is capturable-2.
Hence, it is J2003-alive.
Hence, under the assumption that the string is two-eye-alive, we find that it is J2003-alive. QED.
Best,
Chris
Start of Chris Dams's proof written down differently (Jasiek):Proposition:
In a position, let X be an arbitrary, fixed string.
X is WAGC-alive <==> X is J2003-alive.
Start of a Proof:
"X is WAGC-alive <==> X is J2003-alive"
<==>
"X is two-eye-alive XOR X is WAGC-alive-in-seki <==> X is J2003-alive"
<==>
"X is two-eye-alive XOR (X is J2003-alive AND NOT (X is two-eye-alive) <==> X is J2003-alive"
<==>
"
Case 1: X is two-eye-alive:
X is two-eye-alive <==> X is J2003-alive
Case 2: NOT (X is two-eye-alive):
X is J2003-alive <==> X is J2003-alive
"
Up to here, Case 2 is proven. To prove all, what remains to be proven is is Case 1. This is to be done below.
"X is two-eye-alive <==> X is J2003-alive"
<==>
"X is two-eye-alive <==> X is uncapturable XOR X is capturable-1 XOR X is capturable-2"
This is still to be proven in this proof scheme. See Chris Dams's proof for that.
Presuppositions for WAGC-alive == J2003-alive (Jasiek):These terms are defined in the following extract of J2003/35a:
position, string(s), player, (opponent, by "player" and standard context), intersection(s), adjacent, force
"Axioms [...] A player can force something if there is at least one hypothetical-strategy of his so that each compatible hypothetical-sequence fulfils that something."
These terms are defined in the following extract of J2003/35a:
uncapturable, capturable-1, capturable-2
"Axioms [...] A player's final-string is capturable-2 if
* it is neither uncapturable nor capturable-1 and
* the opponent cannot - with the same hypothetical-strategy - force both capture of the string's stones and no local-2 permanent-stone of the player."
J2003's alive is defined by the aforementioned extrat and this citation:
"A final-string is alive if it is either
* uncapturable,
* capturable-1, or
* capturable-2."
The WAGCmod page simply gives this an alias: J2003-alive.
"two-eye-formation" and "two-eye-alive", using more basic terms, are defined on WAGCmod.
"WAGC-alive-in-seki" is defined on WAGCmod, uses "two-eye-alive", which is defined on WAGCmod, and uses J2003-alive, which is defined in J2003/35a under a different alias. See above.
"WAGC-alive" is defined on WAGCmod and uses "two-eye-alive" and "WAGC-alive-in-seki", see above.
Furthermore, as explained earlier, "WAGC-alive equals J2003-alive" relies on a particular, presumed position and a arbitrary, fixed string.
Proposition (Jasiek):Given a string in a position, the set-intersection of two-eye-alive and WAGC-alive equals the set-intersection of two-eye-alive and J2003-alive.
Proof:
This follows immediately from the definitions and Chris Dams's proof. QED.
Note:
If you don't see it immediately for J2003-alive=>WAGC-alive, write down these two assumption cases: 1) The string is J2003-alive and two-eye-alive. 2) The string is J2003-alive and not two-eye-alive. Prove it for each case.
Example (Cassandra):
- Click Here To Show Diagram Code
[go]$$
$$ -----------------
$$ | X X X . X X X |
$$ | X O O O O O X |
$$ | X O . O . O X |
$$ | X O O O O O X |
$$ | O X X X X X O |
$$ | O X . X . X O |
$$ | O X X X X X O |
$$ | O O O . O O O |
$$ -----------------[/go]
Definitions (Cassandra, Jasiek):A string is "capturable" unless it is uncapturable.
For a player's final-string, "local-2\1" is local-2 without local-1.
A player's neither uncapturable nor capturable-1 final-string is capturable-2\1 if the player moving second can force at least one permanent-stone of his on local-2\1.
Proposition (Jasiek):The player cannot force a local-2 permanent-stone.
=>
The player cannot force a local-1 permanent-stone
AND
The player cannot force a local-2\1 permanent-stone
Proof:
Trivial.
The second part of Chris Dams's proof for "WAGC-alive equals J2003-alive" is done in an alternative way by Cassandra with help from Jasiek:For the implication two-eye-alive -> J2003-alive, imagine that a string is two-eye-alive. Either the opponent cannot force capture of the string or he can force capture of the string.
(1) The opponent cannot force capture of the string -> It is uncapturable. -> It is J2003-alive.
(2) The opponent can force capture of the string. -> Because the string is two-eye-alive there is in every hypothetical-strategy of its opponent a hypothetical-sequence in which we reach the player's two-eye-formation that includes one of its intersections. For every hypothetical-strategy H of the opponent, we choose a hypothetical-sequence S(H) in it where the player reaches such a two-eye-formation and subsequently only passes. Because the two-eye-formation cannot be captured by only moves of its opponent, it consists of permanent-stones. -> In S(H) the two-eye-formation that is formed on at least one intersection of the captured string has either a stone on local-1 of the string or it does not have a stone on local-1 of the string.
(2a) The two-eye-formation has a stone on local-1 of the string -> the string is capturable-1 -> It is J2003-alive.
(2b) The two-eye-formation has no stone on local-1 of the string -> Local-1 of the string consists of one or both of the empty intersections of the two-eye-formation. Actually, it consists of one of the intersections since if it would consist of both, these would have to be adjacent to each other which contradicts the definition of a two-eye-formation. So, local-1 of the string consists of one intersection and during S(H) it becomes one of the empty points of a two-eye-formation. This implies that this two-eye-formation includes strings that occupy the intersections adjacent to local-1. Because local-1 consists of one intersection these adjacent intersections were empty or occupied by opposing stones. Hence, these intersections belong to local-2\1 of the string. We see that the two-eye-formation that is formed in S(H) has permanent-stones on local-2\1 of the string. Hence, in every hypothetical-strategy of the opponent of the string there is a hypothetical-sequence where a permanent-stone is played on local-2\1. Hence, the opponent cannot force both capture of the string and no local-2\1 permanent-stone. Hence, the string is capturable-2\1. Hence it is capturable-2. Hence, it is J2003-alive.
Hence, under the assumption that the string is two-eye-alive, we find that it is J2003-alive. QED.
WAGC-alive-2\1 equals J2003-alive-2\1Given a final-position, a string in it, and the definitions of local-2\1, capturable-2\1, J2003-alive-2\1, WAGC-alive-in-seki-2\1, WAGC-alive-2/1.
Proposition (Jasiek):
The string is WAGC-alive-2\1 equals the string is J2003-alive-2\1.
Proof:
Part 1 of the proof is analogue to part 1 of Chris Dams's proof.
Part 2 of the proof is as follows:
For the implication two-eye-alive -> J2003-alive-2\1, imagine that a string is two-eye-alive. Either the opponent cannot force capture of the string or he can force capture of the string.
(1) The opponent cannot force capture of the string -> It is uncapturable. -> It is J2003-alive-2\1.
(2) The opponent can force capture of the string. -> Because the string is two-eye-alive there is in every hypothetical-strategy of its opponent a hypothetical-sequence in which we reach the player's two-eye-formation that includes one of its intersections. For every hypothetical-strategy H of the opponent, we choose a hypothetical-sequence S(H) in it where the player reaches such a two-eye-formation and subsequently only passes. Because the two-eye-formation cannot be captured by only moves of its opponent, it consists of permanent-stones. -> In S(H) the two-eye-formation that is formed on at least one intersection of the captured string has either a stone on local-1 of the string or it does not have a stone on local-1 of the string.
(2a) The two-eye-formation has a stone on local-1 of the string -> the string is capturable-1 -> It is J2003-alive-2\1.
(2b) The two-eye-formation has no stone on local-1 of the string -> Local-1 of the string consists of one or both of the empty intersections of the two-eye-formation. Actually, it consists of one of the intersections since if it would consist of both, these would have to be adjacent to each other which contradicts the definition of a two-eye-formation. So, local-1 of the string consists of one intersection and during S(H) it becomes one of the empty points of a two-eye-formation. This implies that this two-eye-formation includes strings that occupy the intersections adjacent to local-1. Because local-1 consists of one intersection these adjacent intersections were empty or occupied by opposing stones. Hence, these intersections belong to local-2\1 of the string. We see that the two-eye-formation that is formed in S(H) has permanent-stones on local-2\1 of the string. Hence, in every hypothetical-strategy of the opponent of the string there is a hypothetical-sequence where a permanent-stone is played on local-2\1. Hence, the opponent cannot force both capture of the string and no local-2\1 permanent-stone. Hence, the string is capturable-2\1. Hence, it is J2003-alive-2\1.
Hence, under the assumption that the string is two-eye-alive, we find that it is J2003-alive-2\1. QED.
Proposition (Jasiek):The set of capturable-2\1 strings is a subset of the set of capturable-2 strings.
Proof:
"Trivial."