Mixing
What's the strength of logic without $negnegexists x P(x) implies exists x P(x)$?
$begingroup$
As far as I understand, the main idea of constructive logic is that we only allow proof methods that let us show the statement $exists x:P(x)$ only by constructing an explicit such object $x$, right? So for instance one can't do this:
first assume that $exists x: P(x)$ is false, then this leads to …, which is a contradiction; therefore $exists x: P(x)$.
Having this main idea of constructive logic in mind I would define constructive logic (= intuitionistic logic?) to be logic without the rule $negnegexists x P(x)impliesexists xP(x)$. But this seems to contradict the slogan "constructive logic is classical logic without law of excluded middle (and therefore – because these two happen to be equivalent – without double negation elimination)". I'm assuming this is the "correct" definition of constructive logic. So constructive logic is classical logic without $negneg Aimplies A$.
My question is already in the title: How strong is classical logic without $negnegexists x P(x)impliesexists xP(x)$? Is it strictly stronger than constructive logic; and is it strictly weaker than classical logic?
Another question I have is this (but it's quite "soft"): Why does one define constructive logic as the logic without $negneg Aimplies A$ rather than logic without $negnegexists x P(x)impliesexists xP(x)$? Isn't using the rule $negneg Aimplies A$ for an existential $A$ what makes a proof non-constructive?
logic soft-question formal-proofs constructive-mathematics
asked Dec 25 '16 at 16:44
user7280899user7280899
872516
$endgroup$
add a comment |
$begingroup$
As far as I understand, the main idea of constructive logic is that we only allow proof methods that let us show the statement $exists x:P(x)$ only by constructing an explicit such object $x$, right? So for instance one can't do this:
first assume that $exists x: P(x)$ is false, then this leads to …, which is a contradiction; therefore $exists x: P(x)$.
Having this main idea of constructive logic in mind I would define constructive logic (= intuitionistic logic?) to be logic without the rule $negnegexists x P(x)impliesexists xP(x)$. But this seems to contradict the slogan "constructive logic is classical logic without law of excluded middle (and therefore – because these two happen to be equivalent – without double negation elimination)". I'm assuming this is the "correct" definition of constructive logic. So constructive logic is classical logic without $negneg Aimplies A$.
My question is already in the title: How strong is classical logic without $negnegexists x P(x)impliesexists xP(x)$? Is it strictly stronger than constructive logic; and is it strictly weaker than classical logic?
Another question I have is this (but it's quite "soft"): Why does one define constructive logic as the logic without $negneg Aimplies A$ rather than logic without $negnegexists x P(x)impliesexists xP(x)$? Isn't using the rule $negneg Aimplies A$ for an existential $A$ what makes a proof non-constructive?
logic soft-question formal-proofs constructive-mathematics
asked Dec 25 '16 at 16:44
user7280899user7280899
872516
$endgroup$
$begingroup$
To prove $lnot lnot exists x Px Rightarrow exists x Px$ you need double negation...
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:48
$begingroup$
@MauroALLEGRANZA: To prove what? Could you be a bit more specific?
$endgroup$
– user7280899
Dec 25 '16 at 16:49
$begingroup$
Intuitionism rejects DN (that is equiv to LEM) precisely because he does not agree on the fact that in order to assert the existence of "some $x$ that is $P$" it is enough to prove the absurdity of "there is no $x$ that is $P$".
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:54
1
$begingroup$
You seem to be asking what kind of logic we get if instead of disallowing the double negation schema $lnotlnot Aimplies A$, where $A$ ranges over any closed formula, we only disallow that implication when $A$ has the specific form $exists xP(x)$. But in that case, we could still take $A$ to be $(exists xP(x))lor(Qlandlnot Q)$ for some propositional formula $Q$.
$endgroup$
– symplectomorphic
Dec 25 '16 at 17:31
add a comment |
$begingroup$
As far as I understand, the main idea of constructive logic is that we only allow proof methods that let us show the statement $exists x:P(x)$ only by constructing an explicit such object $x$, right? So for instance one can't do this:
first assume that $exists x: P(x)$ is false, then this leads to …, which is a contradiction; therefore $exists x: P(x)$.
Having this main idea of constructive logic in mind I would define constructive logic (= intuitionistic logic?) to be logic without the rule $negnegexists x P(x)impliesexists xP(x)$. But this seems to contradict the slogan "constructive logic is classical logic without law of excluded middle (and therefore – because these two happen to be equivalent – without double negation elimination)". I'm assuming this is the "correct" definition of constructive logic. So constructive logic is classical logic without $negneg Aimplies A$.
My question is already in the title: How strong is classical logic without $negnegexists x P(x)impliesexists xP(x)$? Is it strictly stronger than constructive logic; and is it strictly weaker than classical logic?
Another question I have is this (but it's quite "soft"): Why does one define constructive logic as the logic without $negneg Aimplies A$ rather than logic without $negnegexists x P(x)impliesexists xP(x)$? Isn't using the rule $negneg Aimplies A$ for an existential $A$ what makes a proof non-constructive?
logic soft-question formal-proofs constructive-mathematics
asked Dec 25 '16 at 16:44
user7280899user7280899
872516
$endgroup$
As far as I understand, the main idea of constructive logic is that we only allow proof methods that let us show the statement $exists x:P(x)$ only by constructing an explicit such object $x$, right? So for instance one can't do this:
first assume that $exists x: P(x)$ is false, then this leads to …, which is a contradiction; therefore $exists x: P(x)$.
Having this main idea of constructive logic in mind I would define constructive logic (= intuitionistic logic?) to be logic without the rule $negnegexists x P(x)impliesexists xP(x)$. But this seems to contradict the slogan "constructive logic is classical logic without law of excluded middle (and therefore – because these two happen to be equivalent – without double negation elimination)". I'm assuming this is the "correct" definition of constructive logic. So constructive logic is classical logic without $negneg Aimplies A$.
My question is already in the title: How strong is classical logic without $negnegexists x P(x)impliesexists xP(x)$? Is it strictly stronger than constructive logic; and is it strictly weaker than classical logic?
Another question I have is this (but it's quite "soft"): Why does one define constructive logic as the logic without $negneg Aimplies A$ rather than logic without $negnegexists x P(x)impliesexists xP(x)$? Isn't using the rule $negneg Aimplies A$ for an existential $A$ what makes a proof non-constructive?
logic soft-question formal-proofs constructive-mathematics
logic soft-question formal-proofs constructive-mathematics
asked Dec 25 '16 at 16:44
user7280899user7280899
872516
asked Dec 25 '16 at 16:44
user7280899user7280899
872516
asked Dec 25 '16 at 16:44
user7280899user7280899
872516
asked Dec 25 '16 at 16:44
user7280899user7280899
872516
asked Dec 25 '16 at 16:44
user7280899user7280899
872516
872516
$begingroup$
To prove $lnot lnot exists x Px Rightarrow exists x Px$ you need double negation...
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:48
$begingroup$
@MauroALLEGRANZA: To prove what? Could you be a bit more specific?
$endgroup$
– user7280899
Dec 25 '16 at 16:49
$begingroup$
Intuitionism rejects DN (that is equiv to LEM) precisely because he does not agree on the fact that in order to assert the existence of "some $x$ that is $P$" it is enough to prove the absurdity of "there is no $x$ that is $P$".
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:54
1
$begingroup$
You seem to be asking what kind of logic we get if instead of disallowing the double negation schema $lnotlnot Aimplies A$, where $A$ ranges over any closed formula, we only disallow that implication when $A$ has the specific form $exists xP(x)$. But in that case, we could still take $A$ to be $(exists xP(x))lor(Qlandlnot Q)$ for some propositional formula $Q$.
$endgroup$
– symplectomorphic
Dec 25 '16 at 17:31
add a comment |
$begingroup$
To prove $lnot lnot exists x Px Rightarrow exists x Px$ you need double negation...
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:48
$begingroup$
@MauroALLEGRANZA: To prove what? Could you be a bit more specific?
$endgroup$
– user7280899
Dec 25 '16 at 16:49
$begingroup$
Intuitionism rejects DN (that is equiv to LEM) precisely because he does not agree on the fact that in order to assert the existence of "some $x$ that is $P$" it is enough to prove the absurdity of "there is no $x$ that is $P$".
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:54
1
$begingroup$
You seem to be asking what kind of logic we get if instead of disallowing the double negation schema $lnotlnot Aimplies A$, where $A$ ranges over any closed formula, we only disallow that implication when $A$ has the specific form $exists xP(x)$. But in that case, we could still take $A$ to be $(exists xP(x))lor(Qlandlnot Q)$ for some propositional formula $Q$.
$endgroup$
– symplectomorphic
Dec 25 '16 at 17:31
$begingroup$
To prove $lnot lnot exists x Px Rightarrow exists x Px$ you need double negation...
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:48
$begingroup$
To prove $lnot lnot exists x Px Rightarrow exists x Px$ you need double negation...
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:48
$begingroup$
@MauroALLEGRANZA: To prove what? Could you be a bit more specific?
$endgroup$
– user7280899
Dec 25 '16 at 16:49
$begingroup$
@MauroALLEGRANZA: To prove what? Could you be a bit more specific?
$endgroup$
– user7280899
Dec 25 '16 at 16:49
$begingroup$
Intuitionism rejects DN (that is equiv to LEM) precisely because he does not agree on the fact that in order to assert the existence of "some $x$ that is $P$" it is enough to prove the absurdity of "there is no $x$ that is $P$".
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:54
$begingroup$
Intuitionism rejects DN (that is equiv to LEM) precisely because he does not agree on the fact that in order to assert the existence of "some $x$ that is $P$" it is enough to prove the absurdity of "there is no $x$ that is $P$".
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:54
1
1
$begingroup$
You seem to be asking what kind of logic we get if instead of disallowing the double negation schema $lnotlnot Aimplies A$, where $A$ ranges over any closed formula, we only disallow that implication when $A$ has the specific form $exists xP(x)$. But in that case, we could still take $A$ to be $(exists xP(x))lor(Qlandlnot Q)$ for some propositional formula $Q$.
$endgroup$
– symplectomorphic
Dec 25 '16 at 17:31
$begingroup$
You seem to be asking what kind of logic we get if instead of disallowing the double negation schema $lnotlnot Aimplies A$, where $A$ ranges over any closed formula, we only disallow that implication when $A$ has the specific form $exists xP(x)$. But in that case, we could still take $A$ to be $(exists xP(x))lor(Qlandlnot Q)$ for some propositional formula $Q$.
$endgroup$
– symplectomorphic
Dec 25 '16 at 17:31
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
Classical logic including proofs by contradiction can be mapped to a subset of constructive logic while preserving consistency: https://plato.stanford.edu/entries/logic-intuitionistic/#TraClaIntLog
Therefore, one might consider constructive logic as being "stronger" when it comes to expressiveness. After all, it can, in addition to providing support for classical logic, express statements which cannon be expressed in classical logic.
answered Jan 23 at 10:44
ternaryternary
61
$endgroup$
add a comment |
$begingroup$
As said in the comments section, in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" the statement "$¬¬A ⟹ A$" where $A$ is $(∃xP(x))∨(Q∧¬Q)$ ($Q$ can be any statement, such as $∃x.x=x$) is still true. Now if $¬¬∃xP(x)$ then $¬¬((∃xP(x))∨(Q∧¬Q))$; because if $¬((∃xP(x))∨(Q∧¬Q))$, then $¬(∃xP(x))$. Also, if $(∃xP(x))∨(Q∧¬Q)$, then by case analysis $∃xP(x)$.
Thus we have proven in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" that $¬¬∃xP(x) ⟹ ∃xP(x)$. Therefore, this logic is equivalent to classical logic.
answered Dec 25 '16 at 18:47
user7280899user7280899
872516
$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%2f2071692%2fwhats-the-strength-of-logic-without-neg-neg-exists-x-px-implies-exists-x%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$
Classical logic including proofs by contradiction can be mapped to a subset of constructive logic while preserving consistency: https://plato.stanford.edu/entries/logic-intuitionistic/#TraClaIntLog
Therefore, one might consider constructive logic as being "stronger" when it comes to expressiveness. After all, it can, in addition to providing support for classical logic, express statements which cannon be expressed in classical logic.
answered Jan 23 at 10:44
ternaryternary
61
$endgroup$
add a comment |
$begingroup$
Classical logic including proofs by contradiction can be mapped to a subset of constructive logic while preserving consistency: https://plato.stanford.edu/entries/logic-intuitionistic/#TraClaIntLog
Therefore, one might consider constructive logic as being "stronger" when it comes to expressiveness. After all, it can, in addition to providing support for classical logic, express statements which cannon be expressed in classical logic.
answered Jan 23 at 10:44
ternaryternary
61
$endgroup$
add a comment |
$begingroup$
Classical logic including proofs by contradiction can be mapped to a subset of constructive logic while preserving consistency: https://plato.stanford.edu/entries/logic-intuitionistic/#TraClaIntLog
Therefore, one might consider constructive logic as being "stronger" when it comes to expressiveness. After all, it can, in addition to providing support for classical logic, express statements which cannon be expressed in classical logic.
answered Jan 23 at 10:44
ternaryternary
61
$endgroup$
Classical logic including proofs by contradiction can be mapped to a subset of constructive logic while preserving consistency: https://plato.stanford.edu/entries/logic-intuitionistic/#TraClaIntLog
Therefore, one might consider constructive logic as being "stronger" when it comes to expressiveness. After all, it can, in addition to providing support for classical logic, express statements which cannon be expressed in classical logic.
answered Jan 23 at 10:44
ternaryternary
61
answered Jan 23 at 10:44
ternaryternary
61
answered Jan 23 at 10:44
ternaryternary
61
answered Jan 23 at 10:44
ternaryternary
61
61
add a comment |
add a comment |
$begingroup$
As said in the comments section, in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" the statement "$¬¬A ⟹ A$" where $A$ is $(∃xP(x))∨(Q∧¬Q)$ ($Q$ can be any statement, such as $∃x.x=x$) is still true. Now if $¬¬∃xP(x)$ then $¬¬((∃xP(x))∨(Q∧¬Q))$; because if $¬((∃xP(x))∨(Q∧¬Q))$, then $¬(∃xP(x))$. Also, if $(∃xP(x))∨(Q∧¬Q)$, then by case analysis $∃xP(x)$.
Thus we have proven in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" that $¬¬∃xP(x) ⟹ ∃xP(x)$. Therefore, this logic is equivalent to classical logic.
answered Dec 25 '16 at 18:47
user7280899user7280899
872516
$endgroup$
add a comment |
$begingroup$
As said in the comments section, in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" the statement "$¬¬A ⟹ A$" where $A$ is $(∃xP(x))∨(Q∧¬Q)$ ($Q$ can be any statement, such as $∃x.x=x$) is still true. Now if $¬¬∃xP(x)$ then $¬¬((∃xP(x))∨(Q∧¬Q))$; because if $¬((∃xP(x))∨(Q∧¬Q))$, then $¬(∃xP(x))$. Also, if $(∃xP(x))∨(Q∧¬Q)$, then by case analysis $∃xP(x)$.
Thus we have proven in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" that $¬¬∃xP(x) ⟹ ∃xP(x)$. Therefore, this logic is equivalent to classical logic.
answered Dec 25 '16 at 18:47
user7280899user7280899
872516
$endgroup$
add a comment |
$begingroup$
As said in the comments section, in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" the statement "$¬¬A ⟹ A$" where $A$ is $(∃xP(x))∨(Q∧¬Q)$ ($Q$ can be any statement, such as $∃x.x=x$) is still true. Now if $¬¬∃xP(x)$ then $¬¬((∃xP(x))∨(Q∧¬Q))$; because if $¬((∃xP(x))∨(Q∧¬Q))$, then $¬(∃xP(x))$. Also, if $(∃xP(x))∨(Q∧¬Q)$, then by case analysis $∃xP(x)$.
Thus we have proven in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" that $¬¬∃xP(x) ⟹ ∃xP(x)$. Therefore, this logic is equivalent to classical logic.
answered Dec 25 '16 at 18:47
user7280899user7280899
872516
$endgroup$
As said in the comments section, in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" the statement "$¬¬A ⟹ A$" where $A$ is $(∃xP(x))∨(Q∧¬Q)$ ($Q$ can be any statement, such as $∃x.x=x$) is still true. Now if $¬¬∃xP(x)$ then $¬¬((∃xP(x))∨(Q∧¬Q))$; because if $¬((∃xP(x))∨(Q∧¬Q))$, then $¬(∃xP(x))$. Also, if $(∃xP(x))∨(Q∧¬Q)$, then by case analysis $∃xP(x)$.
Thus we have proven in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" that $¬¬∃xP(x) ⟹ ∃xP(x)$. Therefore, this logic is equivalent to classical logic.
answered Dec 25 '16 at 18:47
user7280899user7280899
872516
answered Dec 25 '16 at 18:47
user7280899user7280899
872516
answered Dec 25 '16 at 18:47
user7280899user7280899
872516
answered Dec 25 '16 at 18:47
user7280899user7280899
872516
872516
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%2f2071692%2fwhats-the-strength-of-logic-without-neg-neg-exists-x-px-implies-exists-x%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$
To prove $lnot lnot exists x Px Rightarrow exists x Px$ you need double negation...
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:48
$begingroup$
@MauroALLEGRANZA: To prove what? Could you be a bit more specific?
$endgroup$
– user7280899
Dec 25 '16 at 16:49
$begingroup$
Intuitionism rejects DN (that is equiv to LEM) precisely because he does not agree on the fact that in order to assert the existence of "some $x$ that is $P$" it is enough to prove the absurdity of "there is no $x$ that is $P$".
$endgroup$
– Mauro ALLEGRANZA
Dec 25 '16 at 16:54
1
$begingroup$
You seem to be asking what kind of logic we get if instead of disallowing the double negation schema $lnotlnot Aimplies A$, where $A$ ranges over any closed formula, we only disallow that implication when $A$ has the specific form $exists xP(x)$. But in that case, we could still take $A$ to be $(exists xP(x))lor(Qlandlnot Q)$ for some propositional formula $Q$.
$endgroup$
– symplectomorphic
Dec 25 '16 at 17:31