As written in my answer to your next posting, "local" has other characteristics as "capturable".

Local is the primary parameter, capturable only a deduced one.

Both tables refer to "local", not to "capturable", what is a tiny, but very decisive difference.

X = (The player cannot force a local-1 permanent stone) AND (The player cannot force a local-2\1 permanent stone)
X = NOT (The player can force a local-1 permanent stone) AND NOT (The player can force a local-2\1 stone)
X = NOT (the player can force) ((a local-1 permanent stone) OR (a local 2\1 permanent stone))
X = NOT (the player can force) (a (local-1 OR local-2\1) permanent stone))
X = NOT (the player can force) (a local-2 permanent stone)
X = The player cannot force a local-2 permanent stone

Works in either direction.

(edited due to a mistake in the primary sentences)

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

As usual, context is missing so that I cannot understand what you write here.



In J2003-context's local-2, such an implication is wrong: Example 0000 proves this as a counter-example: The tengen stone is not capturable-1, is not capturable-2\1 but is capturable-2.

Maybe you mean a different context? In that case, please state it!



As long as you do not explain your tables well, I can either simply ignore them entirely or tell you what I see in them. And what I see is the mistake because I expected J2003-context.



Since Chris's proof is not about local-2\1, you should state the entire context for your tables explicitly.

How do you prove this step in direction "=>"?

If you refer to capturable-2\1 as there is established a permanent stone in local-2\1, the Tengen stone in your #0000 is as capturable-2\1 as it is capturable-2.

The Tengen stone is turned into an eye point, so the additional player's stones can only be in local-2\1, because local-1 is now the eye point.

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

Thank for the hint, did not work in either direction.
I had not recognised that AND combines two negative clauses in sentence 1.

Have corrected my posting.

Now the sentences are:

X = (The player cannot force a local-1 permanent stone) AND (The player cannot force a local-2\1 permanent stone)
X = NOT (The player can force a local-1 permanent stone) AND NOT (The player can force a local-2\1 permanent stone)
X = NOT (the player can force) ((a local-1 permanent stone) OR (a local 2\1 permanent stone))
X = NOT (the player can force) (a (local-1 OR local-2\1) permanent stone))
X = NOT (the player can force) (a local-2 permanent stone)
X = The player cannot force a local-2 permanent stone

What you are looking for are the two sentences in bold.

local-2\1 = local-2 AND NOT local-1
local-2\1 OR local-1 = (local-2 AND NOT local-1) OR local-1
local-2\1 OR local-1 = (local-2 OR local-1) AND (NOT local-1 OR local-1)
local-2\1 OR local-1 = local-2 AND TRUE
local-2\1 OR local-1 = local-2

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

I'll edit Chris' proof (the second part only, which we are discussing here) later - may be tomorrow -, making the reference to local-1 and local-2\1 clearly visible.

It will be just the contents of the table in prose.

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

Oops, you are right about Example 0000!

Great!



We'll see:)

I do not buy this fake proof by overlooking "force" everywhere. What you really need to do is to apply the definition of force and study what you get then: hypothetical-sequences of hypothetical-strategies. (Before you do that, you better retransform to J2003-style-double-negation.) I have not checked whether you need to do it for every transformations (maybe you use some purely logic operational ones); the bold step requires precision for sure though.

If all this is "user-friendly", can you tell me which user it is supposed to be friendly to?

Best wishes.

_________________
No aji, keshi, kifu or kikashi has been harmed in the compiling of this post.
http://www.gogod.co.uk

If one wants to have a "user-friendly" formulated rule set (consistent and as easy to be understood as possible), it is mandatory to have analysed, in which aspects (e.g. handling of some examples of another rule set) it might differ from the other rule set or other rule sets.

The discussions about this analysis are supposed to be not "user-friendly". This goes without saying, because the aim is not identical.

Some topics that must be discussed cannot be "user-friendly" from the very beginning, because they are related to some "1-in-a-million" or "1-in-a-billion" positions. Robert will have numbers that are more well-founded.

Compared to previous discussions with Robert, I estimate this one as factual and goal-oriented. Robert had been busy several years to develop his rule sets and his view on rule sets. So it will not be trivial to make another kind of view understandable, which is not aimed to torpedo his work, but to give some help by enlighten the szene from a different standpoint. May be that some details come to sight now, which had been hidden in the shadow for long.

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

Here it is:
***RED*** = deleted
BLUE = inserted
---(BLUE ITALIC)--- = comment


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.

...

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*** The opponent can either force capture of the string or not. ---(This is what I mean with "primary")---

(1) ***The string is uncapturable*** The opponent cannot force capture of the string -> It is uncapturable. ---(This is what I mean with "secondary", the J2003-term follows from a "neutral" clause)--- -> It is J2003-alive

(2) ***It is not uncapturable -> The string is either capturable-1 or not capturable-1*** The opponent can force capture of the string. -> The opponent can force either no permanent stone on local-1 or not.

(2a) ***It is capturable-1*** The opponent cannot force no permanent stone on local-1 -> the string is capturable-1 -> It is J2003-alive

(2b) ***It is not capturable-1*** The opponent can force no permanent stone on local-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 ---(this follows from the first sentence of (2b)-new)---

***(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*** ---(superfluous now)--- 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 intersection these adjacent intersections where empty or occupied by opposing stones. Hence, these intersections belong to local-2\1 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\1 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\1. Hence, the opponent cannot force ***both caputre 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.



The table uses "two-eye-formation" as parameter, in Chris' proof this is a precondition. For the sake of comparision you can restrict yourself to the columns with "two-eye-formation" = "Y".

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

Tmark, if you refer to the thread's initial rules text: If you do not understand something, please ask! If you wonder whether J1989 style rules could be user-friendly at all, then the simple answer is "no". If you wonder whether any Japanese style rules could be... - but that is another topic.

If refer to the maths discussion between Cassandra and myself, then the answer is: It is readable but not user-friendly for maths-freaks spending at least an hour per theory message. The contents is mostly preliminary studies for potential research. Afterwards comes research (we hope) and yet later its results might then be translated to something user-friendly. E.g., a likely later result might be: "There is more than one model for an equivalence between life defined via two-eye-formation and life defined via capturability. Different models create differences only in arcane, rare positions."

Before I read your edited proof draft text more carefully, I need this information:

Which conjecture do you want to prove?! Please write it down carefully!

***

With primary you mean source text while with secondary you mean terms (words) defined as substituting abbreviations for the source text?

"If a string is two-eye-alive, it follows that it is J2003-alive.". That's the topic of part II of Chris' proof.

Preconditions are as in the original proof, additionally there is the definition of local-2\1 (local-2, but not local-1) and a deducted capturable-2\1 (... in local-2\1).



Yes, something like that.

Using (may be first) the "primary" text helps preventing to overlook some implications, what might be possible when using "secondary" terms and taking some properties of this term for "self-evident" or loosing them off sight.

An example:

Please refer to the part of Chris' proof, which is connected to your #0000.

Concerning local-2, the only really essential aspect is this one empty board point direct adjacent to the string.

Independent from the definition of any type of local-2xxx, this one empty point is part of local-2xxx, as long as the definition does not contain more that the following three elements:

• Optional: include the string itself.
• Recursively, include all board points adjacent to the string, which are empty or are not occupied by strings with a special property B.

The empty points direct adjacent to the string are never affected by a string's property B.

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

After over 130 posts, and the several years that Robert has spent (seems more like millenia to observers), I would have expected greater progress. Or is it beyond your capabilities?

Best wishes.

_________________
No aji, keshi, kifu or kikashi has been harmed in the compiling of this post.
http://www.gogod.co.uk

Do you mean "J2003-alive (original)" or "like J2003-alive but based on local-2\1 and capturable-2\1 instead of local-2 and capturable-2"?

Cassandra's? His restricted maths capabilities play some role, although he always tries hard. Chris's proof is a hard nut in itself. It is unknown whether another conjecture can be proven or would turn out to be false. Under such circumstances, maths itself can be difficult. That examples that might serve as counter-examples are all rather arcane and difficult does not make things easier either. OTOH, like me, Cassandra always attacks the hardest nuts: He wants to solve Igo Hatsu Yoron #120... Life is more interesting if one tries to solve the difficult problems! :)

I refer to J2003-alive as defined in your original text in WAGCmod.

Local-2\1 could be seen as shortcut for "local-2, but not local-1", aiming to give a more detailled description for the area, in which the permanent stone(s) in your #0000 will turn up.

If you have in mind a relationship to J2003-alive (original) only, "capturable-2\1" is not necessary in the proof's text.

The (additional) usage of local-2\1 (and capturable-2\1) could make apparent (if wished) that the proof would remain true with a somewhat more restricted definition of one area-type. Or be independent of the definition of "local-2xxx", as long as the usage of "local-2" in the compound-term secures to keep the main original characteristics of J2003-local-2 (original). In this case, please refer to my posting above, it is of no interest and does not matter at all, how far "local-2xxx" goes on the board.

In my opinion it will help avoiding some misunderstandings (I think, we had several of this type), when there will be made clear that it's only one (or a few) of several properties of a term, that is really uses and / or needed, e.g. in a proof. This does not mean that all the other properties are superfluous, instead they support other aims.

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

I do not read the rest of your proof change attempt yet. Let me comment on the cited part.

First I need to say something about your English. In maths, careful English is essential. So I correct samples (not as precise as J2003 but precise enough for your purpose):

"The opponent can either force capture of the string or not."
->
"Either the opponent can force capture of the player's string or the opponent cannot force capture of the player's string."

"The opponent can force no permanent stone on local-1"
->
"The opponent can - with the same hypothetical-strategy - force both capture of the string's stones and no local-1 permanent-stone of the player."

Your other inserted texts need the same precision.

Now to the contents:

You write:



With precise English, this should be:



Here you make an oversight that leads to a mistake.

The hypothetical-strategy used by the opponent for "can force both capture of the string's stones and no local-1 permanent-stone of the player" is not necessarily the same hypothetical-strategy H we assume for "the string is two-eye-alive".

Therefore your further deletions in (2b), (2b1), (2b2) for the intention of simplification may not be made.

Your proof rewriting goes to the next round.