 Clerbout (2014a) showed that tableaux for classical logic (Smullyan 1968) are sound and complete for classical dialogical games as defined in  Section 2.2.1,  i.e., with repetition ranks. By soundness and completeness of the tableau method with respect to model-theoretic semantics, it follows that existence of a winning P strategy coincides with validity: There is a winning P strategy in the game for \(\varphi\) if and only if \(\varphi\) is valid.