RELATIVE MODEL‐COMPLETENESS AND THE ELIMINATION OF QUANTIFIERS

Abstract

Most of the early proofs of the decidability or completeness of certain mathematical theories were based on the method of eliminations of quantifiers. Various more recent results on completeness were obtained independently of such procedures. However, it is shown in the present paper that, conversely, the completeness of a mathematical theory will in certain circumstances entail the existence of an elimination method. The proof involves the application of the extended first ε‐theorem of Hilbert‐Bernays. Die meisten früheren Beweise der Vollständigkeit oder Entscheidbarkeit gewisser mathematischer Theorien benutzten die sogenannte Quantoren‐eliminierungsmethode. Dagegen sind einige neuere Ergebnisse über Voll‐ständigkeit unabhängig von diesem Verfahren. Es ist deshalb von Interesse festzustellen, dass umgekehrt die Vollständigkeit einer mathematischen Theorie unter Umständen die Existenz einer Eliminierungsmethode fürdiese Theorie nach sich zieht. Der Beweis benutzt das erweiterte erste ε‐Theorem von Hilbert‐Bernays. Beaucoup de démonstrations concernant la complétude de certaines théories mathématiques, ou concernant l'existence d'un procédé de décision pour une telle théorie, sont basées sur des méthodes d'élimination de quantificateurs. Or, il y a des résultats plus récents sur la complétude de certaines théories qui ne dépendent pas de telles méthodes d'élimination. Toutefois on démontre ici que la complétude d'une théorie mathématique entraîne sous certaines conditions l'existence d'une méthode d'élimination. Au cours de la démonstration on se sert d'un des théorèmes‐ε de Hilbert‐Bernays. Copyright © 1958, Wiley Blackwell. All rights reserved