Talk:Quantifier elimination

Mathematics Start‑class Low‑priority

	Mathematics portal This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
Start	This article has been rated as Start-class on Wikipedia's content assessment scale.
Low	This article has been rated as Low-priority on the project's priority scale.

Template:Vital article

Proposed move

What would people think of moving this title to "elimination of quantifiers", which now redirects to this page? Michael Hardy 18:59, 13 July 2007 (UTC)[reply]

"Quantifier elimination" has far more Google scholar hits, for what that's worth. Algebraist 18:37, 5 September 2008 (UTC)[reply]

The phrase "quantifier elimination is what I use and find used. I have some lecture notes on quantifier elimination here, which may be useful:

 http://lara.epfl.ch/dokuwiki/sav09:lecture_09

Vkuncak (talk) 15:53, 21 June 2009 (UTC)[reply]

Formula / Sentence

Changed this over because QE is for all formulae not just sentences.

Note that for any complete theory $T$ (in a language with a constant symbol $a$ ) we have that every sentence is equivalent mod $T$ to either $a=a$ or $\lnot (a=a)$ . Thehalfone (talk) 09:59, 8 February 2009 (UTC)[reply]

Skolemization and Herbrandization

I think that Skolemization and Herbrandization should be mentioned or at least linked to. —Preceding unsigned comment added by 90.156.82.87 (talk) 10:07, 6 May 2011 (UTC)[reply]

ETA: Perhaps a mention that Skolemization and Herbrandization are really a different thing as they are concerned with logics whereas quantifier elimination is concerned with models? —Preceding unsigned comment added by 90.156.82.87 (talk) 14:10, 12 May 2011 (UTC)[reply]

Alternate Definitions of Quantifier Elimination

Hmm... Seems to be some difference of opinion as to what counts as "quantifier elimination." Doner and Hodges, for example, in their paper "Alfred Tarski and Decidable Theories" (JSL, vol 53, no 1, March 1988, pp 20–35), imply that the method does not necessarily involve actually eliminating any quantifiers. And Tarski himself, in his paper "Grundzüge des Systemenkalküls. Zweiter Teil" (Fundamenta Mathematicae, vol 26, 1936, pp 283–301), uses the phrase "sukzessiven Elimination der Operatoren" (successive elimination of quantifiers) on pages 293 and 295 to describe his proof that every sentence in the elementary theory of dense order is deductively equivalent to a Boolean combination of the two sentences: "There is no first element" and "There is no last element"... both of which sentences, on the face of them, employ quantifiers. See also Jan Zygmunt's paper "Alfred Tarski: Auxiliary Notes on His Legacy" in the Birkhäuser volume "The Lvov-Warsaw School. Past and Present", 2018, pp 425–455. In particular see pages 440 and 441 of this paper. I would suggest that the article somehow acknowledge this difference of opinion. Grandmotherfrompeoria (talk) 16:40, 13 August 2021 (UTC)[reply]