The following is intended for people who are experts in the field and is not essential to the game.

Before talking about the correctness of the game, let's start with a clarification: when, for example, the knight says "The path continues by not pressing A", a priori also not pressing any key is a correct action. In the game there is a tacit agreement that it is obligatory to press A or B (i.e. aut) at every turn.

The more technical issue is about the sentences in which appears another condition like "if X then Y else Z". Because of what we said before, Z is always of type ¬Y. This makes saying "if X then Y else Z" equivalent to saying "X iff Y", i.e. X ↔ Y. Now let K be a character variable (more precisely, K indicates that the speaker is a knight) and let P be any statement. If a character asserts P it is always verified K ↔ P. Specifically, in the game, P = X ↔ Y. Thus, we have that every turn in the game can be rewritten as K ↔ (X ↔ Y). So if K is unverified, i.e., the speaker is a knave, then X ↔ Y must also be false, i.e., the truth values of X and Y must be different. If, on the other hand, the speaker is a knight, then K is verified and thus the truth values of X and Y must coincide. In order to deepen the discussion and tend to Godel's theorems, we recommend reading the book Forever Undecided by Raymond Smyullyan (Knopf, 1987).