Abstract

Solving numeric, logic and language puzzles and paradoxes is common within a wide community of high school and university students, fact witnessed by the increasing number of books published by mathematicians such as Martin Gardner, Douglas Hofstadter [in one of the best popular science books on paradoxes ], inspired by Gödel’s incompleteness theorems), Patrick Hughes and George Brecht and Raymond M. Smullyan, inter alia. Books by Smullyan are, however, much more involved, since they introduce learning trajectories and strategies across several subjects of mathematical logic, as difficult as combinatorial logic, computability theory, and proof theory. These books provide solutions to their suggested exercises. Both statements and their solutions are written in the natural language, introducing some informal algorithms. As an exercise in Mathematics we wonder if an easy proof system could be devised to solve the amusing equations proposed by Smullyan in his books. Moreover, university students of logic could well train themselves in constructing deductive systems to solve puzzles instead of a non-uniform treatment one by one. In this paper, addressing students, we introduce one such formal systems, a tableaux approach able to provide the solutions to the puzzles involving either propositional logic, first order logic, or aspect logic. Let the reader amuse herself or himself!