… kann man das Rätsel formalisieren ? Evtl. unter Verwendung
mehrwertiger und/oder Modallogiken ?
Tja, woher soll ich das wissen? 
Ich denke, das eigentlich Besondere an diesen Rätseln ist, daß hier nach Fragen gefragt wird („Welche Fragen muß man stellen, um den richtigen Weg rauszubekommen?“). Wenn es darum geht, irgendwelche Zahlen nach irgendwelchen Quersummen-Vorgaben oder ähnliches auszutüfteln, dann ist es wohl nicht besonders schwer, dazu einen entsprechenden Algorithmus aufzustellen. Ob das bei den Wächter-Rätseln auch so einfach geht, oder aber nicht, wüßte ich selbst gerne. Ist die Menge aller möglichen Fragen endlich oder wenigstens abzählbar? Wenn ja, wie könnte man sie abzählen? Ich habe keine Ahnung (wenn ich müßte, würde ich auf „nicht abzählbar“ tippen).
Die Motivation wäre dabei
weniger die Formalisierung zum Lösen einzusetzen, als das
solche Rätsel in einen geeigneten Formalismus eine nette
syntaktische Ähnlichkeit aufweisen - man also ggf. neue noch
„spacigere“ Rätsel bauen könnte.
Klar. Ich hab auch mal über eine Verallgmeinerung des Rätsels in der Form „l Lügner, m Wahrheitsliebende, n Ja-Nein-Sager“ nachgedacht, mich aber nicht imstande gesehen, zu einer Erkenntnis zu gelangen. So ist es dann leider beim Nachdenken geblieben 
.
Gruß
Martin