Prequel to Sequel to The nature of proofs

While a proof of some claim A need not be shown in order for it to exist---a "constructive" proof game for A may be inverted to a dual "classical" proof game for not(not(A))---such a game makes sense only if every refutation R₁ of a refutation R₂ of A can convince the adversary that R₂ is indeed invalid. More specifically, the underlying logic cannot be inconsistent; the claim A must be expressed in a logic that does not allow the player to refute not(A) once a correct proof of not(A) is shown by the adversary.