Assistance in completing the proof: (P → Q)∧(Q → R) is equivalent to (P → R)∧ [(P ↔ Q) ∨ (R ↔...
$begingroup$
There is a proof in a previous thread that converts the two expressions (P → Q)∧(Q → R) and (P → R)∧ [(P ↔ Q) ∨ (R ↔ Q)] to a CNF-formula thereby proving their equivalencies.
I am approaching the proof from an entirely different proof technique and am stuck. Instead of using truth tables, or converting these two expressions to the same CNF/DNF-formulas I'd rather prove this by using logical equivalencies.
I am having trouble filling in the missing steps, as I get into a distributive property loop in my attempt to group and eliminate terms.
Can someone show me how to complete the proof that I started and help me fill in my missing steps?
Below is my proof attempt:
$(P to R)land [(P defliff{leftrightarrow}liff Q) lor (R liff Q)] =$
$(lnot P lor R) land [(Pto Q) land (Qto P) lor (Rto Q) land (Qto R)] =$
$(lnot P lor R) land [(Pto Q) land (lnot Ptolnot Q) lor (Rto Q) land (lnot Rtolnot Q)] =$
$(lnot P lor R) land [(lnot P lor Q) land (lnotlnot P lorlnot Q) lor (lnot R lor Q) land (lnotlnot R lor lnot Q)] =$
$(lnot P lor R) land [(lnot P lor Q) land (P lorlnot Q) lor (lnot R lor Q) land (R lorlnot Q)] =$
$(lnot P lor R) land [((lnot P lor Q) land P) lor (lnot P lor Q) landlnot Q) lor (lnot R lor Q) land R) lor (lnot R lor Q) landlnot Q)] =$
$(lnot P lor R) land [(P land(lnot P lor Q)) lor (lnot Q land (lnot P lor Q)) lor (R land (lnot R lor Q)) lor (lnot Q land (lnot R lor Q))] =$
…steps...
$(lnot P lor Q) land (lnot Rtolnot Q)=$
$(lnot P lor Q) land (lnotlnot R lorlnot Q)=$
$(lnot P lor Q) land (R lorlnot Q)=$
$(P to Q)land (Q to R)$
Q.E.D
I would like to see how to complete the "steps" part, as this is where my chain of distributive property loops begin that don't lead me closer to the conclusion. Could someone show me a complete proof?
logic propositional-calculus boolean-algebra
$endgroup$
add a comment |
$begingroup$
There is a proof in a previous thread that converts the two expressions (P → Q)∧(Q → R) and (P → R)∧ [(P ↔ Q) ∨ (R ↔ Q)] to a CNF-formula thereby proving their equivalencies.
I am approaching the proof from an entirely different proof technique and am stuck. Instead of using truth tables, or converting these two expressions to the same CNF/DNF-formulas I'd rather prove this by using logical equivalencies.
I am having trouble filling in the missing steps, as I get into a distributive property loop in my attempt to group and eliminate terms.
Can someone show me how to complete the proof that I started and help me fill in my missing steps?
Below is my proof attempt:
$(P to R)land [(P defliff{leftrightarrow}liff Q) lor (R liff Q)] =$
$(lnot P lor R) land [(Pto Q) land (Qto P) lor (Rto Q) land (Qto R)] =$
$(lnot P lor R) land [(Pto Q) land (lnot Ptolnot Q) lor (Rto Q) land (lnot Rtolnot Q)] =$
$(lnot P lor R) land [(lnot P lor Q) land (lnotlnot P lorlnot Q) lor (lnot R lor Q) land (lnotlnot R lor lnot Q)] =$
$(lnot P lor R) land [(lnot P lor Q) land (P lorlnot Q) lor (lnot R lor Q) land (R lorlnot Q)] =$
$(lnot P lor R) land [((lnot P lor Q) land P) lor (lnot P lor Q) landlnot Q) lor (lnot R lor Q) land R) lor (lnot R lor Q) landlnot Q)] =$
$(lnot P lor R) land [(P land(lnot P lor Q)) lor (lnot Q land (lnot P lor Q)) lor (R land (lnot R lor Q)) lor (lnot Q land (lnot R lor Q))] =$
…steps...
$(lnot P lor Q) land (lnot Rtolnot Q)=$
$(lnot P lor Q) land (lnotlnot R lorlnot Q)=$
$(lnot P lor Q) land (R lorlnot Q)=$
$(P to Q)land (Q to R)$
Q.E.D
I would like to see how to complete the "steps" part, as this is where my chain of distributive property loops begin that don't lead me closer to the conclusion. Could someone show me a complete proof?
logic propositional-calculus boolean-algebra
$endgroup$
add a comment |
$begingroup$
There is a proof in a previous thread that converts the two expressions (P → Q)∧(Q → R) and (P → R)∧ [(P ↔ Q) ∨ (R ↔ Q)] to a CNF-formula thereby proving their equivalencies.
I am approaching the proof from an entirely different proof technique and am stuck. Instead of using truth tables, or converting these two expressions to the same CNF/DNF-formulas I'd rather prove this by using logical equivalencies.
I am having trouble filling in the missing steps, as I get into a distributive property loop in my attempt to group and eliminate terms.
Can someone show me how to complete the proof that I started and help me fill in my missing steps?
Below is my proof attempt:
$(P to R)land [(P defliff{leftrightarrow}liff Q) lor (R liff Q)] =$
$(lnot P lor R) land [(Pto Q) land (Qto P) lor (Rto Q) land (Qto R)] =$
$(lnot P lor R) land [(Pto Q) land (lnot Ptolnot Q) lor (Rto Q) land (lnot Rtolnot Q)] =$
$(lnot P lor R) land [(lnot P lor Q) land (lnotlnot P lorlnot Q) lor (lnot R lor Q) land (lnotlnot R lor lnot Q)] =$
$(lnot P lor R) land [(lnot P lor Q) land (P lorlnot Q) lor (lnot R lor Q) land (R lorlnot Q)] =$
$(lnot P lor R) land [((lnot P lor Q) land P) lor (lnot P lor Q) landlnot Q) lor (lnot R lor Q) land R) lor (lnot R lor Q) landlnot Q)] =$
$(lnot P lor R) land [(P land(lnot P lor Q)) lor (lnot Q land (lnot P lor Q)) lor (R land (lnot R lor Q)) lor (lnot Q land (lnot R lor Q))] =$
…steps...
$(lnot P lor Q) land (lnot Rtolnot Q)=$
$(lnot P lor Q) land (lnotlnot R lorlnot Q)=$
$(lnot P lor Q) land (R lorlnot Q)=$
$(P to Q)land (Q to R)$
Q.E.D
I would like to see how to complete the "steps" part, as this is where my chain of distributive property loops begin that don't lead me closer to the conclusion. Could someone show me a complete proof?
logic propositional-calculus boolean-algebra
$endgroup$
There is a proof in a previous thread that converts the two expressions (P → Q)∧(Q → R) and (P → R)∧ [(P ↔ Q) ∨ (R ↔ Q)] to a CNF-formula thereby proving their equivalencies.
I am approaching the proof from an entirely different proof technique and am stuck. Instead of using truth tables, or converting these two expressions to the same CNF/DNF-formulas I'd rather prove this by using logical equivalencies.
I am having trouble filling in the missing steps, as I get into a distributive property loop in my attempt to group and eliminate terms.
Can someone show me how to complete the proof that I started and help me fill in my missing steps?
Below is my proof attempt:
$(P to R)land [(P defliff{leftrightarrow}liff Q) lor (R liff Q)] =$
$(lnot P lor R) land [(Pto Q) land (Qto P) lor (Rto Q) land (Qto R)] =$
$(lnot P lor R) land [(Pto Q) land (lnot Ptolnot Q) lor (Rto Q) land (lnot Rtolnot Q)] =$
$(lnot P lor R) land [(lnot P lor Q) land (lnotlnot P lorlnot Q) lor (lnot R lor Q) land (lnotlnot R lor lnot Q)] =$
$(lnot P lor R) land [(lnot P lor Q) land (P lorlnot Q) lor (lnot R lor Q) land (R lorlnot Q)] =$
$(lnot P lor R) land [((lnot P lor Q) land P) lor (lnot P lor Q) landlnot Q) lor (lnot R lor Q) land R) lor (lnot R lor Q) landlnot Q)] =$
$(lnot P lor R) land [(P land(lnot P lor Q)) lor (lnot Q land (lnot P lor Q)) lor (R land (lnot R lor Q)) lor (lnot Q land (lnot R lor Q))] =$
…steps...
$(lnot P lor Q) land (lnot Rtolnot Q)=$
$(lnot P lor Q) land (lnotlnot R lorlnot Q)=$
$(lnot P lor Q) land (R lorlnot Q)=$
$(P to Q)land (Q to R)$
Q.E.D
I would like to see how to complete the "steps" part, as this is where my chain of distributive property loops begin that don't lead me closer to the conclusion. Could someone show me a complete proof?
logic propositional-calculus boolean-algebra
logic propositional-calculus boolean-algebra
edited Jan 29 at 22:56
Graham Kemp
87.6k43578
87.6k43578
asked Jan 29 at 19:08
tree_traversaltree_traversal
386
386
add a comment |
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
Here are some useful but elementary equivalence principles:
Complement
$$P lor neg P Leftrightarrow top$$
$$P land neg P Leftrightarrow bot$$
Annihilation
$$P lor top Leftrightarrow top$$
$$P land bot Leftrightarrow bot$$
Identity
$$P land top Leftrightarrow P$$
$$P lor bot Leftrightarrow P$$
Idempotence
$$P lor P = P$$
$$P land P = P$$
Also, as you noticed, the whole big right terms does indeed not get you anywhere ... you need to work in the left term $neg P lor R$
So, starting a few lines from before you get 'stuck' (because indeed, you're just going in loops at that point) (and also throwing in some necessary parentheses):
$(neg P lor R) land [color{red}((neg P lor Q) land (P lor neg Q)color{red}) lor color{red}((neg R lor Q) land (R lor neg Q)color{red})] =$
$(neg P land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) lor (R land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) =$
$[neg P land ((neg P lor Q) land (P lor neg Q))] lor [neg P land ((neg R lor Q) land (R lor neg Q))] lor [R land ((neg P lor Q) land (P lor neg Q))] lor [R land ((neg R lor Q) land (R lor neg Q))] =$
(dropping unncessary parentheses)
$[neg P land (neg P lor Q) land (P lor neg Q)] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land (neg R lor Q) land (R lor neg Q)]$
OK, now two handy laws are:
Absorption
$$P land (P lor Q) = P$$
Reduction
$$P land (neg P lor Q) = P land Q$$
Applying these, we get:
$[neg P land neg Q] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land Q ]$
OK, and now 'unDistribute' the $neg P $ and the $R$:
$= [neg P land (neg Q lor ((neg R lor Q) land (R lor neg Q)))] lor [R land (((neg P lor Q) land (P lor neg Q)) lor Q) ]$
and now you can distribute the $neg Q$ and the $Q$:
$= [neg P land (neg Q lor (neg R lor Q)) land (neg Q lor (R lor neg Q))] lor [R land ((neg P lor Q) lor Q) land ((P lor neg Q) lor Q) ] =$
(dropping unncessary parentheses)
$[neg P land (neg Q lor neg R lor Q) land (neg Q lor R lor neg Q)] lor [R land (neg P lor Q lor Q) land (P lor neg Q lor Q) ]$
And now you can use those simplification laws from the start of my post:
(Complement:)
$[neg P land (neg R lor top) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor top) ]$
(Annihilation:)
$=[neg P land top land (R lor neg Q)] lor [R land (neg P lor Q) land top ]$
(Identity:)
$=[neg P land (R lor neg Q)] lor [R land (neg P lor Q)]$
(Distribution:)
$=(neg P land R) lor (neg P land neg Q) lor (R land neg P) lor (R land Q)$
(Commutation:)
$=(neg P land R) lor (neg P land neg Q) lor (neg P land R) lor (R land Q)$
(Idempotence:)
$=(neg P land R) lor (neg P land neg Q) lor (R land Q)$
(Distribution 2*2*2:)
$=(neg P lor neg P lor R) land (neg P lor neg Q lor R) land (neg P lor neg P lor Q) land (neg P lor neg Q lor Q) land (R lor neg P lor R) land (R lor neg Q lor R) land (R lor neg P lor Q) land (R lor neg Q lor Q)$
(Complement:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor top) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land (R lor top)$
(Annihilation:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land top land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land top$
(Identity:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) $
(two Absorptions and an Idempotence:)
$=(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
Phew! Almost there ....
Now, use:
Adjacency
$$P = (P lor Q) land (P lor neg Q)$$
Applied to where we were:
$(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
(Adjacency:)
$=(neg P lor R lor Q) land (neg P lor R lor neg Q) land (neg P lor Q) land (neg Q lor R)$
(Two Absorptions)
$(neg P lor Q) land (neg Q lor R)$
.. and finally we're there! Sheesh!
$endgroup$
$begingroup$
Comments are not for extended discussion; this conversation has been moved to chat.
$endgroup$
– Aloizio Macedo♦
Jan 30 at 17:21
add a comment |
$begingroup$
Your approach - which I continued in my first Answer - effectively puts the statements into their CNF ... which is what you were trying to avoid.
So, I figure I would give an Alternative answer, working with the whole conditionals, rather than breaking the statements down all the way to literals.
Now, this is going to require some equivalence principles involving conditionals. Notice that in my other answer I showed that
$$(neg P lor R) land (neg P lor Q) land (neg Q lor R) = (neg P lor Q) land (neg Q lor R)$$
This equivalence is actually known to be the Consensus Theorem, which also has a conditional form:
Conditional Consensus
$$(P rightarrow R) land (P rightarrow Q) land (Q rightarrow R) = (P rightarrow Q) land (Q rightarrow R)$$
OK, that's the key equivalence I'll be using, but I want one more, which is:
Conditional Tautology
$$(P rightarrow Q) lor (Q rightarrow R) = top$$
OK, with that, here goes:
$(P rightarrow R) land ((P leftrightarrow Q) lor (Q leftrightarrow R))=$
(Work out biconditional as two conditionals:)
$(P rightarrow R) land (((P rightarrow Q) land (Q rightarrow P)) lor ((Q rightarrow R) land (R rightarrow Q)))=$
(DIstribution of $P rightarrow R$:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q))=$
(Consensus Conditional form!)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P) land (Q rightarrow R)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q) land (P rightarrow Q))$
(Undistribution of three terms in common:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow R)) land ((Q rightarrow P) lor (R rightarrow Q))=$
(conditional Consensus and Conditional Tautology:)
$((P rightarrow Q) land (Q rightarrow R)) land top=$
$(P rightarrow Q) land (Q rightarrow R)$
Ah, much better!
$endgroup$
add a comment |
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%2f3092595%2fassistance-in-completing-the-proof-p-%25e2%2586%2592-q%25e2%2588%25a7q-%25e2%2586%2592-r-is-equivalent-to-p-%25e2%2586%2592-r%25e2%2588%25a7%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$
Here are some useful but elementary equivalence principles:
Complement
$$P lor neg P Leftrightarrow top$$
$$P land neg P Leftrightarrow bot$$
Annihilation
$$P lor top Leftrightarrow top$$
$$P land bot Leftrightarrow bot$$
Identity
$$P land top Leftrightarrow P$$
$$P lor bot Leftrightarrow P$$
Idempotence
$$P lor P = P$$
$$P land P = P$$
Also, as you noticed, the whole big right terms does indeed not get you anywhere ... you need to work in the left term $neg P lor R$
So, starting a few lines from before you get 'stuck' (because indeed, you're just going in loops at that point) (and also throwing in some necessary parentheses):
$(neg P lor R) land [color{red}((neg P lor Q) land (P lor neg Q)color{red}) lor color{red}((neg R lor Q) land (R lor neg Q)color{red})] =$
$(neg P land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) lor (R land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) =$
$[neg P land ((neg P lor Q) land (P lor neg Q))] lor [neg P land ((neg R lor Q) land (R lor neg Q))] lor [R land ((neg P lor Q) land (P lor neg Q))] lor [R land ((neg R lor Q) land (R lor neg Q))] =$
(dropping unncessary parentheses)
$[neg P land (neg P lor Q) land (P lor neg Q)] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land (neg R lor Q) land (R lor neg Q)]$
OK, now two handy laws are:
Absorption
$$P land (P lor Q) = P$$
Reduction
$$P land (neg P lor Q) = P land Q$$
Applying these, we get:
$[neg P land neg Q] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land Q ]$
OK, and now 'unDistribute' the $neg P $ and the $R$:
$= [neg P land (neg Q lor ((neg R lor Q) land (R lor neg Q)))] lor [R land (((neg P lor Q) land (P lor neg Q)) lor Q) ]$
and now you can distribute the $neg Q$ and the $Q$:
$= [neg P land (neg Q lor (neg R lor Q)) land (neg Q lor (R lor neg Q))] lor [R land ((neg P lor Q) lor Q) land ((P lor neg Q) lor Q) ] =$
(dropping unncessary parentheses)
$[neg P land (neg Q lor neg R lor Q) land (neg Q lor R lor neg Q)] lor [R land (neg P lor Q lor Q) land (P lor neg Q lor Q) ]$
And now you can use those simplification laws from the start of my post:
(Complement:)
$[neg P land (neg R lor top) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor top) ]$
(Annihilation:)
$=[neg P land top land (R lor neg Q)] lor [R land (neg P lor Q) land top ]$
(Identity:)
$=[neg P land (R lor neg Q)] lor [R land (neg P lor Q)]$
(Distribution:)
$=(neg P land R) lor (neg P land neg Q) lor (R land neg P) lor (R land Q)$
(Commutation:)
$=(neg P land R) lor (neg P land neg Q) lor (neg P land R) lor (R land Q)$
(Idempotence:)
$=(neg P land R) lor (neg P land neg Q) lor (R land Q)$
(Distribution 2*2*2:)
$=(neg P lor neg P lor R) land (neg P lor neg Q lor R) land (neg P lor neg P lor Q) land (neg P lor neg Q lor Q) land (R lor neg P lor R) land (R lor neg Q lor R) land (R lor neg P lor Q) land (R lor neg Q lor Q)$
(Complement:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor top) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land (R lor top)$
(Annihilation:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land top land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land top$
(Identity:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) $
(two Absorptions and an Idempotence:)
$=(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
Phew! Almost there ....
Now, use:
Adjacency
$$P = (P lor Q) land (P lor neg Q)$$
Applied to where we were:
$(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
(Adjacency:)
$=(neg P lor R lor Q) land (neg P lor R lor neg Q) land (neg P lor Q) land (neg Q lor R)$
(Two Absorptions)
$(neg P lor Q) land (neg Q lor R)$
.. and finally we're there! Sheesh!
$endgroup$
$begingroup$
Comments are not for extended discussion; this conversation has been moved to chat.
$endgroup$
– Aloizio Macedo♦
Jan 30 at 17:21
add a comment |
$begingroup$
Here are some useful but elementary equivalence principles:
Complement
$$P lor neg P Leftrightarrow top$$
$$P land neg P Leftrightarrow bot$$
Annihilation
$$P lor top Leftrightarrow top$$
$$P land bot Leftrightarrow bot$$
Identity
$$P land top Leftrightarrow P$$
$$P lor bot Leftrightarrow P$$
Idempotence
$$P lor P = P$$
$$P land P = P$$
Also, as you noticed, the whole big right terms does indeed not get you anywhere ... you need to work in the left term $neg P lor R$
So, starting a few lines from before you get 'stuck' (because indeed, you're just going in loops at that point) (and also throwing in some necessary parentheses):
$(neg P lor R) land [color{red}((neg P lor Q) land (P lor neg Q)color{red}) lor color{red}((neg R lor Q) land (R lor neg Q)color{red})] =$
$(neg P land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) lor (R land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) =$
$[neg P land ((neg P lor Q) land (P lor neg Q))] lor [neg P land ((neg R lor Q) land (R lor neg Q))] lor [R land ((neg P lor Q) land (P lor neg Q))] lor [R land ((neg R lor Q) land (R lor neg Q))] =$
(dropping unncessary parentheses)
$[neg P land (neg P lor Q) land (P lor neg Q)] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land (neg R lor Q) land (R lor neg Q)]$
OK, now two handy laws are:
Absorption
$$P land (P lor Q) = P$$
Reduction
$$P land (neg P lor Q) = P land Q$$
Applying these, we get:
$[neg P land neg Q] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land Q ]$
OK, and now 'unDistribute' the $neg P $ and the $R$:
$= [neg P land (neg Q lor ((neg R lor Q) land (R lor neg Q)))] lor [R land (((neg P lor Q) land (P lor neg Q)) lor Q) ]$
and now you can distribute the $neg Q$ and the $Q$:
$= [neg P land (neg Q lor (neg R lor Q)) land (neg Q lor (R lor neg Q))] lor [R land ((neg P lor Q) lor Q) land ((P lor neg Q) lor Q) ] =$
(dropping unncessary parentheses)
$[neg P land (neg Q lor neg R lor Q) land (neg Q lor R lor neg Q)] lor [R land (neg P lor Q lor Q) land (P lor neg Q lor Q) ]$
And now you can use those simplification laws from the start of my post:
(Complement:)
$[neg P land (neg R lor top) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor top) ]$
(Annihilation:)
$=[neg P land top land (R lor neg Q)] lor [R land (neg P lor Q) land top ]$
(Identity:)
$=[neg P land (R lor neg Q)] lor [R land (neg P lor Q)]$
(Distribution:)
$=(neg P land R) lor (neg P land neg Q) lor (R land neg P) lor (R land Q)$
(Commutation:)
$=(neg P land R) lor (neg P land neg Q) lor (neg P land R) lor (R land Q)$
(Idempotence:)
$=(neg P land R) lor (neg P land neg Q) lor (R land Q)$
(Distribution 2*2*2:)
$=(neg P lor neg P lor R) land (neg P lor neg Q lor R) land (neg P lor neg P lor Q) land (neg P lor neg Q lor Q) land (R lor neg P lor R) land (R lor neg Q lor R) land (R lor neg P lor Q) land (R lor neg Q lor Q)$
(Complement:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor top) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land (R lor top)$
(Annihilation:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land top land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land top$
(Identity:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) $
(two Absorptions and an Idempotence:)
$=(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
Phew! Almost there ....
Now, use:
Adjacency
$$P = (P lor Q) land (P lor neg Q)$$
Applied to where we were:
$(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
(Adjacency:)
$=(neg P lor R lor Q) land (neg P lor R lor neg Q) land (neg P lor Q) land (neg Q lor R)$
(Two Absorptions)
$(neg P lor Q) land (neg Q lor R)$
.. and finally we're there! Sheesh!
$endgroup$
$begingroup$
Comments are not for extended discussion; this conversation has been moved to chat.
$endgroup$
– Aloizio Macedo♦
Jan 30 at 17:21
add a comment |
$begingroup$
Here are some useful but elementary equivalence principles:
Complement
$$P lor neg P Leftrightarrow top$$
$$P land neg P Leftrightarrow bot$$
Annihilation
$$P lor top Leftrightarrow top$$
$$P land bot Leftrightarrow bot$$
Identity
$$P land top Leftrightarrow P$$
$$P lor bot Leftrightarrow P$$
Idempotence
$$P lor P = P$$
$$P land P = P$$
Also, as you noticed, the whole big right terms does indeed not get you anywhere ... you need to work in the left term $neg P lor R$
So, starting a few lines from before you get 'stuck' (because indeed, you're just going in loops at that point) (and also throwing in some necessary parentheses):
$(neg P lor R) land [color{red}((neg P lor Q) land (P lor neg Q)color{red}) lor color{red}((neg R lor Q) land (R lor neg Q)color{red})] =$
$(neg P land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) lor (R land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) =$
$[neg P land ((neg P lor Q) land (P lor neg Q))] lor [neg P land ((neg R lor Q) land (R lor neg Q))] lor [R land ((neg P lor Q) land (P lor neg Q))] lor [R land ((neg R lor Q) land (R lor neg Q))] =$
(dropping unncessary parentheses)
$[neg P land (neg P lor Q) land (P lor neg Q)] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land (neg R lor Q) land (R lor neg Q)]$
OK, now two handy laws are:
Absorption
$$P land (P lor Q) = P$$
Reduction
$$P land (neg P lor Q) = P land Q$$
Applying these, we get:
$[neg P land neg Q] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land Q ]$
OK, and now 'unDistribute' the $neg P $ and the $R$:
$= [neg P land (neg Q lor ((neg R lor Q) land (R lor neg Q)))] lor [R land (((neg P lor Q) land (P lor neg Q)) lor Q) ]$
and now you can distribute the $neg Q$ and the $Q$:
$= [neg P land (neg Q lor (neg R lor Q)) land (neg Q lor (R lor neg Q))] lor [R land ((neg P lor Q) lor Q) land ((P lor neg Q) lor Q) ] =$
(dropping unncessary parentheses)
$[neg P land (neg Q lor neg R lor Q) land (neg Q lor R lor neg Q)] lor [R land (neg P lor Q lor Q) land (P lor neg Q lor Q) ]$
And now you can use those simplification laws from the start of my post:
(Complement:)
$[neg P land (neg R lor top) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor top) ]$
(Annihilation:)
$=[neg P land top land (R lor neg Q)] lor [R land (neg P lor Q) land top ]$
(Identity:)
$=[neg P land (R lor neg Q)] lor [R land (neg P lor Q)]$
(Distribution:)
$=(neg P land R) lor (neg P land neg Q) lor (R land neg P) lor (R land Q)$
(Commutation:)
$=(neg P land R) lor (neg P land neg Q) lor (neg P land R) lor (R land Q)$
(Idempotence:)
$=(neg P land R) lor (neg P land neg Q) lor (R land Q)$
(Distribution 2*2*2:)
$=(neg P lor neg P lor R) land (neg P lor neg Q lor R) land (neg P lor neg P lor Q) land (neg P lor neg Q lor Q) land (R lor neg P lor R) land (R lor neg Q lor R) land (R lor neg P lor Q) land (R lor neg Q lor Q)$
(Complement:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor top) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land (R lor top)$
(Annihilation:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land top land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land top$
(Identity:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) $
(two Absorptions and an Idempotence:)
$=(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
Phew! Almost there ....
Now, use:
Adjacency
$$P = (P lor Q) land (P lor neg Q)$$
Applied to where we were:
$(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
(Adjacency:)
$=(neg P lor R lor Q) land (neg P lor R lor neg Q) land (neg P lor Q) land (neg Q lor R)$
(Two Absorptions)
$(neg P lor Q) land (neg Q lor R)$
.. and finally we're there! Sheesh!
$endgroup$
Here are some useful but elementary equivalence principles:
Complement
$$P lor neg P Leftrightarrow top$$
$$P land neg P Leftrightarrow bot$$
Annihilation
$$P lor top Leftrightarrow top$$
$$P land bot Leftrightarrow bot$$
Identity
$$P land top Leftrightarrow P$$
$$P lor bot Leftrightarrow P$$
Idempotence
$$P lor P = P$$
$$P land P = P$$
Also, as you noticed, the whole big right terms does indeed not get you anywhere ... you need to work in the left term $neg P lor R$
So, starting a few lines from before you get 'stuck' (because indeed, you're just going in loops at that point) (and also throwing in some necessary parentheses):
$(neg P lor R) land [color{red}((neg P lor Q) land (P lor neg Q)color{red}) lor color{red}((neg R lor Q) land (R lor neg Q)color{red})] =$
$(neg P land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) lor (R land [((neg P lor Q) land (P lor neg Q)) lor ((neg R lor Q) land (R lor neg Q))]) =$
$[neg P land ((neg P lor Q) land (P lor neg Q))] lor [neg P land ((neg R lor Q) land (R lor neg Q))] lor [R land ((neg P lor Q) land (P lor neg Q))] lor [R land ((neg R lor Q) land (R lor neg Q))] =$
(dropping unncessary parentheses)
$[neg P land (neg P lor Q) land (P lor neg Q)] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land (neg R lor Q) land (R lor neg Q)]$
OK, now two handy laws are:
Absorption
$$P land (P lor Q) = P$$
Reduction
$$P land (neg P lor Q) = P land Q$$
Applying these, we get:
$[neg P land neg Q] lor [neg P land (neg R lor Q) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor neg Q)] lor [R land Q ]$
OK, and now 'unDistribute' the $neg P $ and the $R$:
$= [neg P land (neg Q lor ((neg R lor Q) land (R lor neg Q)))] lor [R land (((neg P lor Q) land (P lor neg Q)) lor Q) ]$
and now you can distribute the $neg Q$ and the $Q$:
$= [neg P land (neg Q lor (neg R lor Q)) land (neg Q lor (R lor neg Q))] lor [R land ((neg P lor Q) lor Q) land ((P lor neg Q) lor Q) ] =$
(dropping unncessary parentheses)
$[neg P land (neg Q lor neg R lor Q) land (neg Q lor R lor neg Q)] lor [R land (neg P lor Q lor Q) land (P lor neg Q lor Q) ]$
And now you can use those simplification laws from the start of my post:
(Complement:)
$[neg P land (neg R lor top) land (R lor neg Q)] lor [R land (neg P lor Q) land (P lor top) ]$
(Annihilation:)
$=[neg P land top land (R lor neg Q)] lor [R land (neg P lor Q) land top ]$
(Identity:)
$=[neg P land (R lor neg Q)] lor [R land (neg P lor Q)]$
(Distribution:)
$=(neg P land R) lor (neg P land neg Q) lor (R land neg P) lor (R land Q)$
(Commutation:)
$=(neg P land R) lor (neg P land neg Q) lor (neg P land R) lor (R land Q)$
(Idempotence:)
$=(neg P land R) lor (neg P land neg Q) lor (R land Q)$
(Distribution 2*2*2:)
$=(neg P lor neg P lor R) land (neg P lor neg Q lor R) land (neg P lor neg P lor Q) land (neg P lor neg Q lor Q) land (R lor neg P lor R) land (R lor neg Q lor R) land (R lor neg P lor Q) land (R lor neg Q lor Q)$
(Complement:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor top) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land (R lor top)$
(Annihilation:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land top land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) land top$
(Identity:)
$=(neg P lor R) land (neg P lor neg Q lor R) land (neg P lor Q) land (neg P lor R) land (neg Q lor R) land (R lor neg P lor Q) $
(two Absorptions and an Idempotence:)
$=(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
Phew! Almost there ....
Now, use:
Adjacency
$$P = (P lor Q) land (P lor neg Q)$$
Applied to where we were:
$(neg P lor R) land (neg P lor Q) land (neg Q lor R)$
(Adjacency:)
$=(neg P lor R lor Q) land (neg P lor R lor neg Q) land (neg P lor Q) land (neg Q lor R)$
(Two Absorptions)
$(neg P lor Q) land (neg Q lor R)$
.. and finally we're there! Sheesh!
edited Jan 30 at 16:05
answered Jan 29 at 19:27
Bram28Bram28
64k44793
64k44793
$begingroup$
Comments are not for extended discussion; this conversation has been moved to chat.
$endgroup$
– Aloizio Macedo♦
Jan 30 at 17:21
add a comment |
$begingroup$
Comments are not for extended discussion; this conversation has been moved to chat.
$endgroup$
– Aloizio Macedo♦
Jan 30 at 17:21
$begingroup$
Comments are not for extended discussion; this conversation has been moved to chat.
$endgroup$
– Aloizio Macedo♦
Jan 30 at 17:21
$begingroup$
Comments are not for extended discussion; this conversation has been moved to chat.
$endgroup$
– Aloizio Macedo♦
Jan 30 at 17:21
add a comment |
$begingroup$
Your approach - which I continued in my first Answer - effectively puts the statements into their CNF ... which is what you were trying to avoid.
So, I figure I would give an Alternative answer, working with the whole conditionals, rather than breaking the statements down all the way to literals.
Now, this is going to require some equivalence principles involving conditionals. Notice that in my other answer I showed that
$$(neg P lor R) land (neg P lor Q) land (neg Q lor R) = (neg P lor Q) land (neg Q lor R)$$
This equivalence is actually known to be the Consensus Theorem, which also has a conditional form:
Conditional Consensus
$$(P rightarrow R) land (P rightarrow Q) land (Q rightarrow R) = (P rightarrow Q) land (Q rightarrow R)$$
OK, that's the key equivalence I'll be using, but I want one more, which is:
Conditional Tautology
$$(P rightarrow Q) lor (Q rightarrow R) = top$$
OK, with that, here goes:
$(P rightarrow R) land ((P leftrightarrow Q) lor (Q leftrightarrow R))=$
(Work out biconditional as two conditionals:)
$(P rightarrow R) land (((P rightarrow Q) land (Q rightarrow P)) lor ((Q rightarrow R) land (R rightarrow Q)))=$
(DIstribution of $P rightarrow R$:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q))=$
(Consensus Conditional form!)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P) land (Q rightarrow R)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q) land (P rightarrow Q))$
(Undistribution of three terms in common:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow R)) land ((Q rightarrow P) lor (R rightarrow Q))=$
(conditional Consensus and Conditional Tautology:)
$((P rightarrow Q) land (Q rightarrow R)) land top=$
$(P rightarrow Q) land (Q rightarrow R)$
Ah, much better!
$endgroup$
add a comment |
$begingroup$
Your approach - which I continued in my first Answer - effectively puts the statements into their CNF ... which is what you were trying to avoid.
So, I figure I would give an Alternative answer, working with the whole conditionals, rather than breaking the statements down all the way to literals.
Now, this is going to require some equivalence principles involving conditionals. Notice that in my other answer I showed that
$$(neg P lor R) land (neg P lor Q) land (neg Q lor R) = (neg P lor Q) land (neg Q lor R)$$
This equivalence is actually known to be the Consensus Theorem, which also has a conditional form:
Conditional Consensus
$$(P rightarrow R) land (P rightarrow Q) land (Q rightarrow R) = (P rightarrow Q) land (Q rightarrow R)$$
OK, that's the key equivalence I'll be using, but I want one more, which is:
Conditional Tautology
$$(P rightarrow Q) lor (Q rightarrow R) = top$$
OK, with that, here goes:
$(P rightarrow R) land ((P leftrightarrow Q) lor (Q leftrightarrow R))=$
(Work out biconditional as two conditionals:)
$(P rightarrow R) land (((P rightarrow Q) land (Q rightarrow P)) lor ((Q rightarrow R) land (R rightarrow Q)))=$
(DIstribution of $P rightarrow R$:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q))=$
(Consensus Conditional form!)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P) land (Q rightarrow R)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q) land (P rightarrow Q))$
(Undistribution of three terms in common:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow R)) land ((Q rightarrow P) lor (R rightarrow Q))=$
(conditional Consensus and Conditional Tautology:)
$((P rightarrow Q) land (Q rightarrow R)) land top=$
$(P rightarrow Q) land (Q rightarrow R)$
Ah, much better!
$endgroup$
add a comment |
$begingroup$
Your approach - which I continued in my first Answer - effectively puts the statements into their CNF ... which is what you were trying to avoid.
So, I figure I would give an Alternative answer, working with the whole conditionals, rather than breaking the statements down all the way to literals.
Now, this is going to require some equivalence principles involving conditionals. Notice that in my other answer I showed that
$$(neg P lor R) land (neg P lor Q) land (neg Q lor R) = (neg P lor Q) land (neg Q lor R)$$
This equivalence is actually known to be the Consensus Theorem, which also has a conditional form:
Conditional Consensus
$$(P rightarrow R) land (P rightarrow Q) land (Q rightarrow R) = (P rightarrow Q) land (Q rightarrow R)$$
OK, that's the key equivalence I'll be using, but I want one more, which is:
Conditional Tautology
$$(P rightarrow Q) lor (Q rightarrow R) = top$$
OK, with that, here goes:
$(P rightarrow R) land ((P leftrightarrow Q) lor (Q leftrightarrow R))=$
(Work out biconditional as two conditionals:)
$(P rightarrow R) land (((P rightarrow Q) land (Q rightarrow P)) lor ((Q rightarrow R) land (R rightarrow Q)))=$
(DIstribution of $P rightarrow R$:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q))=$
(Consensus Conditional form!)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P) land (Q rightarrow R)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q) land (P rightarrow Q))$
(Undistribution of three terms in common:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow R)) land ((Q rightarrow P) lor (R rightarrow Q))=$
(conditional Consensus and Conditional Tautology:)
$((P rightarrow Q) land (Q rightarrow R)) land top=$
$(P rightarrow Q) land (Q rightarrow R)$
Ah, much better!
$endgroup$
Your approach - which I continued in my first Answer - effectively puts the statements into their CNF ... which is what you were trying to avoid.
So, I figure I would give an Alternative answer, working with the whole conditionals, rather than breaking the statements down all the way to literals.
Now, this is going to require some equivalence principles involving conditionals. Notice that in my other answer I showed that
$$(neg P lor R) land (neg P lor Q) land (neg Q lor R) = (neg P lor Q) land (neg Q lor R)$$
This equivalence is actually known to be the Consensus Theorem, which also has a conditional form:
Conditional Consensus
$$(P rightarrow R) land (P rightarrow Q) land (Q rightarrow R) = (P rightarrow Q) land (Q rightarrow R)$$
OK, that's the key equivalence I'll be using, but I want one more, which is:
Conditional Tautology
$$(P rightarrow Q) lor (Q rightarrow R) = top$$
OK, with that, here goes:
$(P rightarrow R) land ((P leftrightarrow Q) lor (Q leftrightarrow R))=$
(Work out biconditional as two conditionals:)
$(P rightarrow R) land (((P rightarrow Q) land (Q rightarrow P)) lor ((Q rightarrow R) land (R rightarrow Q)))=$
(DIstribution of $P rightarrow R$:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q))=$
(Consensus Conditional form!)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow P) land (Q rightarrow R)) lor ((P rightarrow R) land (Q rightarrow R) land (R rightarrow Q) land (P rightarrow Q))$
(Undistribution of three terms in common:)
$((P rightarrow R) land (P rightarrow Q) land (Q rightarrow R)) land ((Q rightarrow P) lor (R rightarrow Q))=$
(conditional Consensus and Conditional Tautology:)
$((P rightarrow Q) land (Q rightarrow R)) land top=$
$(P rightarrow Q) land (Q rightarrow R)$
Ah, much better!
answered Jan 29 at 22:41
Bram28Bram28
64k44793
64k44793
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%2f3092595%2fassistance-in-completing-the-proof-p-%25e2%2586%2592-q%25e2%2588%25a7q-%25e2%2586%2592-r-is-equivalent-to-p-%25e2%2586%2592-r%25e2%2588%25a7%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