Mixing
S5 proof of $square(square Prightarrowsquare Q)veesquare(square Qrightarrowsquare P)$
$begingroup$
I'm trying to construct an S5 proof of $vdashsquare(square Prightarrowsquare Q)veesquare(square Qrightarrowsquare P)$.
I know that $phiveepsi$ is equivalent to $text{~}phirightarrowpsi$, and so what I'm really trying to derive is $text{~}square(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$ (which is equivalent to $lozengetext{~}(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$), but I'm not sure what steps I'd have to take to reach this.
Your help would be appreciated.
(in S5 I have the axioms
$square(phirightarrowpsi)rightarrow (squarephirightarrowsquarepsi)$
$squarephi rightarrow phi$
$lozengesquarephirightarrowsquarephi$
as well as the rules modus ponens ($phi$, $phirightarrowpsi$ $vdash psi$) and necessitation ($phi$ becomes $squarephi$)).
EDIT: here are the approaches that I've considered so far:
As above, I know that what I need to prove is of the form:
$lozengetext{~}(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$
I've tried working back from this to get to something more familiar that I would know how to prove, but without much success.
Taking the contrapositive certainly doesn't work because you just end up with the same thing but with Q and P swapped.
I could start by taking $(Prightarrow Q) rightarrow(text{~}Qrightarrow text{~}P)$ (true by propositional logic (it's just the contrapositive)), then applying necessitation and the first axiom gives $(square Prightarrowsquare Q) rightarrow(square text{~}Qrightarrowsquare text{~}P)$, but I can't see any obvious way to proceed from here.
I could also start by saying that $(square Prightarrowsquare Q) rightarrow(text{~}square Qrightarrowtext{~}square P)$, but again I see no obvious way to proceed because the negations make things more difficult.
I'm really at a loss as to how to actually approach this, so even just helping tell me how I get started would help a lot.
logic propositional-calculus modal-logic
asked Jan 29 at 23:01
j j jamesonj j jameson
94
$endgroup$
add a comment |
$begingroup$
I'm trying to construct an S5 proof of $vdashsquare(square Prightarrowsquare Q)veesquare(square Qrightarrowsquare P)$.
I know that $phiveepsi$ is equivalent to $text{~}phirightarrowpsi$, and so what I'm really trying to derive is $text{~}square(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$ (which is equivalent to $lozengetext{~}(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$), but I'm not sure what steps I'd have to take to reach this.
Your help would be appreciated.
(in S5 I have the axioms
$square(phirightarrowpsi)rightarrow (squarephirightarrowsquarepsi)$
$squarephi rightarrow phi$
$lozengesquarephirightarrowsquarephi$
as well as the rules modus ponens ($phi$, $phirightarrowpsi$ $vdash psi$) and necessitation ($phi$ becomes $squarephi$)).
EDIT: here are the approaches that I've considered so far:
As above, I know that what I need to prove is of the form:
$lozengetext{~}(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$
I've tried working back from this to get to something more familiar that I would know how to prove, but without much success.
Taking the contrapositive certainly doesn't work because you just end up with the same thing but with Q and P swapped.
I could start by taking $(Prightarrow Q) rightarrow(text{~}Qrightarrow text{~}P)$ (true by propositional logic (it's just the contrapositive)), then applying necessitation and the first axiom gives $(square Prightarrowsquare Q) rightarrow(square text{~}Qrightarrowsquare text{~}P)$, but I can't see any obvious way to proceed from here.
I could also start by saying that $(square Prightarrowsquare Q) rightarrow(text{~}square Qrightarrowtext{~}square P)$, but again I see no obvious way to proceed because the negations make things more difficult.
I'm really at a loss as to how to actually approach this, so even just helping tell me how I get started would help a lot.
logic propositional-calculus modal-logic
asked Jan 29 at 23:01
j j jamesonj j jameson
94
$endgroup$
$begingroup$
What have you tried?
$endgroup$
– Jishin Noben
Jan 30 at 10:15
$begingroup$
@JishinNoben I've edited to include what I've considered, but it's not much because I haven't been able to get very far at all.
$endgroup$
– j j jameson
Jan 30 at 11:00
$begingroup$
Have you tried checking it in the semantics? That is, is it semantically valid?
$endgroup$
– ShyPerson
Feb 1 at 23:03
$begingroup$
Answered here
$endgroup$
– Jishin Noben
Feb 2 at 0:03
add a comment |
$begingroup$
I'm trying to construct an S5 proof of $vdashsquare(square Prightarrowsquare Q)veesquare(square Qrightarrowsquare P)$.
I know that $phiveepsi$ is equivalent to $text{~}phirightarrowpsi$, and so what I'm really trying to derive is $text{~}square(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$ (which is equivalent to $lozengetext{~}(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$), but I'm not sure what steps I'd have to take to reach this.
Your help would be appreciated.
(in S5 I have the axioms
$square(phirightarrowpsi)rightarrow (squarephirightarrowsquarepsi)$
$squarephi rightarrow phi$
$lozengesquarephirightarrowsquarephi$
as well as the rules modus ponens ($phi$, $phirightarrowpsi$ $vdash psi$) and necessitation ($phi$ becomes $squarephi$)).
EDIT: here are the approaches that I've considered so far:
As above, I know that what I need to prove is of the form:
$lozengetext{~}(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$
I've tried working back from this to get to something more familiar that I would know how to prove, but without much success.
Taking the contrapositive certainly doesn't work because you just end up with the same thing but with Q and P swapped.
I could start by taking $(Prightarrow Q) rightarrow(text{~}Qrightarrow text{~}P)$ (true by propositional logic (it's just the contrapositive)), then applying necessitation and the first axiom gives $(square Prightarrowsquare Q) rightarrow(square text{~}Qrightarrowsquare text{~}P)$, but I can't see any obvious way to proceed from here.
I could also start by saying that $(square Prightarrowsquare Q) rightarrow(text{~}square Qrightarrowtext{~}square P)$, but again I see no obvious way to proceed because the negations make things more difficult.
I'm really at a loss as to how to actually approach this, so even just helping tell me how I get started would help a lot.
logic propositional-calculus modal-logic
asked Jan 29 at 23:01
j j jamesonj j jameson
94
$endgroup$
I'm trying to construct an S5 proof of $vdashsquare(square Prightarrowsquare Q)veesquare(square Qrightarrowsquare P)$.
I know that $phiveepsi$ is equivalent to $text{~}phirightarrowpsi$, and so what I'm really trying to derive is $text{~}square(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$ (which is equivalent to $lozengetext{~}(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$), but I'm not sure what steps I'd have to take to reach this.
Your help would be appreciated.
(in S5 I have the axioms
$square(phirightarrowpsi)rightarrow (squarephirightarrowsquarepsi)$
$squarephi rightarrow phi$
$lozengesquarephirightarrowsquarephi$
as well as the rules modus ponens ($phi$, $phirightarrowpsi$ $vdash psi$) and necessitation ($phi$ becomes $squarephi$)).
EDIT: here are the approaches that I've considered so far:
As above, I know that what I need to prove is of the form:
$lozengetext{~}(square Prightarrowsquare Q) rightarrowsquare(square Qrightarrowsquare P)$
I've tried working back from this to get to something more familiar that I would know how to prove, but without much success.
Taking the contrapositive certainly doesn't work because you just end up with the same thing but with Q and P swapped.
I could start by taking $(Prightarrow Q) rightarrow(text{~}Qrightarrow text{~}P)$ (true by propositional logic (it's just the contrapositive)), then applying necessitation and the first axiom gives $(square Prightarrowsquare Q) rightarrow(square text{~}Qrightarrowsquare text{~}P)$, but I can't see any obvious way to proceed from here.
I could also start by saying that $(square Prightarrowsquare Q) rightarrow(text{~}square Qrightarrowtext{~}square P)$, but again I see no obvious way to proceed because the negations make things more difficult.
I'm really at a loss as to how to actually approach this, so even just helping tell me how I get started would help a lot.
logic propositional-calculus modal-logic
logic propositional-calculus modal-logic
asked Jan 29 at 23:01
j j jamesonj j jameson
94
asked Jan 29 at 23:01
j j jamesonj j jameson
94
edited Jan 30 at 10:59
j j jameson
asked Jan 29 at 23:01
j j jamesonj j jameson
94
asked Jan 29 at 23:01
j j jamesonj j jameson
94
asked Jan 29 at 23:01
j j jamesonj j jameson
94
94
$begingroup$
What have you tried?
$endgroup$
– Jishin Noben
Jan 30 at 10:15
$begingroup$
@JishinNoben I've edited to include what I've considered, but it's not much because I haven't been able to get very far at all.
$endgroup$
– j j jameson
Jan 30 at 11:00
$begingroup$
Have you tried checking it in the semantics? That is, is it semantically valid?
$endgroup$
– ShyPerson
Feb 1 at 23:03
$begingroup$
Answered here
$endgroup$
– Jishin Noben
Feb 2 at 0:03
add a comment |
$begingroup$
What have you tried?
$endgroup$
– Jishin Noben
Jan 30 at 10:15
$begingroup$
@JishinNoben I've edited to include what I've considered, but it's not much because I haven't been able to get very far at all.
$endgroup$
– j j jameson
Jan 30 at 11:00
$begingroup$
Have you tried checking it in the semantics? That is, is it semantically valid?
$endgroup$
– ShyPerson
Feb 1 at 23:03
$begingroup$
Answered here
$endgroup$
– Jishin Noben
Feb 2 at 0:03
$begingroup$
What have you tried?
$endgroup$
– Jishin Noben
Jan 30 at 10:15
$begingroup$
What have you tried?
$endgroup$
– Jishin Noben
Jan 30 at 10:15
$begingroup$
@JishinNoben I've edited to include what I've considered, but it's not much because I haven't been able to get very far at all.
$endgroup$
– j j jameson
Jan 30 at 11:00
$begingroup$
@JishinNoben I've edited to include what I've considered, but it's not much because I haven't been able to get very far at all.
$endgroup$
– j j jameson
Jan 30 at 11:00
$begingroup$
Have you tried checking it in the semantics? That is, is it semantically valid?
$endgroup$
– ShyPerson
Feb 1 at 23:03
$begingroup$
Have you tried checking it in the semantics? That is, is it semantically valid?
$endgroup$
– ShyPerson
Feb 1 at 23:03
$begingroup$
Answered here
$endgroup$
– Jishin Noben
Feb 2 at 0:03
$begingroup$
Answered here
$endgroup$
– Jishin Noben
Feb 2 at 0:03
add a comment |
0
active
oldest
votes
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%2f3092843%2fs5-proof-of-square-square-p-rightarrow-square-q-vee-square-square-q-rightar%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
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%2f3092843%2fs5-proof-of-square-square-p-rightarrow-square-q-vee-square-square-q-rightar%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 have you tried?
$endgroup$
– Jishin Noben
Jan 30 at 10:15
$begingroup$
@JishinNoben I've edited to include what I've considered, but it's not much because I haven't been able to get very far at all.
$endgroup$
– j j jameson
Jan 30 at 11:00
$begingroup$
Have you tried checking it in the semantics? That is, is it semantically valid?
$endgroup$
– ShyPerson
Feb 1 at 23:03
$begingroup$
Answered here
$endgroup$
– Jishin Noben
Feb 2 at 0:03