Mixing
Natural deduction proof of $(A to lnot B lor C), ((lnot D land A) to B), (lnot E to A) vdash D lor (C lor E)$
$begingroup$
I'm struggling to proof this both if I use or introduction rule $lor_{I_1}$ (to work on $D$) or or introduction rule $lor_{I_2}$ (to work on $C lor E$). Could you help me?
logic propositional-calculus natural-deduction formal-proofs
edited Jan 2 at 18:51
Taroccoesbrocco
5,14761839
asked Jan 2 at 12:11
MaicakeMaicake
615
$endgroup$
add a comment |
$begingroup$
I'm struggling to proof this both if I use or introduction rule $lor_{I_1}$ (to work on $D$) or or introduction rule $lor_{I_2}$ (to work on $C lor E$). Could you help me?
logic propositional-calculus natural-deduction formal-proofs
edited Jan 2 at 18:51
Taroccoesbrocco
5,14761839
asked Jan 2 at 12:11
MaicakeMaicake
615
$endgroup$
1
$begingroup$
$D lor (C land E)$ or $D lor (C lor E)$ ?
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 12:33
$begingroup$
Second one, sorry.
$endgroup$
– Maicake
Jan 2 at 12:39
add a comment |
$begingroup$
I'm struggling to proof this both if I use or introduction rule $lor_{I_1}$ (to work on $D$) or or introduction rule $lor_{I_2}$ (to work on $C lor E$). Could you help me?
logic propositional-calculus natural-deduction formal-proofs
edited Jan 2 at 18:51
Taroccoesbrocco
5,14761839
asked Jan 2 at 12:11
MaicakeMaicake
615
$endgroup$
I'm struggling to proof this both if I use or introduction rule $lor_{I_1}$ (to work on $D$) or or introduction rule $lor_{I_2}$ (to work on $C lor E$). Could you help me?
logic propositional-calculus natural-deduction formal-proofs
logic propositional-calculus natural-deduction formal-proofs
edited Jan 2 at 18:51
Taroccoesbrocco
5,14761839
asked Jan 2 at 12:11
MaicakeMaicake
615
edited Jan 2 at 18:51
Taroccoesbrocco
5,14761839
asked Jan 2 at 12:11
MaicakeMaicake
615
edited Jan 2 at 18:51
Taroccoesbrocco
5,14761839
edited Jan 2 at 18:51
Taroccoesbrocco
5,14761839
edited Jan 2 at 18:51
Taroccoesbrocco
5,14761839
5,14761839
asked Jan 2 at 12:11
MaicakeMaicake
615
asked Jan 2 at 12:11
MaicakeMaicake
615
asked Jan 2 at 12:11
MaicakeMaicake
615
615
1
$begingroup$
$D lor (C land E)$ or $D lor (C lor E)$ ?
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 12:33
$begingroup$
Second one, sorry.
$endgroup$
– Maicake
Jan 2 at 12:39
add a comment |
1
$begingroup$
$D lor (C land E)$ or $D lor (C lor E)$ ?
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 12:33
$begingroup$
Second one, sorry.
$endgroup$
– Maicake
Jan 2 at 12:39
1
1
$begingroup$
$D lor (C land E)$ or $D lor (C lor E)$ ?
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 12:33
$begingroup$
$D lor (C land E)$ or $D lor (C lor E)$ ?
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 12:33
$begingroup$
Second one, sorry.
$endgroup$
– Maicake
Jan 2 at 12:39
$begingroup$
Second one, sorry.
$endgroup$
– Maicake
Jan 2 at 12:39
add a comment |
3 Answers
3
active
oldest
votes
$begingroup$
We will work by contradicition, starting assuming :
1) $lnot [D lor (C lor E)]$ --- assumed [a]
2) $lnot D$ --- assumed [b]
3) $lnot E$ --- assumed [c]
4) $A$ --- from 3) and premise-3
5) $lnot D land A$ --- from 2) and 4)
6) $B$ --- from 5) and premise-2
7) $lnot B lor C$ --- from 4) and premise-1
Now we need $lor$-elim on 7)
8) $lnot B$ --- assumed [d1] from 7)
9) $bot$ --- contradiction ! with 6) and 8)
10) $C$ --- assumed [d2] from 7)
11) $C lor E$ --- from 10)
12) $D lor (C lor E)$ --- from 11)
13) $bot$ --- contradiction ! with 1) and 12)
We have derived $bot$ in both cases of the $lor$-elim; thus we have :
14) $bot$ --- from 8)-9) and 10)-13) and 7) by $lor$-elim, discharging assumptions [d1] and [d2]
15) $E$ --- from 3) and 14) by RAA and DN, discharging [c]
16) $C lor E$ --- from 15)
17) $D lor (C lor E)$ --- from 16)
18) $bot$ --- contradiction ! with 1) and 17)
19) $D$ --- from 2) and 18) by RAA and DN, discharging [b]
20) $D lor (C lor E)$ --- from 19)
21) $bot$ --- contradiction ! with 1) and 20)
22) $D lor (C lor E)$ --- from 1) and 21) by RAA and DN, discharging [a].
answered Jan 2 at 13:01
Mauro ALLEGRANZAMauro ALLEGRANZA
64.7k448112
$endgroup$
$begingroup$
thanks a lot. I m not used to this notation where can I find a little example of it use?
$endgroup$
– Maicake
Jan 2 at 13:06
$begingroup$
You are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:40
$begingroup$
@Maicake - do you mean the $bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:41
$begingroup$
I didn't explain well . I mean I usually do this proof drawing trees. It's the first time I see a "linear proof". Also why did you choose to start with RAA?
$endgroup$
– Maicake
Jan 2 at 14:49
1
$begingroup$
@Maicake - because it is cumbersome to draw a tree with the editor here... But it is easy to convert the proof above in tree form: a starting node for every assumption.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:50
add a comment |
$begingroup$
Natural deduction proof of $(A to lnot B lor C), ((lnot D land A) to B), (lnot E to A) vdash D lor (C lor E)$
Here is a skeleton; just flesh it out. The subproofs are mostly proofs by reduction to absurdity, and a proof by cases.
$$deffitch#1#2{~~begin{array}{|l}#1\hline#2end{array}}fitch{(A to lnot B lor C)\ ((lnot D land A) to B)\ (lnot E to A) }{fitch{lnot(Dlor (Clor E))}{fitch{~}{~\~\fitch{~}{fitch{~}{~\~\bot}\~\~\Dlor(Blor E)\bot}\~\fitch{~}{~\Dlor(Clor E)\bot}\~\bot}\~\~\~\Dlor(Clor E)\bot}\~\Dlor (Clor E)}$$
answered Jan 2 at 13:24
Graham KempGraham Kemp
84.8k43378
$endgroup$
add a comment |
$begingroup$
$A implies lnot B lor C$ is equivalent to $lnot Blor C$ or $lnot A$
$lnot D land A implies B $ is equivalent to $B$ or $Dlor lnot A$
$lnot E implies A$ is equivalent to $A$ or $E$
So you want to prove that $lnot A lor lnot Blor C$, $lnot Alor Blor D$, $Alor E$ gives you $Clor Dlor E$. Can you show this last step?
answered Jan 2 at 12:41
Test123Test123
2,762828
$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%2f3059408%2fnatural-deduction-proof-of-a-to-lnot-b-lor-c-lnot-d-land-a-to-b%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
We will work by contradicition, starting assuming :
1) $lnot [D lor (C lor E)]$ --- assumed [a]
2) $lnot D$ --- assumed [b]
3) $lnot E$ --- assumed [c]
4) $A$ --- from 3) and premise-3
5) $lnot D land A$ --- from 2) and 4)
6) $B$ --- from 5) and premise-2
7) $lnot B lor C$ --- from 4) and premise-1
Now we need $lor$-elim on 7)
8) $lnot B$ --- assumed [d1] from 7)
9) $bot$ --- contradiction ! with 6) and 8)
10) $C$ --- assumed [d2] from 7)
11) $C lor E$ --- from 10)
12) $D lor (C lor E)$ --- from 11)
13) $bot$ --- contradiction ! with 1) and 12)
We have derived $bot$ in both cases of the $lor$-elim; thus we have :
14) $bot$ --- from 8)-9) and 10)-13) and 7) by $lor$-elim, discharging assumptions [d1] and [d2]
15) $E$ --- from 3) and 14) by RAA and DN, discharging [c]
16) $C lor E$ --- from 15)
17) $D lor (C lor E)$ --- from 16)
18) $bot$ --- contradiction ! with 1) and 17)
19) $D$ --- from 2) and 18) by RAA and DN, discharging [b]
20) $D lor (C lor E)$ --- from 19)
21) $bot$ --- contradiction ! with 1) and 20)
22) $D lor (C lor E)$ --- from 1) and 21) by RAA and DN, discharging [a].
answered Jan 2 at 13:01
Mauro ALLEGRANZAMauro ALLEGRANZA
64.7k448112
$endgroup$
$begingroup$
thanks a lot. I m not used to this notation where can I find a little example of it use?
$endgroup$
– Maicake
Jan 2 at 13:06
$begingroup$
You are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:40
$begingroup$
@Maicake - do you mean the $bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:41
$begingroup$
I didn't explain well . I mean I usually do this proof drawing trees. It's the first time I see a "linear proof". Also why did you choose to start with RAA?
$endgroup$
– Maicake
Jan 2 at 14:49
1
$begingroup$
@Maicake - because it is cumbersome to draw a tree with the editor here... But it is easy to convert the proof above in tree form: a starting node for every assumption.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:50
add a comment |
$begingroup$
We will work by contradicition, starting assuming :
1) $lnot [D lor (C lor E)]$ --- assumed [a]
2) $lnot D$ --- assumed [b]
3) $lnot E$ --- assumed [c]
4) $A$ --- from 3) and premise-3
5) $lnot D land A$ --- from 2) and 4)
6) $B$ --- from 5) and premise-2
7) $lnot B lor C$ --- from 4) and premise-1
Now we need $lor$-elim on 7)
8) $lnot B$ --- assumed [d1] from 7)
9) $bot$ --- contradiction ! with 6) and 8)
10) $C$ --- assumed [d2] from 7)
11) $C lor E$ --- from 10)
12) $D lor (C lor E)$ --- from 11)
13) $bot$ --- contradiction ! with 1) and 12)
We have derived $bot$ in both cases of the $lor$-elim; thus we have :
14) $bot$ --- from 8)-9) and 10)-13) and 7) by $lor$-elim, discharging assumptions [d1] and [d2]
15) $E$ --- from 3) and 14) by RAA and DN, discharging [c]
16) $C lor E$ --- from 15)
17) $D lor (C lor E)$ --- from 16)
18) $bot$ --- contradiction ! with 1) and 17)
19) $D$ --- from 2) and 18) by RAA and DN, discharging [b]
20) $D lor (C lor E)$ --- from 19)
21) $bot$ --- contradiction ! with 1) and 20)
22) $D lor (C lor E)$ --- from 1) and 21) by RAA and DN, discharging [a].
answered Jan 2 at 13:01
Mauro ALLEGRANZAMauro ALLEGRANZA
64.7k448112
$endgroup$
$begingroup$
thanks a lot. I m not used to this notation where can I find a little example of it use?
$endgroup$
– Maicake
Jan 2 at 13:06
$begingroup$
You are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:40
$begingroup$
@Maicake - do you mean the $bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:41
$begingroup$
I didn't explain well . I mean I usually do this proof drawing trees. It's the first time I see a "linear proof". Also why did you choose to start with RAA?
$endgroup$
– Maicake
Jan 2 at 14:49
1
$begingroup$
@Maicake - because it is cumbersome to draw a tree with the editor here... But it is easy to convert the proof above in tree form: a starting node for every assumption.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:50
add a comment |
$begingroup$
We will work by contradicition, starting assuming :
1) $lnot [D lor (C lor E)]$ --- assumed [a]
2) $lnot D$ --- assumed [b]
3) $lnot E$ --- assumed [c]
4) $A$ --- from 3) and premise-3
5) $lnot D land A$ --- from 2) and 4)
6) $B$ --- from 5) and premise-2
7) $lnot B lor C$ --- from 4) and premise-1
Now we need $lor$-elim on 7)
8) $lnot B$ --- assumed [d1] from 7)
9) $bot$ --- contradiction ! with 6) and 8)
10) $C$ --- assumed [d2] from 7)
11) $C lor E$ --- from 10)
12) $D lor (C lor E)$ --- from 11)
13) $bot$ --- contradiction ! with 1) and 12)
We have derived $bot$ in both cases of the $lor$-elim; thus we have :
14) $bot$ --- from 8)-9) and 10)-13) and 7) by $lor$-elim, discharging assumptions [d1] and [d2]
15) $E$ --- from 3) and 14) by RAA and DN, discharging [c]
16) $C lor E$ --- from 15)
17) $D lor (C lor E)$ --- from 16)
18) $bot$ --- contradiction ! with 1) and 17)
19) $D$ --- from 2) and 18) by RAA and DN, discharging [b]
20) $D lor (C lor E)$ --- from 19)
21) $bot$ --- contradiction ! with 1) and 20)
22) $D lor (C lor E)$ --- from 1) and 21) by RAA and DN, discharging [a].
answered Jan 2 at 13:01
Mauro ALLEGRANZAMauro ALLEGRANZA
64.7k448112
$endgroup$
We will work by contradicition, starting assuming :
1) $lnot [D lor (C lor E)]$ --- assumed [a]
2) $lnot D$ --- assumed [b]
3) $lnot E$ --- assumed [c]
4) $A$ --- from 3) and premise-3
5) $lnot D land A$ --- from 2) and 4)
6) $B$ --- from 5) and premise-2
7) $lnot B lor C$ --- from 4) and premise-1
Now we need $lor$-elim on 7)
8) $lnot B$ --- assumed [d1] from 7)
9) $bot$ --- contradiction ! with 6) and 8)
10) $C$ --- assumed [d2] from 7)
11) $C lor E$ --- from 10)
12) $D lor (C lor E)$ --- from 11)
13) $bot$ --- contradiction ! with 1) and 12)
We have derived $bot$ in both cases of the $lor$-elim; thus we have :
14) $bot$ --- from 8)-9) and 10)-13) and 7) by $lor$-elim, discharging assumptions [d1] and [d2]
15) $E$ --- from 3) and 14) by RAA and DN, discharging [c]
16) $C lor E$ --- from 15)
17) $D lor (C lor E)$ --- from 16)
18) $bot$ --- contradiction ! with 1) and 17)
19) $D$ --- from 2) and 18) by RAA and DN, discharging [b]
20) $D lor (C lor E)$ --- from 19)
21) $bot$ --- contradiction ! with 1) and 20)
22) $D lor (C lor E)$ --- from 1) and 21) by RAA and DN, discharging [a].
answered Jan 2 at 13:01
Mauro ALLEGRANZAMauro ALLEGRANZA
64.7k448112
edited Jan 2 at 14:49
answered Jan 2 at 13:01
Mauro ALLEGRANZAMauro ALLEGRANZA
64.7k448112
answered Jan 2 at 13:01
Mauro ALLEGRANZAMauro ALLEGRANZA
64.7k448112
answered Jan 2 at 13:01
Mauro ALLEGRANZAMauro ALLEGRANZA
64.7k448112
64.7k448112
$begingroup$
thanks a lot. I m not used to this notation where can I find a little example of it use?
$endgroup$
– Maicake
Jan 2 at 13:06
$begingroup$
You are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:40
$begingroup$
@Maicake - do you mean the $bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:41
$begingroup$
I didn't explain well . I mean I usually do this proof drawing trees. It's the first time I see a "linear proof". Also why did you choose to start with RAA?
$endgroup$
– Maicake
Jan 2 at 14:49
1
$begingroup$
@Maicake - because it is cumbersome to draw a tree with the editor here... But it is easy to convert the proof above in tree form: a starting node for every assumption.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:50
add a comment |
$begingroup$
thanks a lot. I m not used to this notation where can I find a little example of it use?
$endgroup$
– Maicake
Jan 2 at 13:06
$begingroup$
You are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:40
$begingroup$
@Maicake - do you mean the $bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:41
$begingroup$
I didn't explain well . I mean I usually do this proof drawing trees. It's the first time I see a "linear proof". Also why did you choose to start with RAA?
$endgroup$
– Maicake
Jan 2 at 14:49
1
$begingroup$
@Maicake - because it is cumbersome to draw a tree with the editor here... But it is easy to convert the proof above in tree form: a starting node for every assumption.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:50
$begingroup$
thanks a lot. I m not used to this notation where can I find a little example of it use?
$endgroup$
– Maicake
Jan 2 at 13:06
$begingroup$
thanks a lot. I m not used to this notation where can I find a little example of it use?
$endgroup$
– Maicake
Jan 2 at 13:06
$begingroup$
You are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:40
$begingroup$
You are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:40
$begingroup$
@Maicake - do you mean the $bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:41
$begingroup$
@Maicake - do you mean the $bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:41
$begingroup$
I didn't explain well . I mean I usually do this proof drawing trees. It's the first time I see a "linear proof". Also why did you choose to start with RAA?
$endgroup$
– Maicake
Jan 2 at 14:49
$begingroup$
I didn't explain well . I mean I usually do this proof drawing trees. It's the first time I see a "linear proof". Also why did you choose to start with RAA?
$endgroup$
– Maicake
Jan 2 at 14:49
1
1
$begingroup$
@Maicake - because it is cumbersome to draw a tree with the editor here... But it is easy to convert the proof above in tree form: a starting node for every assumption.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:50
$begingroup$
@Maicake - because it is cumbersome to draw a tree with the editor here... But it is easy to convert the proof above in tree form: a starting node for every assumption.
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 14:50
add a comment |
$begingroup$
Natural deduction proof of $(A to lnot B lor C), ((lnot D land A) to B), (lnot E to A) vdash D lor (C lor E)$
Here is a skeleton; just flesh it out. The subproofs are mostly proofs by reduction to absurdity, and a proof by cases.
$$deffitch#1#2{~~begin{array}{|l}#1\hline#2end{array}}fitch{(A to lnot B lor C)\ ((lnot D land A) to B)\ (lnot E to A) }{fitch{lnot(Dlor (Clor E))}{fitch{~}{~\~\fitch{~}{fitch{~}{~\~\bot}\~\~\Dlor(Blor E)\bot}\~\fitch{~}{~\Dlor(Clor E)\bot}\~\bot}\~\~\~\Dlor(Clor E)\bot}\~\Dlor (Clor E)}$$
answered Jan 2 at 13:24
Graham KempGraham Kemp
84.8k43378
$endgroup$
add a comment |
$begingroup$
Natural deduction proof of $(A to lnot B lor C), ((lnot D land A) to B), (lnot E to A) vdash D lor (C lor E)$
Here is a skeleton; just flesh it out. The subproofs are mostly proofs by reduction to absurdity, and a proof by cases.
$$deffitch#1#2{~~begin{array}{|l}#1\hline#2end{array}}fitch{(A to lnot B lor C)\ ((lnot D land A) to B)\ (lnot E to A) }{fitch{lnot(Dlor (Clor E))}{fitch{~}{~\~\fitch{~}{fitch{~}{~\~\bot}\~\~\Dlor(Blor E)\bot}\~\fitch{~}{~\Dlor(Clor E)\bot}\~\bot}\~\~\~\Dlor(Clor E)\bot}\~\Dlor (Clor E)}$$
answered Jan 2 at 13:24
Graham KempGraham Kemp
84.8k43378
$endgroup$
add a comment |
$begingroup$
Natural deduction proof of $(A to lnot B lor C), ((lnot D land A) to B), (lnot E to A) vdash D lor (C lor E)$
Here is a skeleton; just flesh it out. The subproofs are mostly proofs by reduction to absurdity, and a proof by cases.
$$deffitch#1#2{~~begin{array}{|l}#1\hline#2end{array}}fitch{(A to lnot B lor C)\ ((lnot D land A) to B)\ (lnot E to A) }{fitch{lnot(Dlor (Clor E))}{fitch{~}{~\~\fitch{~}{fitch{~}{~\~\bot}\~\~\Dlor(Blor E)\bot}\~\fitch{~}{~\Dlor(Clor E)\bot}\~\bot}\~\~\~\Dlor(Clor E)\bot}\~\Dlor (Clor E)}$$
answered Jan 2 at 13:24
Graham KempGraham Kemp
84.8k43378
$endgroup$
Natural deduction proof of $(A to lnot B lor C), ((lnot D land A) to B), (lnot E to A) vdash D lor (C lor E)$
Here is a skeleton; just flesh it out. The subproofs are mostly proofs by reduction to absurdity, and a proof by cases.
$$deffitch#1#2{~~begin{array}{|l}#1\hline#2end{array}}fitch{(A to lnot B lor C)\ ((lnot D land A) to B)\ (lnot E to A) }{fitch{lnot(Dlor (Clor E))}{fitch{~}{~\~\fitch{~}{fitch{~}{~\~\bot}\~\~\Dlor(Blor E)\bot}\~\fitch{~}{~\Dlor(Clor E)\bot}\~\bot}\~\~\~\Dlor(Clor E)\bot}\~\Dlor (Clor E)}$$
answered Jan 2 at 13:24
Graham KempGraham Kemp
84.8k43378
answered Jan 2 at 13:24
Graham KempGraham Kemp
84.8k43378
answered Jan 2 at 13:24
Graham KempGraham Kemp
84.8k43378
answered Jan 2 at 13:24
Graham KempGraham Kemp
84.8k43378
84.8k43378
add a comment |
add a comment |
$begingroup$
$A implies lnot B lor C$ is equivalent to $lnot Blor C$ or $lnot A$
$lnot D land A implies B $ is equivalent to $B$ or $Dlor lnot A$
$lnot E implies A$ is equivalent to $A$ or $E$
So you want to prove that $lnot A lor lnot Blor C$, $lnot Alor Blor D$, $Alor E$ gives you $Clor Dlor E$. Can you show this last step?
answered Jan 2 at 12:41
Test123Test123
2,762828
$endgroup$
add a comment |
$begingroup$
$A implies lnot B lor C$ is equivalent to $lnot Blor C$ or $lnot A$
$lnot D land A implies B $ is equivalent to $B$ or $Dlor lnot A$
$lnot E implies A$ is equivalent to $A$ or $E$
So you want to prove that $lnot A lor lnot Blor C$, $lnot Alor Blor D$, $Alor E$ gives you $Clor Dlor E$. Can you show this last step?
answered Jan 2 at 12:41
Test123Test123
2,762828
$endgroup$
add a comment |
$begingroup$
$A implies lnot B lor C$ is equivalent to $lnot Blor C$ or $lnot A$
$lnot D land A implies B $ is equivalent to $B$ or $Dlor lnot A$
$lnot E implies A$ is equivalent to $A$ or $E$
So you want to prove that $lnot A lor lnot Blor C$, $lnot Alor Blor D$, $Alor E$ gives you $Clor Dlor E$. Can you show this last step?
answered Jan 2 at 12:41
Test123Test123
2,762828
$endgroup$
$A implies lnot B lor C$ is equivalent to $lnot Blor C$ or $lnot A$
$lnot D land A implies B $ is equivalent to $B$ or $Dlor lnot A$
$lnot E implies A$ is equivalent to $A$ or $E$
So you want to prove that $lnot A lor lnot Blor C$, $lnot Alor Blor D$, $Alor E$ gives you $Clor Dlor E$. Can you show this last step?
answered Jan 2 at 12:41
Test123Test123
2,762828
answered Jan 2 at 12:41
Test123Test123
2,762828
answered Jan 2 at 12:41
Test123Test123
2,762828
answered Jan 2 at 12:41
Test123Test123
2,762828
2,762828
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%2f3059408%2fnatural-deduction-proof-of-a-to-lnot-b-lor-c-lnot-d-land-a-to-b%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
1
$begingroup$
$D lor (C land E)$ or $D lor (C lor E)$ ?
$endgroup$
– Mauro ALLEGRANZA
Jan 2 at 12:33
$begingroup$
Second one, sorry.
$endgroup$
– Maicake
Jan 2 at 12:39