Strategy-stealing Argument - Constructivity

Constructivity

The argument shows that the second player cannot win, by means of deriving a contradiction from any purported winning strategy for second player. According to the BHK interpretation, the most widely used basis for constructive interpretation of logical formulae, this is constructive.

The argument is commonly employed in games where there can be no draw to show that first player has a winning strategy, such as in Hex. This application of the argument is usually non-constructive, where the inference from the absence of a strategy and the impossibility of a draw is made by means of the law of the excluded middle. For finite games, and games where the appropriate instance of Markov's rule can be constructively established by means of bar induction, then the non-constructive proof of a winning strategy for the first player can be converted into a winning strategy.