Yes, specifically the ones that come right after our “Bot” and therefore must be accepted by Bot.
This is more apparent if you use the intuitive definition of “good(X)”: “X accepts the chocolate and only accepts good successors”.
I believe that definition doesn’t directly formalize in a conventional setup though because of its coinductive nature, recursing directly into itself. So we ground it out by saying “this recursive property holds for arbitrarily long chains” and that’s where we get the successor-chains definition from. Which should be equivalent.
Perhaps I should clarify what’s going on there better, hope this helps for now.
(Edit: I did try to make this clearer in the post now.)
What are the X’s over which you quantified in the rightmost biconditional? Bots in chains that started with Bot?
Yes, specifically the ones that come right after our “Bot” and therefore must be accepted by Bot.
This is more apparent if you use the intuitive definition of “good(X)”: “X accepts the chocolate and only accepts good successors”.
I believe that definition doesn’t directly formalize in a conventional setup though because of its coinductive nature, recursing directly into itself. So we ground it out by saying “this recursive property holds for arbitrarily long chains” and that’s where we get the successor-chains definition from. Which should be equivalent.
Perhaps I should clarify what’s going on there better, hope this helps for now.
(Edit: I did try to make this clearer in the post now.)