My article Formalization of two Puzzles Involving Knowledge http://www-formal.stanford.edu/jmc/puzzles.html covers both the wise man puzzle and Mr S and Mr P. The point of the article is to express the puzzles in first order logic and push an interactive theorem prover to their solutions. There is a variant of the wise men puzzle called the puzzle of the 40 unfaithful wives in Baghdad. There is obviously a solution beginning "if my wife were faithful there would be only 39 unfaithful wives and each of the husbands would have reasoned ...". However, Arabs, at least before the Mongols wiped out Baghdad in 1258 were capable of mathematical induction. I don't have and would like to see a formalization in which the Arabs use mathematical induction. A judicious use of the word "etc." should do it.