Why is quantifier elimination desirable for a given theory?
$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?
first-order-logic predicate-logic model-theory quantifiers quantifier-elimination
$endgroup$
add a comment |
$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?
first-order-logic predicate-logic model-theory quantifiers quantifier-elimination
$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
add a comment |
$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?
first-order-logic predicate-logic model-theory quantifiers quantifier-elimination
$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
first-order-logic predicate-logic model-theory quantifiers quantifier-elimination
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
add a comment |
$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
add a comment |
2 Answers
2
active
oldest
votes
$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.
$endgroup$
add a comment |
$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.
$endgroup$
add a comment |
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
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
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
$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.
$endgroup$
add a comment |
$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.
$endgroup$
add a comment |
$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.
$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.
answered Mar 30 at 15:48
Noah SchweberNoah Schweber
128k10152294
128k10152294
add a comment |
add a comment |
$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.
$endgroup$
add a comment |
$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.
$endgroup$
add a comment |
$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.
$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.
answered Mar 30 at 16:23
dav11dav11
1,059512
1,059512
add a comment |
add a comment |
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.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
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
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
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
$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