Quantifier Elimination - History

History

In early model theory, quantifier elimination was used to demonstrate that various theories possess certain model-theoretic properties like decidability and completeness. A common technique was to show first that a theory admits elimination of quantifiers and thereafter prove decidability or completeness by considering only the quantifier-free formulas. This technique is used to show that Presburger arithmetic, i.e. the theory of the additive natural numbers, is decidable.

Theories could be decidable yet not admit quantifier elimination. Strictly speaking, the theory of the additive natural numbers did not admit quantifier elimination, but it was an expansion of the additive natural numbers that was shown to be decidable. Whenever a theory in a countable language is decidable, it is possible to extend its language with countably many relations to ensure that it admits quantifier elimination (for example, one can introduce a relation symbol for each formula).

Example: Nullstellensatz in ACF and DCF.

Read more about this topic:  Quantifier Elimination

Famous quotes containing the word history:

    “A man acquainted with history may, in some respect, be said to have lived from the beginning of the world, and to have been making continual additions to his stock of knowledge in every century.”
    —David Hume (1711–1776)

    “The history of mankind interests us only as it exhibits a steady gain of truth and right, in the incessant conflict which it records between the material and the moral nature.”
    —Ralph Waldo Emerson (1803–1882)

    “Literary works cannot be taken over like factories, or literary forms of expression like industrial methods. Realist writing, of which history offers many widely varying examples, is likewise conditioned by the question of how, when and for what class it is made use of.”
    —Bertolt Brecht (1898–1956)