Proving the distributive law with natural deduction
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
I have to prove the following logical equivalence, also known as one of the two distributive laws:
$$
P vee (Q wedge R) equiv (P vee Q) wedge (P vee R)
$$
I have solved the first part, $P lor (Q land R) to (P lor Q) land (P lor R)$, like so:
But now that I'm trying to solve the next part, $(P lor Q) land (P lor R) rightarrow P lor (Q land R)$, I keep getting stuck somewhere with a disjunction elimination where I'm trying to prove something like $P$ with only $Q$ and $(P ∨ Q) ∧ (P ∨ R)$.
So how can I prove $(P lor Q) land (P lor R) rightarrow P lor (Q land R)$ using a proof tree, like shown above? Thanks!
logic proof-writing proof-theory natural-deduction formal-proofs
edited Sep 7 at 21:56
Taroccoesbrocco
3,96961535
asked Sep 7 at 20:04
tobloef
1084
add a comment |Â
up vote
1
down vote
favorite
I have to prove the following logical equivalence, also known as one of the two distributive laws:
$$
P vee (Q wedge R) equiv (P vee Q) wedge (P vee R)
$$
I have solved the first part, $P lor (Q land R) to (P lor Q) land (P lor R)$, like so:
But now that I'm trying to solve the next part, $(P lor Q) land (P lor R) rightarrow P lor (Q land R)$, I keep getting stuck somewhere with a disjunction elimination where I'm trying to prove something like $P$ with only $Q$ and $(P ∨ Q) ∧ (P ∨ R)$.
So how can I prove $(P lor Q) land (P lor R) rightarrow P lor (Q land R)$ using a proof tree, like shown above? Thanks!
logic proof-writing proof-theory natural-deduction formal-proofs
edited Sep 7 at 21:56
Taroccoesbrocco
3,96961535
asked Sep 7 at 20:04
tobloef
1084
Unpack the premise with $land$-elim; then two "nested" $lor$-elim. Three cases : 1) $P$ : done. 2) $Q$ then $P$ : done. 3) $Q$ then $R$ : done.
– Mauro ALLEGRANZA
Sep 7 at 20:11
@MauroALLEGRANZA Thank you for commenting, but I'm not sure I understand. After I've used implication introduction on the premise ($P∨(Q∧R)$), wouldn't I have to use disjunction elimination before being able to do a conjunction elimination as you suggest?
– tobloef
Sep 7 at 20:43
add a comment |Â
up vote
1
down vote
favorite
up vote
1
down vote
favorite
I have to prove the following logical equivalence, also known as one of the two distributive laws:
$$
P vee (Q wedge R) equiv (P vee Q) wedge (P vee R)
$$
I have solved the first part, $P lor (Q land R) to (P lor Q) land (P lor R)$, like so:
But now that I'm trying to solve the next part, $(P lor Q) land (P lor R) rightarrow P lor (Q land R)$, I keep getting stuck somewhere with a disjunction elimination where I'm trying to prove something like $P$ with only $Q$ and $(P ∨ Q) ∧ (P ∨ R)$.
So how can I prove $(P lor Q) land (P lor R) rightarrow P lor (Q land R)$ using a proof tree, like shown above? Thanks!
logic proof-writing proof-theory natural-deduction formal-proofs
edited Sep 7 at 21:56
Taroccoesbrocco
3,96961535
asked Sep 7 at 20:04
tobloef
1084
I have to prove the following logical equivalence, also known as one of the two distributive laws:
$$
P vee (Q wedge R) equiv (P vee Q) wedge (P vee R)
$$
I have solved the first part, $P lor (Q land R) to (P lor Q) land (P lor R)$, like so:
But now that I'm trying to solve the next part, $(P lor Q) land (P lor R) rightarrow P lor (Q land R)$, I keep getting stuck somewhere with a disjunction elimination where I'm trying to prove something like $P$ with only $Q$ and $(P ∨ Q) ∧ (P ∨ R)$.
So how can I prove $(P lor Q) land (P lor R) rightarrow P lor (Q land R)$ using a proof tree, like shown above? Thanks!
logic proof-writing proof-theory natural-deduction formal-proofs
logic proof-writing proof-theory natural-deduction formal-proofs
edited Sep 7 at 21:56
Taroccoesbrocco
3,96961535
asked Sep 7 at 20:04
tobloef
1084
edited Sep 7 at 21:56
Taroccoesbrocco
3,96961535
asked Sep 7 at 20:04
tobloef
1084
edited Sep 7 at 21:56
Taroccoesbrocco
3,96961535
edited Sep 7 at 21:56
Taroccoesbrocco
3,96961535
edited Sep 7 at 21:56
Taroccoesbrocco
3,96961535
3,96961535
asked Sep 7 at 20:04
tobloef
1084
asked Sep 7 at 20:04
tobloef
1084
asked Sep 7 at 20:04
tobloef
1084
1084
Unpack the premise with $land$-elim; then two "nested" $lor$-elim. Three cases : 1) $P$ : done. 2) $Q$ then $P$ : done. 3) $Q$ then $R$ : done.
– Mauro ALLEGRANZA
Sep 7 at 20:11
@MauroALLEGRANZA Thank you for commenting, but I'm not sure I understand. After I've used implication introduction on the premise ($P∨(Q∧R)$), wouldn't I have to use disjunction elimination before being able to do a conjunction elimination as you suggest?
– tobloef
Sep 7 at 20:43
add a comment |Â
Unpack the premise with $land$-elim; then two "nested" $lor$-elim. Three cases : 1) $P$ : done. 2) $Q$ then $P$ : done. 3) $Q$ then $R$ : done.
– Mauro ALLEGRANZA
Sep 7 at 20:11
@MauroALLEGRANZA Thank you for commenting, but I'm not sure I understand. After I've used implication introduction on the premise ($P∨(Q∧R)$), wouldn't I have to use disjunction elimination before being able to do a conjunction elimination as you suggest?
– tobloef
Sep 7 at 20:43
Unpack the premise with $land$-elim; then two "nested" $lor$-elim. Three cases : 1) $P$ : done. 2) $Q$ then $P$ : done. 3) $Q$ then $R$ : done.
– Mauro ALLEGRANZA
Sep 7 at 20:11
Unpack the premise with $land$-elim; then two "nested" $lor$-elim. Three cases : 1) $P$ : done. 2) $Q$ then $P$ : done. 3) $Q$ then $R$ : done.
– Mauro ALLEGRANZA
Sep 7 at 20:11
@MauroALLEGRANZA Thank you for commenting, but I'm not sure I understand. After I've used implication introduction on the premise ($P∨(Q∧R)$), wouldn't I have to use disjunction elimination before being able to do a conjunction elimination as you suggest?
– tobloef
Sep 7 at 20:43
@MauroALLEGRANZA Thank you for commenting, but I'm not sure I understand. After I've used implication introduction on the premise ($P∨(Q∧R)$), wouldn't I have to use disjunction elimination before being able to do a conjunction elimination as you suggest?
– tobloef
Sep 7 at 20:43
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
1
down vote
accepted
Let $A = (P lor Q) land (P lor R)$ and $B = P lor (Q land R)$.
The following is a derivation in natural deduction of $B$ from $A$.
$$
dfracdfracAP lor Qland_e_1 quad dfrac[P]^*Blor_i_1 quad dfracdfracAP lor Rland_e_2 quad dfrac[P]^**Blor_i_1 quad dfracdfrac[Q]^* quad [R]^**Q land Rland_iBlor_i_2Blor_e^**B lor_e^*
$$
Note that the derivation above is based on two nested applications of the rule $lor_e$.
From the derivation above you obtain the derivation of $A to B$ (without assumptions) by adding a $to_i$ rule as last rule, discharging the two occurrences of $A$.
answered Sep 7 at 21:45
Taroccoesbrocco
3,96961535
Thank you so much. Re-writing your answer in the same style as my previous example results in this final proof tree.
– tobloef
Sep 7 at 23:03
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
Let $A = (P lor Q) land (P lor R)$ and $B = P lor (Q land R)$.
The following is a derivation in natural deduction of $B$ from $A$.
$$
dfracdfracAP lor Qland_e_1 quad dfrac[P]^*Blor_i_1 quad dfracdfracAP lor Rland_e_2 quad dfrac[P]^**Blor_i_1 quad dfracdfrac[Q]^* quad [R]^**Q land Rland_iBlor_i_2Blor_e^**B lor_e^*
$$
Note that the derivation above is based on two nested applications of the rule $lor_e$.
From the derivation above you obtain the derivation of $A to B$ (without assumptions) by adding a $to_i$ rule as last rule, discharging the two occurrences of $A$.
answered Sep 7 at 21:45
Taroccoesbrocco
3,96961535
Thank you so much. Re-writing your answer in the same style as my previous example results in this final proof tree.
– tobloef
Sep 7 at 23:03
add a comment |Â
up vote
1
down vote
accepted
Let $A = (P lor Q) land (P lor R)$ and $B = P lor (Q land R)$.
The following is a derivation in natural deduction of $B$ from $A$.
$$
dfracdfracAP lor Qland_e_1 quad dfrac[P]^*Blor_i_1 quad dfracdfracAP lor Rland_e_2 quad dfrac[P]^**Blor_i_1 quad dfracdfrac[Q]^* quad [R]^**Q land Rland_iBlor_i_2Blor_e^**B lor_e^*
$$
Note that the derivation above is based on two nested applications of the rule $lor_e$.
From the derivation above you obtain the derivation of $A to B$ (without assumptions) by adding a $to_i$ rule as last rule, discharging the two occurrences of $A$.
answered Sep 7 at 21:45
Taroccoesbrocco
3,96961535
Thank you so much. Re-writing your answer in the same style as my previous example results in this final proof tree.
– tobloef
Sep 7 at 23:03
add a comment |Â
up vote
1
down vote
accepted
up vote
1
down vote
accepted
Let $A = (P lor Q) land (P lor R)$ and $B = P lor (Q land R)$.
The following is a derivation in natural deduction of $B$ from $A$.
$$
dfracdfracAP lor Qland_e_1 quad dfrac[P]^*Blor_i_1 quad dfracdfracAP lor Rland_e_2 quad dfrac[P]^**Blor_i_1 quad dfracdfrac[Q]^* quad [R]^**Q land Rland_iBlor_i_2Blor_e^**B lor_e^*
$$
Note that the derivation above is based on two nested applications of the rule $lor_e$.
From the derivation above you obtain the derivation of $A to B$ (without assumptions) by adding a $to_i$ rule as last rule, discharging the two occurrences of $A$.
answered Sep 7 at 21:45
Taroccoesbrocco
3,96961535
Let $A = (P lor Q) land (P lor R)$ and $B = P lor (Q land R)$.
The following is a derivation in natural deduction of $B$ from $A$.
$$
dfracdfracAP lor Qland_e_1 quad dfrac[P]^*Blor_i_1 quad dfracdfracAP lor Rland_e_2 quad dfrac[P]^**Blor_i_1 quad dfracdfrac[Q]^* quad [R]^**Q land Rland_iBlor_i_2Blor_e^**B lor_e^*
$$
Note that the derivation above is based on two nested applications of the rule $lor_e$.
From the derivation above you obtain the derivation of $A to B$ (without assumptions) by adding a $to_i$ rule as last rule, discharging the two occurrences of $A$.
answered Sep 7 at 21:45
Taroccoesbrocco
3,96961535
edited Sep 7 at 21:53
answered Sep 7 at 21:45
Taroccoesbrocco
3,96961535
answered Sep 7 at 21:45
Taroccoesbrocco
3,96961535
answered Sep 7 at 21:45
Taroccoesbrocco
3,96961535
3,96961535
Thank you so much. Re-writing your answer in the same style as my previous example results in this final proof tree.
– tobloef
Sep 7 at 23:03
add a comment |Â
Thank you so much. Re-writing your answer in the same style as my previous example results in this final proof tree.
– tobloef
Sep 7 at 23:03
Thank you so much. Re-writing your answer in the same style as my previous example results in this final proof tree.
– tobloef
Sep 7 at 23:03
Thank you so much. Re-writing your answer in the same style as my previous example results in this final proof tree.
– tobloef
Sep 7 at 23:03
add a comment |Â
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
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2909006%2fproving-the-distributive-law-with-natural-deduction%23new-answer', 'question_page');
);
Post as a guest
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
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
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
Unpack the premise with $land$-elim; then two "nested" $lor$-elim. Three cases : 1) $P$ : done. 2) $Q$ then $P$ : done. 3) $Q$ then $R$ : done.
– Mauro ALLEGRANZA
Sep 7 at 20:11
@MauroALLEGRANZA Thank you for commenting, but I'm not sure I understand. After I've used implication introduction on the premise ($P∨(Q∧R)$), wouldn't I have to use disjunction elimination before being able to do a conjunction elimination as you suggest?
– tobloef
Sep 7 at 20:43