Talk:Quantifier elimination: Difference between revisions
→Alternate Definitions of Quantifier Elimination: new section |
|||
Line 23: | Line 23: | ||
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? <span style="font-size: smaller;" class="autosigned">—Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[Special:Contributions/90.156.82.87|90.156.82.87]] ([[User talk:90.156.82.87|talk]]) 14:10, 12 May 2011 (UTC)</span><!-- Template:UnsignedIP --> <!--Autosigned by SineBot--> |
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? <span style="font-size: smaller;" class="autosigned">—Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[Special:Contributions/90.156.82.87|90.156.82.87]] ([[User talk:90.156.82.87|talk]]) 14:10, 12 May 2011 (UTC)</span><!-- Template:UnsignedIP --> <!--Autosigned by SineBot--> |
||
== Alternate |
== Alternate Definition of Quantifier Elimination == |
||
⚫ | John Doner and Wilfrid Hodges, in their paper "Alfred Tarski and Decidable Theories" ('''Journal of Symbolic Logic''', vol 53, no 1, March 1988, pp 20–35), give a formal definition of "the method of eliminating quantifiers" wherein the ''definiens'' does not require (or even mention) eliminating any quantifiers. See specifically page 24 of Doner and Hodges's paper. |
||
Hmm... Seems to be some difference of opinion as to what counts as "quantifier elimination." |
|||
⚫ | 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) in describing 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" ... even though both of these sentences, on the face of them, employ quantifiers. See specifically pages 293 and 295 of Tarski's paper. |
||
⚫ | |||
Jan Zygmunt, in a paper titled "Alfred Tarski: Auxiliary Notes on His Legacy" in the Birkhäuser volume '''The Lvov-Warsaw School. Past and Present''', 2018, pp 425–455, gives a succinct overview of the method of eliminating quantifiers in the context of decidable and undecidable theories, quoting both the Doner and Hodges paper and the Tarski paper, and also quoting Chang and Keisler on the subject. See specifically pages 440 and 441 of Zygmunt's paper. |
|||
⚫ | |||
⚫ | |||
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. |
|||
⚫ | |||
[[User:Grandmotherfrompeoria|Grandmotherfrompeoria]] ([[User talk:Grandmotherfrompeoria|talk]]) 16:40, 13 August 2021 (UTC) |
[[User:Grandmotherfrompeoria|Grandmotherfrompeoria]] ([[User talk:Grandmotherfrompeoria|talk]]) 16:40, 13 August 2021 (UTC) |
Revision as of 17:20, 14 August 2021
![]() | Mathematics Start‑class Low‑priority | |||||||||
|
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)
- "Quantifier elimination" has far more Google scholar hits, for what that's worth. Algebraist 18:37, 5 September 2008 (UTC)
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)
Formula / Sentence
Changed this over because QE is for all formulae not just sentences.
Note that for any complete theory (in a language with a constant symbol ) we have that every sentence is equivalent mod to either or . Thehalfone (talk) 09:59, 8 February 2009 (UTC)
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)
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)
Alternate Definition of Quantifier Elimination
John Doner and Wilfrid Hodges, in their paper "Alfred Tarski and Decidable Theories" (Journal of Symbolic Logic, vol 53, no 1, March 1988, pp 20–35), give a formal definition of "the method of eliminating quantifiers" wherein the definiens does not require (or even mention) eliminating any quantifiers. See specifically page 24 of Doner and Hodges's paper. 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) in describing 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" ... even though both of these sentences, on the face of them, employ quantifiers. See specifically pages 293 and 295 of Tarski's paper. Jan Zygmunt, in a paper titled "Alfred Tarski: Auxiliary Notes on His Legacy" in the Birkhäuser volume The Lvov-Warsaw School. Past and Present, 2018, pp 425–455, gives a succinct overview of the method of eliminating quantifiers in the context of decidable and undecidable theories, quoting both the Doner and Hodges paper and the Tarski paper, and also quoting Chang and Keisler on the subject. See specifically pages 440 and 441 of Zygmunt's paper. I would suggest that the article should somehow acknowledge this alternative definition of the method of quantifier elimination. Grandmotherfrompeoria (talk) 16:40, 13 August 2021 (UTC)