Relative model‐completeness and the elimination of quantifiers1

Dialectica 12 (3‐4):394-407 (1958)
  Copy   BIBTEX

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.ZusammenfassungDie 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.SommaireBeaucoup 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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

T-Convexity and Tame Extensions.Dries Lou Van Den & H. Lewenberg Adam - 1995 - Journal of Symbolic Logic 60 (1):74 - 102.
T-convexity and Tame extensions.LouDen Dries & Adam H. Lewenberg - 1995 - Journal of Symbolic Logic 60 (1):74 - 102.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Dynamic non-commutative logic.Norihiro Kamide - 2010 - Journal of Logic, Language and Information 19 (1):33-51.
Proof normalization modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
A Hierarchy of Weak Double Negations.Norihiro Kamide - 2013 - Studia Logica 101 (6):1277-1297.

Analytics

Added to PP
2013-11-21

Downloads
14 (#846,545)

6 months
3 (#445,838)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Alfred Tarski and decidable theories.John Doner & Wilfrid Hodges - 1988 - Journal of Symbolic Logic 53 (1):20-35.

Add more citations

References found in this work

No references found.

Add more references