Decidable Pairing Functions
In Chapter I of this paper we show that the usual, textbook pairing functions have decidable first-order theories. This will be done by exhibiting an infinite axiomatization of certain pairing functions which we characterize as ``acyclic except for $\triangle$''. This condition is satisfied by the usual pairing functions. We then use a technique of Ehrenfeucht and Fraisse to show that the decision problem for such a pairing function is effectively reduced to the decision problem for the function restricted to $\triangle$. In contrast to the decidability of the first-order theories of certain pairing functions, we show that the weak second-order and monadic second-order theories of these pairing functions are undecidable. In Chapter II we show how to extend the first-order Ehrenfeucht game to a second-order game. Using this extended game, we show that the monadic second-order theory of an equivalence relation is decidable. Some of the results of Chapter I were announced in [16].