Kalmar's proof of the undecidability of first-order predicate logic

We analyse in detail László Kálmár’s little known, yet very interesting and elegant proof (1956) of the recursive undecidability of the satisfiability problem for first- order predicate logic. As is well known, Church and Turing independently provided in 1936 the negative answer to Hilbert’s Entscheidungsproblem. The proof strategy they employed (and other scholars, later, as well) is indirect, by reduction: it is shown that a positive solution to the problem would entail the decidability of another specific problem that has been previously proved to be undecidable. Kálmár proof is, on the contrary, direct.