Why is quantifier elimination desirable for a given theory?












6












$begingroup$


We say that a given theory $T$ admits QE in a language $mathcal{L}$ if for every $mathcal{L}$-formula, there is an equivalent quantifier free $mathcal{L}$-formula. That is for every $mathcal{L}$-formula $phi(x)$, where $x$ is a free variable, there is an $mathcal{L}$-formula $psi(x)$ so that $TvDashforall xleft(phi(x)iffpsi(x)right)$.



The way I interpret this is that for any formula which $T$ implies, there is an equivalent q-free formula which $T$ imples. In other words, all the logical consequences of $T$ are expressible q-free.



My question is then:




Why is this advantageous? What is the benefit of having every logical consequence of a theory being q-free expressible?




Wikipedia says something along the lines that admitting QE makes the decidability problem simpler. But doesn't every theory admit QE in a sufficienctly complex language? Why is it desirable to be decidable with respect to a small (simpler) language?










share|cite|improve this question











$endgroup$












  • $begingroup$
    Isn't it the case that QE is frequently the most obvious way to prove that some nice first-order theory is decidable? Not every decidable theory has QE, but many do. Even so, note that there may be no practical decider. For instance, Wikipedia says Presburger arithmetic requires at least doubly-exponential time to decide.
    $endgroup$
    – user21820
    Mar 30 at 16:46
















6












$begingroup$


We say that a given theory $T$ admits QE in a language $mathcal{L}$ if for every $mathcal{L}$-formula, there is an equivalent quantifier free $mathcal{L}$-formula. That is for every $mathcal{L}$-formula $phi(x)$, where $x$ is a free variable, there is an $mathcal{L}$-formula $psi(x)$ so that $TvDashforall xleft(phi(x)iffpsi(x)right)$.



The way I interpret this is that for any formula which $T$ implies, there is an equivalent q-free formula which $T$ imples. In other words, all the logical consequences of $T$ are expressible q-free.



My question is then:




Why is this advantageous? What is the benefit of having every logical consequence of a theory being q-free expressible?




Wikipedia says something along the lines that admitting QE makes the decidability problem simpler. But doesn't every theory admit QE in a sufficienctly complex language? Why is it desirable to be decidable with respect to a small (simpler) language?










share|cite|improve this question











$endgroup$












  • $begingroup$
    Isn't it the case that QE is frequently the most obvious way to prove that some nice first-order theory is decidable? Not every decidable theory has QE, but many do. Even so, note that there may be no practical decider. For instance, Wikipedia says Presburger arithmetic requires at least doubly-exponential time to decide.
    $endgroup$
    – user21820
    Mar 30 at 16:46














6












6








6





$begingroup$


We say that a given theory $T$ admits QE in a language $mathcal{L}$ if for every $mathcal{L}$-formula, there is an equivalent quantifier free $mathcal{L}$-formula. That is for every $mathcal{L}$-formula $phi(x)$, where $x$ is a free variable, there is an $mathcal{L}$-formula $psi(x)$ so that $TvDashforall xleft(phi(x)iffpsi(x)right)$.



The way I interpret this is that for any formula which $T$ implies, there is an equivalent q-free formula which $T$ imples. In other words, all the logical consequences of $T$ are expressible q-free.



My question is then:




Why is this advantageous? What is the benefit of having every logical consequence of a theory being q-free expressible?




Wikipedia says something along the lines that admitting QE makes the decidability problem simpler. But doesn't every theory admit QE in a sufficienctly complex language? Why is it desirable to be decidable with respect to a small (simpler) language?










share|cite|improve this question











$endgroup$




We say that a given theory $T$ admits QE in a language $mathcal{L}$ if for every $mathcal{L}$-formula, there is an equivalent quantifier free $mathcal{L}$-formula. That is for every $mathcal{L}$-formula $phi(x)$, where $x$ is a free variable, there is an $mathcal{L}$-formula $psi(x)$ so that $TvDashforall xleft(phi(x)iffpsi(x)right)$.



The way I interpret this is that for any formula which $T$ implies, there is an equivalent q-free formula which $T$ imples. In other words, all the logical consequences of $T$ are expressible q-free.



My question is then:




Why is this advantageous? What is the benefit of having every logical consequence of a theory being q-free expressible?




Wikipedia says something along the lines that admitting QE makes the decidability problem simpler. But doesn't every theory admit QE in a sufficienctly complex language? Why is it desirable to be decidable with respect to a small (simpler) language?







first-order-logic predicate-logic model-theory quantifiers quantifier-elimination






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited Mar 30 at 15:51









Rodrigo de Azevedo

13.1k41960




13.1k41960










asked Mar 30 at 15:26









quanticboltquanticbolt

826514




826514












  • $begingroup$
    Isn't it the case that QE is frequently the most obvious way to prove that some nice first-order theory is decidable? Not every decidable theory has QE, but many do. Even so, note that there may be no practical decider. For instance, Wikipedia says Presburger arithmetic requires at least doubly-exponential time to decide.
    $endgroup$
    – user21820
    Mar 30 at 16:46


















  • $begingroup$
    Isn't it the case that QE is frequently the most obvious way to prove that some nice first-order theory is decidable? Not every decidable theory has QE, but many do. Even so, note that there may be no practical decider. For instance, Wikipedia says Presburger arithmetic requires at least doubly-exponential time to decide.
    $endgroup$
    – user21820
    Mar 30 at 16:46
















$begingroup$
Isn't it the case that QE is frequently the most obvious way to prove that some nice first-order theory is decidable? Not every decidable theory has QE, but many do. Even so, note that there may be no practical decider. For instance, Wikipedia says Presburger arithmetic requires at least doubly-exponential time to decide.
$endgroup$
– user21820
Mar 30 at 16:46




$begingroup$
Isn't it the case that QE is frequently the most obvious way to prove that some nice first-order theory is decidable? Not every decidable theory has QE, but many do. Even so, note that there may be no practical decider. For instance, Wikipedia says Presburger arithmetic requires at least doubly-exponential time to decide.
$endgroup$
– user21820
Mar 30 at 16:46










2 Answers
2






active

oldest

votes


















8












$begingroup$

You're quite right that we can "shoehorn in" quantifier elimination to any theory we want, by adding new predicates for all old formulas (this is called Morleyization if I recall correctly). So considered in a vacuum, there's nothing particularly special about quantifier elimination.



Quantifier elimination is useful in the context of theories whose quantifier-free fragments already have nice properties - that is, it forms half of an argument, with the other half being the analysis of the quantifier-free fragment of the theory in question to begin with. For a good example of this, look at the model-theoretic proof of the Nullstellensatz: quantifier elimination on its own doesn't do anything, but in combination with what we already know (e.g. per the fundamental theorem of algebra) about quantifier-free formulas in algebraically closed fields it gives us something nontrivial.






share|cite|improve this answer









$endgroup$





















    6












    $begingroup$

    I'm going to write this answer from a model theoretic perspective and focus a bit more on why forcing quantifier elimination via Morleyization may not aid our understanding of the theory in question.



    Given a particular theory $T$, one of the key steps in understanding $T$ is to understand the definable subsets of $T$. Having quantifier elimination in this context is extremely useful. Instead of looking at extremely complicated formulas you simply look at quantifier free formulas.



    For example the theory of the random graph (in the language $L={E}$) has quantifier elimination. So instead of attempting to understand an extremely complicated formula $varphi(overline{x})$, say a formula with a billion alternation of quantifiers, we can replace it with a quantifier free formula, which in this case simply ends up describing some finite graph. So checking to see if $varphi(overline{x})$ is satisfied by the tuple $overline{a}$ from a model $M$ of the random graph simply boils down to checking whether $overline{a}$ has the proper graph structure, essentially ignoring the billion quantifiers.



    This example also leads nicely in to your question about forcing quantifier elimination via Morleyization. It can be done. But the quantifier free formulas obtained this way may not have a nice representation that aids in our understanding of the theory. For example, if we carry out Morleyzation for the theory here we obtain that there is some new relation symbol $R_{varphi}((overline{x}))$ such that for any tuple $overline{a}$ from a model $M$ of the random graph $Mmodelsvarphi(overline{a})$, if and only if $Mmodels R_{varphi}overline{a}$. This doesn't really increase our understanding of how $varphi$ behaves or how to evaluate it.






    share|cite|improve this answer









    $endgroup$














      Your Answer





      StackExchange.ifUsing("editor", function () {
      return StackExchange.using("mathjaxEditing", function () {
      StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
      StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
      });
      });
      }, "mathjax-editing");

      StackExchange.ready(function() {
      var channelOptions = {
      tags: "".split(" "),
      id: "69"
      };
      initTagRenderer("".split(" "), "".split(" "), channelOptions);

      StackExchange.using("externalEditor", function() {
      // Have to fire editor after snippets, if snippets enabled
      if (StackExchange.settings.snippets.snippetsEnabled) {
      StackExchange.using("snippets", function() {
      createEditor();
      });
      }
      else {
      createEditor();
      }
      });

      function createEditor() {
      StackExchange.prepareEditor({
      heartbeatType: 'answer',
      autoActivateHeartbeat: false,
      convertImagesToLinks: true,
      noModals: true,
      showLowRepImageUploadWarning: true,
      reputationToPostImages: 10,
      bindNavPrevention: true,
      postfix: "",
      imageUploader: {
      brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
      contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
      allowUrls: true
      },
      noCode: true, onDemand: true,
      discardSelector: ".discard-answer"
      ,immediatelyShowMarkdownHelp:true
      });


      }
      });














      draft saved

      draft discarded


















      StackExchange.ready(
      function () {
      StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3168402%2fwhy-is-quantifier-elimination-desirable-for-a-given-theory%23new-answer', 'question_page');
      }
      );

      Post as a guest















      Required, but never shown

























      2 Answers
      2






      active

      oldest

      votes








      2 Answers
      2






      active

      oldest

      votes









      active

      oldest

      votes






      active

      oldest

      votes









      8












      $begingroup$

      You're quite right that we can "shoehorn in" quantifier elimination to any theory we want, by adding new predicates for all old formulas (this is called Morleyization if I recall correctly). So considered in a vacuum, there's nothing particularly special about quantifier elimination.



      Quantifier elimination is useful in the context of theories whose quantifier-free fragments already have nice properties - that is, it forms half of an argument, with the other half being the analysis of the quantifier-free fragment of the theory in question to begin with. For a good example of this, look at the model-theoretic proof of the Nullstellensatz: quantifier elimination on its own doesn't do anything, but in combination with what we already know (e.g. per the fundamental theorem of algebra) about quantifier-free formulas in algebraically closed fields it gives us something nontrivial.






      share|cite|improve this answer









      $endgroup$


















        8












        $begingroup$

        You're quite right that we can "shoehorn in" quantifier elimination to any theory we want, by adding new predicates for all old formulas (this is called Morleyization if I recall correctly). So considered in a vacuum, there's nothing particularly special about quantifier elimination.



        Quantifier elimination is useful in the context of theories whose quantifier-free fragments already have nice properties - that is, it forms half of an argument, with the other half being the analysis of the quantifier-free fragment of the theory in question to begin with. For a good example of this, look at the model-theoretic proof of the Nullstellensatz: quantifier elimination on its own doesn't do anything, but in combination with what we already know (e.g. per the fundamental theorem of algebra) about quantifier-free formulas in algebraically closed fields it gives us something nontrivial.






        share|cite|improve this answer









        $endgroup$
















          8












          8








          8





          $begingroup$

          You're quite right that we can "shoehorn in" quantifier elimination to any theory we want, by adding new predicates for all old formulas (this is called Morleyization if I recall correctly). So considered in a vacuum, there's nothing particularly special about quantifier elimination.



          Quantifier elimination is useful in the context of theories whose quantifier-free fragments already have nice properties - that is, it forms half of an argument, with the other half being the analysis of the quantifier-free fragment of the theory in question to begin with. For a good example of this, look at the model-theoretic proof of the Nullstellensatz: quantifier elimination on its own doesn't do anything, but in combination with what we already know (e.g. per the fundamental theorem of algebra) about quantifier-free formulas in algebraically closed fields it gives us something nontrivial.






          share|cite|improve this answer









          $endgroup$



          You're quite right that we can "shoehorn in" quantifier elimination to any theory we want, by adding new predicates for all old formulas (this is called Morleyization if I recall correctly). So considered in a vacuum, there's nothing particularly special about quantifier elimination.



          Quantifier elimination is useful in the context of theories whose quantifier-free fragments already have nice properties - that is, it forms half of an argument, with the other half being the analysis of the quantifier-free fragment of the theory in question to begin with. For a good example of this, look at the model-theoretic proof of the Nullstellensatz: quantifier elimination on its own doesn't do anything, but in combination with what we already know (e.g. per the fundamental theorem of algebra) about quantifier-free formulas in algebraically closed fields it gives us something nontrivial.







          share|cite|improve this answer












          share|cite|improve this answer



          share|cite|improve this answer










          answered Mar 30 at 15:48









          Noah SchweberNoah Schweber

          128k10152294




          128k10152294























              6












              $begingroup$

              I'm going to write this answer from a model theoretic perspective and focus a bit more on why forcing quantifier elimination via Morleyization may not aid our understanding of the theory in question.



              Given a particular theory $T$, one of the key steps in understanding $T$ is to understand the definable subsets of $T$. Having quantifier elimination in this context is extremely useful. Instead of looking at extremely complicated formulas you simply look at quantifier free formulas.



              For example the theory of the random graph (in the language $L={E}$) has quantifier elimination. So instead of attempting to understand an extremely complicated formula $varphi(overline{x})$, say a formula with a billion alternation of quantifiers, we can replace it with a quantifier free formula, which in this case simply ends up describing some finite graph. So checking to see if $varphi(overline{x})$ is satisfied by the tuple $overline{a}$ from a model $M$ of the random graph simply boils down to checking whether $overline{a}$ has the proper graph structure, essentially ignoring the billion quantifiers.



              This example also leads nicely in to your question about forcing quantifier elimination via Morleyization. It can be done. But the quantifier free formulas obtained this way may not have a nice representation that aids in our understanding of the theory. For example, if we carry out Morleyzation for the theory here we obtain that there is some new relation symbol $R_{varphi}((overline{x}))$ such that for any tuple $overline{a}$ from a model $M$ of the random graph $Mmodelsvarphi(overline{a})$, if and only if $Mmodels R_{varphi}overline{a}$. This doesn't really increase our understanding of how $varphi$ behaves or how to evaluate it.






              share|cite|improve this answer









              $endgroup$


















                6












                $begingroup$

                I'm going to write this answer from a model theoretic perspective and focus a bit more on why forcing quantifier elimination via Morleyization may not aid our understanding of the theory in question.



                Given a particular theory $T$, one of the key steps in understanding $T$ is to understand the definable subsets of $T$. Having quantifier elimination in this context is extremely useful. Instead of looking at extremely complicated formulas you simply look at quantifier free formulas.



                For example the theory of the random graph (in the language $L={E}$) has quantifier elimination. So instead of attempting to understand an extremely complicated formula $varphi(overline{x})$, say a formula with a billion alternation of quantifiers, we can replace it with a quantifier free formula, which in this case simply ends up describing some finite graph. So checking to see if $varphi(overline{x})$ is satisfied by the tuple $overline{a}$ from a model $M$ of the random graph simply boils down to checking whether $overline{a}$ has the proper graph structure, essentially ignoring the billion quantifiers.



                This example also leads nicely in to your question about forcing quantifier elimination via Morleyization. It can be done. But the quantifier free formulas obtained this way may not have a nice representation that aids in our understanding of the theory. For example, if we carry out Morleyzation for the theory here we obtain that there is some new relation symbol $R_{varphi}((overline{x}))$ such that for any tuple $overline{a}$ from a model $M$ of the random graph $Mmodelsvarphi(overline{a})$, if and only if $Mmodels R_{varphi}overline{a}$. This doesn't really increase our understanding of how $varphi$ behaves or how to evaluate it.






                share|cite|improve this answer









                $endgroup$
















                  6












                  6








                  6





                  $begingroup$

                  I'm going to write this answer from a model theoretic perspective and focus a bit more on why forcing quantifier elimination via Morleyization may not aid our understanding of the theory in question.



                  Given a particular theory $T$, one of the key steps in understanding $T$ is to understand the definable subsets of $T$. Having quantifier elimination in this context is extremely useful. Instead of looking at extremely complicated formulas you simply look at quantifier free formulas.



                  For example the theory of the random graph (in the language $L={E}$) has quantifier elimination. So instead of attempting to understand an extremely complicated formula $varphi(overline{x})$, say a formula with a billion alternation of quantifiers, we can replace it with a quantifier free formula, which in this case simply ends up describing some finite graph. So checking to see if $varphi(overline{x})$ is satisfied by the tuple $overline{a}$ from a model $M$ of the random graph simply boils down to checking whether $overline{a}$ has the proper graph structure, essentially ignoring the billion quantifiers.



                  This example also leads nicely in to your question about forcing quantifier elimination via Morleyization. It can be done. But the quantifier free formulas obtained this way may not have a nice representation that aids in our understanding of the theory. For example, if we carry out Morleyzation for the theory here we obtain that there is some new relation symbol $R_{varphi}((overline{x}))$ such that for any tuple $overline{a}$ from a model $M$ of the random graph $Mmodelsvarphi(overline{a})$, if and only if $Mmodels R_{varphi}overline{a}$. This doesn't really increase our understanding of how $varphi$ behaves or how to evaluate it.






                  share|cite|improve this answer









                  $endgroup$



                  I'm going to write this answer from a model theoretic perspective and focus a bit more on why forcing quantifier elimination via Morleyization may not aid our understanding of the theory in question.



                  Given a particular theory $T$, one of the key steps in understanding $T$ is to understand the definable subsets of $T$. Having quantifier elimination in this context is extremely useful. Instead of looking at extremely complicated formulas you simply look at quantifier free formulas.



                  For example the theory of the random graph (in the language $L={E}$) has quantifier elimination. So instead of attempting to understand an extremely complicated formula $varphi(overline{x})$, say a formula with a billion alternation of quantifiers, we can replace it with a quantifier free formula, which in this case simply ends up describing some finite graph. So checking to see if $varphi(overline{x})$ is satisfied by the tuple $overline{a}$ from a model $M$ of the random graph simply boils down to checking whether $overline{a}$ has the proper graph structure, essentially ignoring the billion quantifiers.



                  This example also leads nicely in to your question about forcing quantifier elimination via Morleyization. It can be done. But the quantifier free formulas obtained this way may not have a nice representation that aids in our understanding of the theory. For example, if we carry out Morleyzation for the theory here we obtain that there is some new relation symbol $R_{varphi}((overline{x}))$ such that for any tuple $overline{a}$ from a model $M$ of the random graph $Mmodelsvarphi(overline{a})$, if and only if $Mmodels R_{varphi}overline{a}$. This doesn't really increase our understanding of how $varphi$ behaves or how to evaluate it.







                  share|cite|improve this answer












                  share|cite|improve this answer



                  share|cite|improve this answer










                  answered Mar 30 at 16:23









                  dav11dav11

                  1,059512




                  1,059512






























                      draft saved

                      draft discarded




















































                      Thanks for contributing an answer to Mathematics Stack Exchange!


                      • Please be sure to answer the question. Provide details and share your research!

                      But avoid



                      • Asking for help, clarification, or responding to other answers.

                      • Making statements based on opinion; back them up with references or personal experience.


                      Use MathJax to format equations. MathJax reference.


                      To learn more, see our tips on writing great answers.




                      draft saved


                      draft discarded














                      StackExchange.ready(
                      function () {
                      StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3168402%2fwhy-is-quantifier-elimination-desirable-for-a-given-theory%23new-answer', 'question_page');
                      }
                      );

                      Post as a guest















                      Required, but never shown





















































                      Required, but never shown














                      Required, but never shown












                      Required, but never shown







                      Required, but never shown

































                      Required, but never shown














                      Required, but never shown












                      Required, but never shown







                      Required, but never shown







                      Popular posts from this blog

                      He _____ here since 1970 . Answer needed [closed]What does “since he was so high” mean?Meaning of “catch birds for”?How do I ensure “since” takes the meaning I want?“Who cares here” meaningWhat does “right round toward” mean?the time tense (had now been detected)What does the phrase “ring around the roses” mean here?Correct usage of “visited upon”Meaning of “foiled rail sabotage bid”It was the third time I had gone to Rome or It is the third time I had been to Rome

                      Bunad

                      Færeyskur hestur Heimild | Tengill | Tilvísanir | LeiðsagnarvalRossið - síða um færeyska hrossið á færeyskuGott ár hjá færeyska hestinum