Mixing
Would natural deduction maintain its soundness with introduction of new rule?
$begingroup$
I'm asked if adding the following rule to natural deduction would maintain the soundness and completeness of natural deduction. I think with the first one, natural deduction would maintain its completeness, because it doesn't change or take away any rules, so everything true can be proved true with the logic system, but it wouldn't be sound, but I'm not exactly sure why, it seems like maybe because one assumption could be false, then from that you're concluding true with the OR, which seems like a contradiction.
ϕ ψ
.............. (∨I')
ϕ ∨ ψ
With the second one, I feel it's the same that it would be complete still, but not sound because you can't just prove true from nothing.
................ (¬⊥I)
¬⊥
natural-deduction
asked Dec 29 '18 at 6:06
Jamie WhitakerJamie Whitaker
162
$endgroup$
add a comment |
$begingroup$
I'm asked if adding the following rule to natural deduction would maintain the soundness and completeness of natural deduction. I think with the first one, natural deduction would maintain its completeness, because it doesn't change or take away any rules, so everything true can be proved true with the logic system, but it wouldn't be sound, but I'm not exactly sure why, it seems like maybe because one assumption could be false, then from that you're concluding true with the OR, which seems like a contradiction.
ϕ ψ
.............. (∨I')
ϕ ∨ ψ
With the second one, I feel it's the same that it would be complete still, but not sound because you can't just prove true from nothing.
................ (¬⊥I)
¬⊥
natural-deduction
asked Dec 29 '18 at 6:06
Jamie WhitakerJamie Whitaker
162
$endgroup$
$begingroup$
What is a conclusion in the first rule?
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:27
$begingroup$
ϕ ∨ ψ Sorry I'm not sure what happened to it.
$endgroup$
– Jamie Whitaker
Dec 29 '18 at 6:28
$begingroup$
To prove soundness you have to show that the new rules are truth-preserving. It's quite easy. The second rule is obviously truth-preserving, because there is nothing above the line and below there is a tautology.
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:34
$begingroup$
Is the rule $lor_I'$ added to the usual rules $lor_{I_1}$ and $lor_{I_2}$ in natural deduction, or does it replace them?
$endgroup$
– Taroccoesbrocco
Dec 29 '18 at 7:10
$begingroup$
I believe this is true since the new system is no more powerful than the old system. The fact that all proofs in the new system could be re-formulated in the old system means that IF a contradiction could be found in the new system, THEN a contradiction could be found in the old system. By contrapositive, soundness is implied. Not as sure about completeness.
$endgroup$
– Quelklef
Dec 29 '18 at 22:00
add a comment |
$begingroup$
I'm asked if adding the following rule to natural deduction would maintain the soundness and completeness of natural deduction. I think with the first one, natural deduction would maintain its completeness, because it doesn't change or take away any rules, so everything true can be proved true with the logic system, but it wouldn't be sound, but I'm not exactly sure why, it seems like maybe because one assumption could be false, then from that you're concluding true with the OR, which seems like a contradiction.
ϕ ψ
.............. (∨I')
ϕ ∨ ψ
With the second one, I feel it's the same that it would be complete still, but not sound because you can't just prove true from nothing.
................ (¬⊥I)
¬⊥
natural-deduction
asked Dec 29 '18 at 6:06
Jamie WhitakerJamie Whitaker
162
$endgroup$
I'm asked if adding the following rule to natural deduction would maintain the soundness and completeness of natural deduction. I think with the first one, natural deduction would maintain its completeness, because it doesn't change or take away any rules, so everything true can be proved true with the logic system, but it wouldn't be sound, but I'm not exactly sure why, it seems like maybe because one assumption could be false, then from that you're concluding true with the OR, which seems like a contradiction.
ϕ ψ
.............. (∨I')
ϕ ∨ ψ
With the second one, I feel it's the same that it would be complete still, but not sound because you can't just prove true from nothing.
................ (¬⊥I)
¬⊥
natural-deduction
natural-deduction
asked Dec 29 '18 at 6:06
Jamie WhitakerJamie Whitaker
162
asked Dec 29 '18 at 6:06
Jamie WhitakerJamie Whitaker
162
edited Dec 29 '18 at 6:30
Jamie Whitaker
asked Dec 29 '18 at 6:06
Jamie WhitakerJamie Whitaker
162
asked Dec 29 '18 at 6:06
Jamie WhitakerJamie Whitaker
162
asked Dec 29 '18 at 6:06
Jamie WhitakerJamie Whitaker
162
162
$begingroup$
What is a conclusion in the first rule?
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:27
$begingroup$
ϕ ∨ ψ Sorry I'm not sure what happened to it.
$endgroup$
– Jamie Whitaker
Dec 29 '18 at 6:28
$begingroup$
To prove soundness you have to show that the new rules are truth-preserving. It's quite easy. The second rule is obviously truth-preserving, because there is nothing above the line and below there is a tautology.
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:34
$begingroup$
Is the rule $lor_I'$ added to the usual rules $lor_{I_1}$ and $lor_{I_2}$ in natural deduction, or does it replace them?
$endgroup$
– Taroccoesbrocco
Dec 29 '18 at 7:10
$begingroup$
I believe this is true since the new system is no more powerful than the old system. The fact that all proofs in the new system could be re-formulated in the old system means that IF a contradiction could be found in the new system, THEN a contradiction could be found in the old system. By contrapositive, soundness is implied. Not as sure about completeness.
$endgroup$
– Quelklef
Dec 29 '18 at 22:00
add a comment |
$begingroup$
What is a conclusion in the first rule?
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:27
$begingroup$
ϕ ∨ ψ Sorry I'm not sure what happened to it.
$endgroup$
– Jamie Whitaker
Dec 29 '18 at 6:28
$begingroup$
To prove soundness you have to show that the new rules are truth-preserving. It's quite easy. The second rule is obviously truth-preserving, because there is nothing above the line and below there is a tautology.
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:34
$begingroup$
Is the rule $lor_I'$ added to the usual rules $lor_{I_1}$ and $lor_{I_2}$ in natural deduction, or does it replace them?
$endgroup$
– Taroccoesbrocco
Dec 29 '18 at 7:10
$begingroup$
I believe this is true since the new system is no more powerful than the old system. The fact that all proofs in the new system could be re-formulated in the old system means that IF a contradiction could be found in the new system, THEN a contradiction could be found in the old system. By contrapositive, soundness is implied. Not as sure about completeness.
$endgroup$
– Quelklef
Dec 29 '18 at 22:00
$begingroup$
What is a conclusion in the first rule?
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:27
$begingroup$
What is a conclusion in the first rule?
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:27
$begingroup$
ϕ ∨ ψ Sorry I'm not sure what happened to it.
$endgroup$
– Jamie Whitaker
Dec 29 '18 at 6:28
$begingroup$
ϕ ∨ ψ Sorry I'm not sure what happened to it.
$endgroup$
– Jamie Whitaker
Dec 29 '18 at 6:28
$begingroup$
To prove soundness you have to show that the new rules are truth-preserving. It's quite easy. The second rule is obviously truth-preserving, because there is nothing above the line and below there is a tautology.
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:34
$begingroup$
To prove soundness you have to show that the new rules are truth-preserving. It's quite easy. The second rule is obviously truth-preserving, because there is nothing above the line and below there is a tautology.
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:34
$begingroup$
Is the rule $lor_I'$ added to the usual rules $lor_{I_1}$ and $lor_{I_2}$ in natural deduction, or does it replace them?
$endgroup$
– Taroccoesbrocco
Dec 29 '18 at 7:10
$begingroup$
Is the rule $lor_I'$ added to the usual rules $lor_{I_1}$ and $lor_{I_2}$ in natural deduction, or does it replace them?
$endgroup$
– Taroccoesbrocco
Dec 29 '18 at 7:10
$begingroup$
I believe this is true since the new system is no more powerful than the old system. The fact that all proofs in the new system could be re-formulated in the old system means that IF a contradiction could be found in the new system, THEN a contradiction could be found in the old system. By contrapositive, soundness is implied. Not as sure about completeness.
$endgroup$
– Quelklef
Dec 29 '18 at 22:00
$begingroup$
I believe this is true since the new system is no more powerful than the old system. The fact that all proofs in the new system could be re-formulated in the old system means that IF a contradiction could be found in the new system, THEN a contradiction could be found in the old system. By contrapositive, soundness is implied. Not as sure about completeness.
$endgroup$
– Quelklef
Dec 29 '18 at 22:00
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Both ND+$lor I'$ and ND+$negbot I$ are sound:
ND+$lor I'$-Soundness: Suppose ${phi,psi}vdash(philorpsi)$ by $lor I'$, then we have to show ${phi,psi}models(philorpsi)$, but this is of course true by the usual semantics of ND.
ND+$negbot I$-Soundness: Similarly, we have $modelsnegbot$ since every model $A$ has $A(bot)=F$ and hence has $A(negbot)=T$.
And ND+$R$ where $R$ is any rule is complete:
ND+$R$-Completeness: Suppose $Gammamodelsphi$, then $Gammavdash_{mathrm{ND}}phi$ by ND-completeness, which is a still a proof of $Gammavdash_{mathrm{ND}+R}phi$ (without any uses of $R$).
I'm not an expert in logic so if there are any mistakes, please me know!
answered Jan 9 at 2:18
palmpopalmpo
3861213
$endgroup$
1
$begingroup$
For completeness in both cases, shouldn't it be sufficient just to say any valid sequent $Gamma vdash phi$ has a proof in ND which fairly trivially lifts to a proof in ND+$vee I'$ and to a proof in ND+$lnotbot I$?
$endgroup$
– Daniel Schepler
Jan 9 at 18:21
$begingroup$
Wow I completely missed that, yeah it sounds like completeness is trivial then. Let me edit that in.
$endgroup$
– palmpo
Jan 9 at 23:57
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%2f3055587%2fwould-natural-deduction-maintain-its-soundness-with-introduction-of-new-rule%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Both ND+$lor I'$ and ND+$negbot I$ are sound:
ND+$lor I'$-Soundness: Suppose ${phi,psi}vdash(philorpsi)$ by $lor I'$, then we have to show ${phi,psi}models(philorpsi)$, but this is of course true by the usual semantics of ND.
ND+$negbot I$-Soundness: Similarly, we have $modelsnegbot$ since every model $A$ has $A(bot)=F$ and hence has $A(negbot)=T$.
And ND+$R$ where $R$ is any rule is complete:
ND+$R$-Completeness: Suppose $Gammamodelsphi$, then $Gammavdash_{mathrm{ND}}phi$ by ND-completeness, which is a still a proof of $Gammavdash_{mathrm{ND}+R}phi$ (without any uses of $R$).
I'm not an expert in logic so if there are any mistakes, please me know!
answered Jan 9 at 2:18
palmpopalmpo
3861213
$endgroup$
1
$begingroup$
For completeness in both cases, shouldn't it be sufficient just to say any valid sequent $Gamma vdash phi$ has a proof in ND which fairly trivially lifts to a proof in ND+$vee I'$ and to a proof in ND+$lnotbot I$?
$endgroup$
– Daniel Schepler
Jan 9 at 18:21
$begingroup$
Wow I completely missed that, yeah it sounds like completeness is trivial then. Let me edit that in.
$endgroup$
– palmpo
Jan 9 at 23:57
add a comment |
$begingroup$
Both ND+$lor I'$ and ND+$negbot I$ are sound:
ND+$lor I'$-Soundness: Suppose ${phi,psi}vdash(philorpsi)$ by $lor I'$, then we have to show ${phi,psi}models(philorpsi)$, but this is of course true by the usual semantics of ND.
ND+$negbot I$-Soundness: Similarly, we have $modelsnegbot$ since every model $A$ has $A(bot)=F$ and hence has $A(negbot)=T$.
And ND+$R$ where $R$ is any rule is complete:
ND+$R$-Completeness: Suppose $Gammamodelsphi$, then $Gammavdash_{mathrm{ND}}phi$ by ND-completeness, which is a still a proof of $Gammavdash_{mathrm{ND}+R}phi$ (without any uses of $R$).
I'm not an expert in logic so if there are any mistakes, please me know!
answered Jan 9 at 2:18
palmpopalmpo
3861213
$endgroup$
1
$begingroup$
For completeness in both cases, shouldn't it be sufficient just to say any valid sequent $Gamma vdash phi$ has a proof in ND which fairly trivially lifts to a proof in ND+$vee I'$ and to a proof in ND+$lnotbot I$?
$endgroup$
– Daniel Schepler
Jan 9 at 18:21
$begingroup$
Wow I completely missed that, yeah it sounds like completeness is trivial then. Let me edit that in.
$endgroup$
– palmpo
Jan 9 at 23:57
add a comment |
$begingroup$
Both ND+$lor I'$ and ND+$negbot I$ are sound:
ND+$lor I'$-Soundness: Suppose ${phi,psi}vdash(philorpsi)$ by $lor I'$, then we have to show ${phi,psi}models(philorpsi)$, but this is of course true by the usual semantics of ND.
ND+$negbot I$-Soundness: Similarly, we have $modelsnegbot$ since every model $A$ has $A(bot)=F$ and hence has $A(negbot)=T$.
And ND+$R$ where $R$ is any rule is complete:
ND+$R$-Completeness: Suppose $Gammamodelsphi$, then $Gammavdash_{mathrm{ND}}phi$ by ND-completeness, which is a still a proof of $Gammavdash_{mathrm{ND}+R}phi$ (without any uses of $R$).
I'm not an expert in logic so if there are any mistakes, please me know!
answered Jan 9 at 2:18
palmpopalmpo
3861213
$endgroup$
Both ND+$lor I'$ and ND+$negbot I$ are sound:
ND+$lor I'$-Soundness: Suppose ${phi,psi}vdash(philorpsi)$ by $lor I'$, then we have to show ${phi,psi}models(philorpsi)$, but this is of course true by the usual semantics of ND.
ND+$negbot I$-Soundness: Similarly, we have $modelsnegbot$ since every model $A$ has $A(bot)=F$ and hence has $A(negbot)=T$.
And ND+$R$ where $R$ is any rule is complete:
ND+$R$-Completeness: Suppose $Gammamodelsphi$, then $Gammavdash_{mathrm{ND}}phi$ by ND-completeness, which is a still a proof of $Gammavdash_{mathrm{ND}+R}phi$ (without any uses of $R$).
I'm not an expert in logic so if there are any mistakes, please me know!
answered Jan 9 at 2:18
palmpopalmpo
3861213
edited Jan 10 at 0:02
answered Jan 9 at 2:18
palmpopalmpo
3861213
answered Jan 9 at 2:18
palmpopalmpo
3861213
answered Jan 9 at 2:18
palmpopalmpo
3861213
3861213
1
$begingroup$
For completeness in both cases, shouldn't it be sufficient just to say any valid sequent $Gamma vdash phi$ has a proof in ND which fairly trivially lifts to a proof in ND+$vee I'$ and to a proof in ND+$lnotbot I$?
$endgroup$
– Daniel Schepler
Jan 9 at 18:21
$begingroup$
Wow I completely missed that, yeah it sounds like completeness is trivial then. Let me edit that in.
$endgroup$
– palmpo
Jan 9 at 23:57
add a comment |
1
$begingroup$
For completeness in both cases, shouldn't it be sufficient just to say any valid sequent $Gamma vdash phi$ has a proof in ND which fairly trivially lifts to a proof in ND+$vee I'$ and to a proof in ND+$lnotbot I$?
$endgroup$
– Daniel Schepler
Jan 9 at 18:21
$begingroup$
Wow I completely missed that, yeah it sounds like completeness is trivial then. Let me edit that in.
$endgroup$
– palmpo
Jan 9 at 23:57
1
1
$begingroup$
For completeness in both cases, shouldn't it be sufficient just to say any valid sequent $Gamma vdash phi$ has a proof in ND which fairly trivially lifts to a proof in ND+$vee I'$ and to a proof in ND+$lnotbot I$?
$endgroup$
– Daniel Schepler
Jan 9 at 18:21
$begingroup$
For completeness in both cases, shouldn't it be sufficient just to say any valid sequent $Gamma vdash phi$ has a proof in ND which fairly trivially lifts to a proof in ND+$vee I'$ and to a proof in ND+$lnotbot I$?
$endgroup$
– Daniel Schepler
Jan 9 at 18:21
$begingroup$
Wow I completely missed that, yeah it sounds like completeness is trivial then. Let me edit that in.
$endgroup$
– palmpo
Jan 9 at 23:57
$begingroup$
Wow I completely missed that, yeah it sounds like completeness is trivial then. Let me edit that in.
$endgroup$
– palmpo
Jan 9 at 23:57
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%2f3055587%2fwould-natural-deduction-maintain-its-soundness-with-introduction-of-new-rule%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$
What is a conclusion in the first rule?
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:27
$begingroup$
ϕ ∨ ψ Sorry I'm not sure what happened to it.
$endgroup$
– Jamie Whitaker
Dec 29 '18 at 6:28
$begingroup$
To prove soundness you have to show that the new rules are truth-preserving. It's quite easy. The second rule is obviously truth-preserving, because there is nothing above the line and below there is a tautology.
$endgroup$
– Ilya Vlasov
Dec 29 '18 at 6:34
$begingroup$
Is the rule $lor_I'$ added to the usual rules $lor_{I_1}$ and $lor_{I_2}$ in natural deduction, or does it replace them?
$endgroup$
– Taroccoesbrocco
Dec 29 '18 at 7:10
$begingroup$
I believe this is true since the new system is no more powerful than the old system. The fact that all proofs in the new system could be re-formulated in the old system means that IF a contradiction could be found in the new system, THEN a contradiction could be found in the old system. By contrapositive, soundness is implied. Not as sure about completeness.
$endgroup$
– Quelklef
Dec 29 '18 at 22:00