Being good in maths at school is probably insufficient for understanding well how to prove and how proofs work. I had way above average maths lessons at school, was the best pupil in maths and we did some (sometimes fake) proofs of classical maths. But it did not prepare me for rules maths. For the proofs there, I needed a couple of years at university. Not because the proofs would be difficult but rather because they are so rather basic that one needs a clear view on what is and what is not a definition or a proof.

Your major mistake is: You do not recognize at which procedural moment which prior definitions or propositions are already given and may be applied and which not.

Look at J2003 and its pile on pile definitioning scheme. This is exactly how new definitions and new proofs may be establised. By using only the previously already known. ONLY!

Here are some comments on your long attached file. I do not comment on all the many minor unclarities.

Your classification headlines are unclear. Maybe you mean: "If either players tries to force creation of a ko-ban, then the opponent can prevent this."

If you should be attempting a subclassificatin scheme, I am not sure which you intend.

You assume only one end of evaluation position per studied string. This is wrong. More than one hypothetical-sequence exist!

It is unclear why the examples with visible-kos under the headline "Independent of ko rule during evaluation" should be independent of the used ko rule. (It is straightforward to introduce ko rules so that we get different outcomes.)

Since different ko rulesets can create different results, you should specify the set of ko rulesets that you permit as input.

You mark stones as ko stones ("part of a cycle") but you overlook that every stone might or might not be part of a cycle, depending on which hypothetical-sequence is being studied and whether the players cooperate or force something specific.

Do your own-local and both-local terms have any purpose? If yes, which?

That's no contradiction. Let the "term" be defined earlier, it becomes a "parameter" in the moment, when anything else might be declared as a function of it. This might not be so apparent when you remain in one rule set only, but it is evident if you want to compare two rule sets.
If you use one and only one term in two rule sets, based on the definition of this term in one rule set, it is as I said before: You assume that the general framework of both rule sets - including all procedures - is identical.

The term alive as defined in J2003 does NOT rely on defining "two-eye-formation" !!!!!!!!!!!!!!!!!!!!!!!!!
The numbers of exclamation marks does neither inhance nor ensure the accuracy of a statement. You want to refute something that I have not written. Completely indepentent from the definition of "two-eye-formation", some of your "alive"-subsets are a function of "two-eye-formation". And it is what is inside this function, what you apparently do not realise.

A neutral observer migth identify a correlation between

• 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.
• A player's final-string is capturable-1 if it is not uncapturable and the opponent cannot - with the same hypothetical-strategy - force both capture of the string's stones and no local-1 permanent-stone of the player.
• 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.

Each of the quoted definitions uses an identical procedure "cannot force no". Referring to the term "force" therein, see above.

You say: "None of the "life-subsets" of J2003 can - following their definition - contain anything else than "two-eye-formation" or "Seki"." Do you make this statement before, during or after Chris's proof? In which context do you assume "seki" to be defined?
The statement is implicit part of your J2003. And part of general Go knowledge
If you go back to my first diagram in this thread, you will realise that I made this statement before Chris' "proof".
Definition of "Seki" - in the sense I suppose you to have "definition" in mind - is not required.

See A final-string is alive if it is either uncapturable, capturable-1, or capturable-2.

"uncapturable", "capturable-1" and "capturable-2" are all subsets of "alive".
Completely independent of a rule set (as long as we remain inside what is generally understood as "Go"), all "alive" strings are either "two-eye-formations" already, or can be forced into "two-eye-formations", or have nothing to do with "two-eye-formation", but remain on the board as they are.
Usually, "Seki" is just a short name for the latter subset. I.e. it is the complement of "two-eye-alive".

Your post is not a proof at all for in particular the above unclarities.
Let's return to Chris' "proof".
What Chris really has proven, is the following, what cannot be very surprising:

• Members of a subset A of the set "two-eye-alive" are also members of the set "uncapturable".
• Members of a subset B of the set "two-eye-alive" are also members of the set "capturable-1".
• Members of a subset C of the set "two-eye-alive" are also members of the set "capturable-2".
• Subsets A, B, and C are distinct, and their union is the set "two-eye-alive".

As I had already written in the very beginning of this topic, nothing had been done than clustering "alive" positions in two different ways. First in J2003, thereafter using "...-Seki" as a bridging element to WAGCmod.


Logic follows the same principles in all fields of mathematics. It has to do with not being aware of the preconditions of the framework used, when throwing some smoke granades makes is temporarily possible to hide a division through Zero, for example, during the course of a "proof".
In my opinion, you are absolutely focussed on a very special type of "proof", in a very special field, and neglecting some fields, which might be also useful.

Your major mistake is: You do not recognize at which procedural moment which prior definitions or propositions are already given and may be applied and which not.
Did you ever have a look at yourself in the mirror?

Look at J2003 and its pile on pile definitioning scheme. This is exactly how new definitions and new proofs may be establised. By using only the previously already known. ONLY!
You have defined so much, and what you defined has become second nature to you, so it's understandable that sometimes you seem to overlook some side effects of dependencies between what you defined. This is true especially for "force".

It may be defined within the rule set, what is meant when using "force" (e.g. "the opponent will be unable to reach a complementary result"). But despite this (declarative) "definition", "force" (in its content) is based on everything that is defined before, concerning the evaluation procedure.

If the evaluation procedure of two rule sets is not identical (i.e. the results are not identical), you must not use the same term for "force" within the two rule sets. Or otherwise any "proof" of the identity of the rule sets' "alive" philosophies is only a phantom.

Only if the evaluation procedure of two rule sets is identical (i.e. the results are identical), it will do no harm using the same term for "force". But in this case any "proof" of the identity of the rule sets' "alive" philosophies is trivial.




Your classification headlines are unclear. Maybe you mean: "If either players tries to force creation of a ko-ban, then the opponent can prevent this."
The headlines are not this important.

If you should be attempting a subclassificatin scheme, I am not sure which you intend.
Complete and as subdivided as necessary to incorporate the investigated rule sets' probably diverging results and / or parameters used.

You assume only one end of evaluation position per studied string. This is wrong. More than one hypothetical-sequence exist!
May be. If you have any example with multiple forced sequences ending in diverging results for the string under evaluation, please let me know.

It is unclear why the examples with visible-kos under the headline "Independent of ko rule during evaluation" should be independent of the used ko rule. (It is straightforward to introduce ko rules so that we get different outcomes.)
Concerning #15, #16 you are right. But this is a typo, as I accidentally forgot a Dame. PDFs have been edited.
Concerning all the other examples in table 1 with visible Ko, please let me know how the Ko-Pass rule should look like to gain different results.
Some super-Ko rule (perhaps you had this in mind) is out of the field of observation, because not used by any of the investigated rule sets.

Since different ko rulesets can create different results, you should specify the set of ko rulesets that you permit as input.
This is done in table 2, where it is necessary.
The examples in "classification" mirror the rule sets given in "comparison".

You mark stones as ko stones ("part of a cycle") but you overlook that every stone might or might not be part of a cycle, depending on which hypothetical-sequence is being studied and whether the players cooperate or force something specific.
The fate of single stones in table 2 depends on the fate of neighboring strings. I had been too tired to just copy the diagrams and redye some stones.

It goes without saying that any player can force the capture of his stones. But I do not think that this complies with the J2003 motivation for "force", see
A player's opponent can force something if the opponent has at least one strategy so that that something is fulfilled regardless of the player's chosen hypothetical sequence.

There is a hierarchie of what the player wants to accomplish for the string (or its successor):

• It cannot be captured due to at least 2 taboo-points.
• It cannot be captured due to Dame.
• It cannot be captured due to a cycle respectively is part of a cycle.

The opponent has to read the list upside down.

Do your own-local and both-local terms have any purpose? If yes, which?
It's the reflection of Lady Justice's view. Stay independent of any rule set's terminology.

"own-local" corresponds to "local-2", as used in J2003.
"both-local" is what I think is really "local" (i.e. no effect beyond any living groups).

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

You do not recognize at which procedural moment which prior definitions or propositions are already given and may be applied and which not. Even worse, intentionally you presuppose informal, verbal concepts as if they had been well-defined in a mathematical sense. After haaving done so, you complain about circularity or triviality created by yourself in the form of fake maths. As long as you do not want to learn mathematical proving, it is fruitless to discuss with you about why a proof is correct or incorrect.

You are right to recognize that different definitions of "force" might inhibit equivalence.

own-local differs from local-2.

What I have written about the real nature of Chris' proof has nothing to do with verbal concepts. The proof in itself is without flaw, but it does not prove what stands before q.e.d.
And it remains trivial to "prove" that a set remains unaffected by clustering it.


Yeah, I forgot Uttegaeshi (has to sharpen the text in the legend) and our "at least one" vs. "all of" difference. But in the moment I don't think that it really matters that your local-2 might be sometimes smaller than my own-local.

By the way:
For a player's final-string, local-2 is local-1 and, recursively, any adjacent intersection without a stone of a string that is of the player and either uncapturable or capturable-1.
Is it really necessary to include "local-1" in "local-2" ? If at least one permanent successor of a captured string in on local-1, J2003 will stop at "capturable-1".

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

Hear, hear. So far you have said about the proof itself: 1) It is trivial. 2) It is wrong. 3) It is correct without flaw.



It does not prove the definitions of the terms it uses. Definitions are not proven anyway - definitions are to be well-defined and it must be possible to reduce them to axioms of the used axiom set.

But I guess this might not be what you mean.



You abuse this.

***

Necessary in which sense? After having determined that a string is not capturable-1, defining local-2 to include local-1 gives the string's player greater freedom. - I have not checked how it affects examples. Anyway I would check first whether it is needed for Chris's proof to work.

"Proof" refers to what Chris' has really proven in my opinion. This is the second part of his text (see also below). This second part works in J2003 only, so it is not influenced by anything, which might be part of WAGCmods preconditions. "Precondition" is, what you continuously seem to regard as not so important.

Statement 1) refers to the precondition that both rule sets use the same framework. Under this precondition it is trivial to prove the identity of the resprective "alive" statuses.
Statement 2) refers to what cannot be taken from the WAGCmod rule text: "Force" inside WAGCmod is undefined. So there is no precondition that it equals "force" inside J2003, so the "proof" cannot be valid.
For statement 3) refer to above.


If we now also have the implication two-eye-alive -> J2003-alive it follows that WAGC-alive == J2003-alive
For the implication ...

... it is J2003-alive. QED.
The implication is what Chris' really has proven. And it is no prove of definitions.
There is no prove of "WAGC-alive == J2003-alive" possible because we cannot get any idea from the rule text what "force" inside WAGCmod is.


***

Necessary in which sense? After having determined that a string is not capturable-1, defining local-2 to include local-1 gives the string's player greater freedom. - I have not checked how it affects examples. Anyway I would check first whether it is needed for Chris's proof to work.
You are inconsistent, Robert.

You insist on using XOR instead of OR for operations with naturally exclusive variables.
But include something in local-2 that cannot have any effect on capturable-2, in which definition it is used. Local-1 and local-2 are not distinct.

For use in capturable-2, it would be sufficient to have
For a player's final-string, local-2 is, recursively, any local-1 adjacent intersection without a stone of a string that is of the player and either uncapturable or capturable-1.

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

Instead of dismissing the proof's first and easy part, you should try to understand it!



Wrong.



I have written a lot to help you with the preconditions. See in the earlier messages.



Yawn. Mathematicians like to abbreviate. If you do not understand the abbreviations and obvious omissions, either get used to them by reading first year's maths students practice books or wait some more years for my Go Rules Encyclopedia, in which I might explain Chris's Proof for Dummies.

***

I am not inconsistent WRT to local-1 but use local-1 and local-2 as growing environments. First it is checked whether life occurs in the smaller, then whether life occurs in the increased, larger environment.



In the rules, I do so for greater clarity. In a proof, I start from the definition, which uses XOR. Only a next step might then transform to OR. Do not begin with the second step!



You have not understood how capturable-2 works. That a string is not capturable-1 does not (necessarily) mean that having local-1 as a subset of local-2 would have no effect on capturable-2.



It would be possible to define such a capturable-2-Cassandra. Currently I do not see a relevant advantage for it though. I see a disadvantage: Chris's proof would not work as is any longer. One would have to find a new proof, if then any did exist.

There would be no disadvantage, Robert.

Advantage would be that the definition of capturable-2 would be independent of the definition of capturable-1 (which refers to local-1).

If Chris' proof would it make necessary to rely on local-2 (including local-1), why do you have any problem with referring to an area instead, which is the sum of local-2 (excluding local-1) and local-1 ?
Chris' proof would remain unaffected.


By the way:
Congratulation the the German Pair Go Championships !

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

I maintain my stated disadvantage.



Ok, but then one would have the same desire for capturable-1 WRT uncapturable. The J1989/J2003 construction of life simply is not as simple as it could get.

Anyway, sekis and capturable-2 shapes should be studied as to which are invariant or not under slight definition changes ("all" vs. "at least one", iterative vs. mutually exclusive local-x)



Because I do not see that the proof would remain unaffected and a new proof for a changed local-2 definition is not available.

Here you are, Robert.

I think you will also be able to recognise that there is some superflous text in Chris' original 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.

*** insert >>> For the following it is assumed that "local-2" is understood without its points, which belong to "local-1" <<< insert

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 *** could be deleted, see below >>> has either a
stone on local-1 of the string or it <<< could be deleted, see below *** does not have a stone on local-1
of the string
(2b1) If it has a stone on local-1 of the string, *** delete >>> it is also on
local-2 <<< delete *** *** insert >>> it would be capturable-1, what contradicts the assumption that the string is not capturable-1. So the string cannot have a stone on local-1. <<< insert *** *** (2b1) can be deleted completely !!! ***.
(2b2) *** delete >>> If <<< delete *** *** insert >>> Because <<< insert *** 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 *** delete >>> both (2b1) and <<< delete *** (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

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

Why would it be capturable-1? From the fact that initially a stone of the string is on local-1, it does not (obviously) necessarily follow that, after the string's capture, a new permanent-stone will be on local-1. So your contradiction of the string being both capturable-1 and not capturable-1 is a fake construction. Therefore your guessed simplification would need better justification.

(2b) is a restriction to "not capturable-1".

"capturable-1" is defined as "... the opponent cannot ... force ... no local-1 permanent-stone of the player."

(A) It follows that "capturable-1" is TRUE, if there develops a permanent stone on at least one point of local-1.

(B) It follows that "capturable-1" is FALSE, if there will be no permanent stone on any of the points of local-1.

(2b) is true only if "capturable-1" is FALSE, so there is no room left for (2b1), due to (B).


Better think logical about "logic" before starting to quarrel !

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

Citation from J2003:

"A permanent-stone is a stone that IS PLAYED during a hypothetical-sequence and then not removed during the rest of the hypothetical-sequence."

(2b) says: "It is not capturable-1".

As you describe correctly in informal words, (2b) means:
"there WILL BE [PLAYED] no permanent-stone on any of the points of local-1."

Now compare this to condition (2b1):
"[IN THE FINAL-POSITION,] it [CURRENTLY] HAS a stone on local-1 of the string"

While (2b1) speaks about the present (the initial string in the final-position), (2b) speaks about the future (after the string's capture: a then newly played permanent-stone). (2b1) and (2b) speak about different times!

Therefore the conditions (2b) and (2b1) are NOT mutually exclusive.

So your conclusion "so there is no room left for (2b1)" is false.



Since I think logically, I may quarrel!:) (Socrates would have said more generally: "I think therefore I am.") You still need to learn thinking locally before you may quarrel;)

Sorry, Robert, but you are introducing a type of string, that has no stone on its local-1.

Can you please give an example ?

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

I am not introducing a type of string, that HAS no stone on its local-1. I am explaining that, for a string and its local-1,

AFTER THE STRING'S CAPTURE,

a NEW stone THEN might or might not be on the local-1.

That's correct without doubt.

But if the new stone (permanent of course, otherwise it would make no sense) is on local-1, the string will be called capturable-1, due to the definition of capturable-1.

(2b) determines the string to be NOT capturable-1.

If follows that a string, which is treated within (2b) cannot have a new stone on local-1.

Any condition within (2b) referring to local-1 is senseless, at the same time superfluous.

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

This is not necessarily so!

Click Here To Show Diagram Code

[go]$$B circle = local-1
$$ -------------
$$ |. . . . . . .|
$$ |. . . . . . .|
$$ |. . W . O . .|
$$ |. . X X X . .|
$$ |. . . X . . .|
$$ |. . . X . . .|
$$ |. . . . . . .|
$$ -------------[/go]

Suppose White cannot force a permanent-stone on circle, i.e., the initial string is not capturable-1. Now suppose we are in the analysis of whether the initial string is capturable-2 and White has hypothetically played the two stones. Next Black will cut and suppose that Black cannot capture both stones. (White can force a permanent-stone that is the left white stone, the right white stone or elsewhere in the local-2.) Suppose that Black can capture one of them but that the other will become a permanent-stone. If Black captures the right stone, then the left stone is on the local-1 part of the local-2. If Black captures the left stone, then the right one is not on the local-1 part of the local-2.

I do not know an actual example with that behaviour but the above illustrates the principle possibility.

1989 Nihon Kiin rules example #4.

Obviously you want to follow multiple aims with your J2003 construction, this may be a problem somewhat. But let me try a conclusion:

With my suggestion of using (local-2 without its local-1) in capturable-2, White's strings would be neither capturable-1 nor capturable-2, following your thinking to evaluate the possibility of both statuses independently from another (I would not prefer this kind of thinking, but this would be another topic).

So they would be "dead", what I have ever claimed.

If it is your wish to have both of White's strings capturable-2, I would suggest you to use (local-2 without its local-1) as "local-2" (new version) and to extend the board area used in the formula for capturable-2 by "local-1".

This way it would become clearly visible that this very special area-extension will be necessary in a very few very "exotic" positions only.

_________________
The really most difficult Go problem ever: https://igohatsuyoron120.de/index.htm
Igo Hatsuyōron #120 (really solved by KataGo)

Presumably, thanks.



For J2003, sure.



What do you mean by this?



For typically final positions, pretty likely.