A fundamental problem of symbolic logic is to define logical calculi sufficient to comprise important parts of mathematics, and to develop systematic methods of calculation therein.

The possibility of progress in this direction has been severely limited by Gödel's proof that a consistent system sufficient to comprise arithmetic must contain propositions whose truth-value cannot be decided within the system, and by Church's extension of Gödel's method to the result that even in the first order logical function calculus the general decision problem cannot be solved.

In a previous note I showed a new way to define the ordered pair. I made use of the notations ‘Nn’ (for class of natural numbers) and ‘Sv’ (for successor of v), remarking that they are readily defined without appeal to ordered pairs or relations. Adopting the auxiliary abbreviation:

I defined the ordered pair thus:

In his excellent review of four notes of Skolem on recursive functions of natural numbers Bernays states: “The question whether every relation y = f(x1,…, xn) with a recursive function ƒ is primitive recursive remains undecided.” Actually, the question is easily answered in the negative by a form of the familiar diagonal argument.

We start with the ternary recursive relation R, referred to in the review, such that R(x, y, 0), R(x, y, 1), … is an enumeration of all binary primitive recursive relations.