A Method in Proofs of Undefinability
Karel Louis de Bouvère

Abstract:
This study is a sample of a semantic method in the theory of definition. Already in 1900 A. Padoa proposed a semantic method in proofs of undefinability. G. Peano was the first to recognize the value of this method, followed by A. Tarski, A. Lindenbaum, J. C. C. McKinsey and others. A new step was made by E. W. Beth in 1953, when he showed that Padoa’s method is a general method, in other words, that whenever (under certain conditions) a non-logical constant is undefinable explicitly with respect to a theory from the other non-logical constants occurring in this theory, there is a way to prove this fact by Padoa’s method. At the same time this was a first application of logical methods related to G. Gentzen’s formalization to a problem in the theory of models.
In this work the concept of explicit definability is characterized in terms of models. Both Padoa’s method and Beth’s theorem appear to be tools for this characterization. The study is confined to theories with standard formalization, but the results could be extended. The characterization in terms of models entails a new method in proofs of explicit undefinability which seems to have certain advantages over Padoa’s method. A distinction is made between explicit undefinability and essential explicit undefinability. The latter term means that a certain non-logical constant is undefinable explicitly from certain other non-logical constants not only with respect to the theory in question, but also with respect to every consistent extension of this theory. Under certain conditions the method developed in this study enables us to state that a given non-logical constant is essentially undefinable explicitly from the other non-logical constants occurring with respect to a certain, say finitely axiomatizable, subtheory of the theory concerned. This implies that the same non-logical constant is undefinable explicitly from the same other non-logical constants with respect to the theory itself. For example, the method enables us to state that multiplication is essentially undefinable explicitly from addition and unity with respect to a finitely axiomatizable sub-theory of the formalized arithmetic of natural numbers. It follows that multiplication is undefinable explicitly from unity and addition with respect to the formalized arithmetic of natural numbers. This fact was well-known for indirect reasons: the theory with multiplication is undecidable, whereas the theory with only unity and addition is decidable. But the method provides us with a direct proof of this fact, at the same time suggesting its own usefulness.
A further distinction is made between explicit definability and equational definability of operation constants. The latter term points to a definition by means of equality. It is known by a result of K. Gödel that e.g. the higher functions in the sequence of W. Ackermann are arithmetical, i.e. definable explicitly and validly from addition and multiplication with respect to the formalized arithmetic of natural numbers. At the same time they are undefinable equationally from the lower ones in the sequence with respect to the same theory. Application of the method developed in this study to show the explicit undefinability of these functions with respect to certain subtheories of the formalized arithmetic of natural numbers embodies a method to show their equational undefinability with respect to the complete theory of the formalized arithmetic of natural numbers.
It is the author’s conviction that the suggestions made in this study are not more than a start for further investigations.