Mixing
Axiomatic proof of $vdash_{S4} square Prightarrowsquarelozengesquare P$ in S4
$begingroup$
As the title explains, I'm trying to give an axiomatic proof of $vdash_{S4} square Prightarrowsquarelozengesquare P$.
This is quite simple to prove in B, but I'm struggling to see how it's done in S4. I'd really appreciate any help you could offer.
In S4, I have the following axioms:
A1: $phirightarrow (psi rightarrow phi)$
A2: $(phi rightarrow (psi rightarrow chi))rightarrow((phirightarrowpsi)rightarrow(phi rightarrowchi)) $
A3: $(text{~}psi rightarrow text{~}phi)rightarrow((text{~}psi rightarrow phi)rightarrowpsi)$
K: $square(phirightarrowpsi)rightarrow (squarephirightarrowsquarepsi)$
T: $squarephi rightarrow phi$
S4: $squarephirightarrowsquaresquarephi$
and the rules necessitation (i.e. we can make $phi$ into $squarephi$ for any sentence $phi$ and modus ponens.
logic propositional-calculus modal-logic
asked Jan 29 at 19:09
user639595user639595
62
$endgroup$
add a comment |
$begingroup$
As the title explains, I'm trying to give an axiomatic proof of $vdash_{S4} square Prightarrowsquarelozengesquare P$.
This is quite simple to prove in B, but I'm struggling to see how it's done in S4. I'd really appreciate any help you could offer.
In S4, I have the following axioms:
A1: $phirightarrow (psi rightarrow phi)$
A2: $(phi rightarrow (psi rightarrow chi))rightarrow((phirightarrowpsi)rightarrow(phi rightarrowchi)) $
A3: $(text{~}psi rightarrow text{~}phi)rightarrow((text{~}psi rightarrow phi)rightarrowpsi)$
K: $square(phirightarrowpsi)rightarrow (squarephirightarrowsquarepsi)$
T: $squarephi rightarrow phi$
S4: $squarephirightarrowsquaresquarephi$
and the rules necessitation (i.e. we can make $phi$ into $squarephi$ for any sentence $phi$ and modus ponens.
logic propositional-calculus modal-logic
asked Jan 29 at 19:09
user639595user639595
62
$endgroup$
$begingroup$
Perhaps remind the reader what the axioms of S4 are?
$endgroup$
– Henning Makholm
Jan 29 at 20:14
$begingroup$
@HenningMakholm I've updated the question to include them!
$endgroup$
– user639595
Jan 29 at 20:23
$begingroup$
Just for my information: what does ◊ mean/satisfy?
$endgroup$
– rrogers
Feb 5 at 19:21
$begingroup$
@rrogers In classical modal logic, $lozenge$ can be taken as an abbreviation for $lnotsquarelnot.$ (In much the same sense that $exists x$ can be taken as an abbreviation for $lnotforall xlnot$ in classical first order logic.) The meaning of these things can’t be summarized in a comment; if you’re interested, consult a reference on modal logic.
$endgroup$
– spaceisdarkgreen
Feb 18 at 16:54
add a comment |
$begingroup$
As the title explains, I'm trying to give an axiomatic proof of $vdash_{S4} square Prightarrowsquarelozengesquare P$.
This is quite simple to prove in B, but I'm struggling to see how it's done in S4. I'd really appreciate any help you could offer.
In S4, I have the following axioms:
A1: $phirightarrow (psi rightarrow phi)$
A2: $(phi rightarrow (psi rightarrow chi))rightarrow((phirightarrowpsi)rightarrow(phi rightarrowchi)) $
A3: $(text{~}psi rightarrow text{~}phi)rightarrow((text{~}psi rightarrow phi)rightarrowpsi)$
K: $square(phirightarrowpsi)rightarrow (squarephirightarrowsquarepsi)$
T: $squarephi rightarrow phi$
S4: $squarephirightarrowsquaresquarephi$
and the rules necessitation (i.e. we can make $phi$ into $squarephi$ for any sentence $phi$ and modus ponens.
logic propositional-calculus modal-logic
asked Jan 29 at 19:09
user639595user639595
62
$endgroup$
As the title explains, I'm trying to give an axiomatic proof of $vdash_{S4} square Prightarrowsquarelozengesquare P$.
This is quite simple to prove in B, but I'm struggling to see how it's done in S4. I'd really appreciate any help you could offer.
In S4, I have the following axioms:
A1: $phirightarrow (psi rightarrow phi)$
A2: $(phi rightarrow (psi rightarrow chi))rightarrow((phirightarrowpsi)rightarrow(phi rightarrowchi)) $
A3: $(text{~}psi rightarrow text{~}phi)rightarrow((text{~}psi rightarrow phi)rightarrowpsi)$
K: $square(phirightarrowpsi)rightarrow (squarephirightarrowsquarepsi)$
T: $squarephi rightarrow phi$
S4: $squarephirightarrowsquaresquarephi$
and the rules necessitation (i.e. we can make $phi$ into $squarephi$ for any sentence $phi$ and modus ponens.
logic propositional-calculus modal-logic
logic propositional-calculus modal-logic
asked Jan 29 at 19:09
user639595user639595
62
asked Jan 29 at 19:09
user639595user639595
62
edited Jan 29 at 20:23
user639595
asked Jan 29 at 19:09
user639595user639595
62
asked Jan 29 at 19:09
user639595user639595
62
asked Jan 29 at 19:09
user639595user639595
62
62
$begingroup$
Perhaps remind the reader what the axioms of S4 are?
$endgroup$
– Henning Makholm
Jan 29 at 20:14
$begingroup$
@HenningMakholm I've updated the question to include them!
$endgroup$
– user639595
Jan 29 at 20:23
$begingroup$
Just for my information: what does ◊ mean/satisfy?
$endgroup$
– rrogers
Feb 5 at 19:21
$begingroup$
@rrogers In classical modal logic, $lozenge$ can be taken as an abbreviation for $lnotsquarelnot.$ (In much the same sense that $exists x$ can be taken as an abbreviation for $lnotforall xlnot$ in classical first order logic.) The meaning of these things can’t be summarized in a comment; if you’re interested, consult a reference on modal logic.
$endgroup$
– spaceisdarkgreen
Feb 18 at 16:54
add a comment |
$begingroup$
Perhaps remind the reader what the axioms of S4 are?
$endgroup$
– Henning Makholm
Jan 29 at 20:14
$begingroup$
@HenningMakholm I've updated the question to include them!
$endgroup$
– user639595
Jan 29 at 20:23
$begingroup$
Just for my information: what does ◊ mean/satisfy?
$endgroup$
– rrogers
Feb 5 at 19:21
$begingroup$
@rrogers In classical modal logic, $lozenge$ can be taken as an abbreviation for $lnotsquarelnot.$ (In much the same sense that $exists x$ can be taken as an abbreviation for $lnotforall xlnot$ in classical first order logic.) The meaning of these things can’t be summarized in a comment; if you’re interested, consult a reference on modal logic.
$endgroup$
– spaceisdarkgreen
Feb 18 at 16:54
$begingroup$
Perhaps remind the reader what the axioms of S4 are?
$endgroup$
– Henning Makholm
Jan 29 at 20:14
$begingroup$
Perhaps remind the reader what the axioms of S4 are?
$endgroup$
– Henning Makholm
Jan 29 at 20:14
$begingroup$
@HenningMakholm I've updated the question to include them!
$endgroup$
– user639595
Jan 29 at 20:23
$begingroup$
@HenningMakholm I've updated the question to include them!
$endgroup$
– user639595
Jan 29 at 20:23
$begingroup$
Just for my information: what does ◊ mean/satisfy?
$endgroup$
– rrogers
Feb 5 at 19:21
$begingroup$
Just for my information: what does ◊ mean/satisfy?
$endgroup$
– rrogers
Feb 5 at 19:21
$begingroup$
@rrogers In classical modal logic, $lozenge$ can be taken as an abbreviation for $lnotsquarelnot.$ (In much the same sense that $exists x$ can be taken as an abbreviation for $lnotforall xlnot$ in classical first order logic.) The meaning of these things can’t be summarized in a comment; if you’re interested, consult a reference on modal logic.
$endgroup$
– spaceisdarkgreen
Feb 18 at 16:54
$begingroup$
@rrogers In classical modal logic, $lozenge$ can be taken as an abbreviation for $lnotsquarelnot.$ (In much the same sense that $exists x$ can be taken as an abbreviation for $lnotforall xlnot$ in classical first order logic.) The meaning of these things can’t be summarized in a comment; if you’re interested, consult a reference on modal logic.
$endgroup$
– spaceisdarkgreen
Feb 18 at 16:54
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
From contrapositive of axiom T, $Atolozenge A,$ applying necessitation and taking $A=square P$ gives $square(square Pto lozengesquare P),$ which via K gives $squaresquare Pto squarelozengesquare P.$ Then axiom $square Pto square square P$ finishes it off.
answered Jan 29 at 21:10
spaceisdarkgreenspaceisdarkgreen
33.8k21753
$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%2f3092599%2faxiomatic-proof-of-vdash-s4-square-p-rightarrow-square-lozenge-square-p-in%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
From contrapositive of axiom T, $Atolozenge A,$ applying necessitation and taking $A=square P$ gives $square(square Pto lozengesquare P),$ which via K gives $squaresquare Pto squarelozengesquare P.$ Then axiom $square Pto square square P$ finishes it off.
answered Jan 29 at 21:10
spaceisdarkgreenspaceisdarkgreen
33.8k21753
$endgroup$
add a comment |
$begingroup$
From contrapositive of axiom T, $Atolozenge A,$ applying necessitation and taking $A=square P$ gives $square(square Pto lozengesquare P),$ which via K gives $squaresquare Pto squarelozengesquare P.$ Then axiom $square Pto square square P$ finishes it off.
answered Jan 29 at 21:10
spaceisdarkgreenspaceisdarkgreen
33.8k21753
$endgroup$
add a comment |
$begingroup$
From contrapositive of axiom T, $Atolozenge A,$ applying necessitation and taking $A=square P$ gives $square(square Pto lozengesquare P),$ which via K gives $squaresquare Pto squarelozengesquare P.$ Then axiom $square Pto square square P$ finishes it off.
answered Jan 29 at 21:10
spaceisdarkgreenspaceisdarkgreen
33.8k21753
$endgroup$
From contrapositive of axiom T, $Atolozenge A,$ applying necessitation and taking $A=square P$ gives $square(square Pto lozengesquare P),$ which via K gives $squaresquare Pto squarelozengesquare P.$ Then axiom $square Pto square square P$ finishes it off.
answered Jan 29 at 21:10
spaceisdarkgreenspaceisdarkgreen
33.8k21753
answered Jan 29 at 21:10
spaceisdarkgreenspaceisdarkgreen
33.8k21753
answered Jan 29 at 21:10
spaceisdarkgreenspaceisdarkgreen
33.8k21753
answered Jan 29 at 21:10
spaceisdarkgreenspaceisdarkgreen
33.8k21753
33.8k21753
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%2f3092599%2faxiomatic-proof-of-vdash-s4-square-p-rightarrow-square-lozenge-square-p-in%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$
Perhaps remind the reader what the axioms of S4 are?
$endgroup$
– Henning Makholm
Jan 29 at 20:14
$begingroup$
@HenningMakholm I've updated the question to include them!
$endgroup$
– user639595
Jan 29 at 20:23
$begingroup$
Just for my information: what does ◊ mean/satisfy?
$endgroup$
– rrogers
Feb 5 at 19:21
$begingroup$
@rrogers In classical modal logic, $lozenge$ can be taken as an abbreviation for $lnotsquarelnot.$ (In much the same sense that $exists x$ can be taken as an abbreviation for $lnotforall xlnot$ in classical first order logic.) The meaning of these things can’t be summarized in a comment; if you’re interested, consult a reference on modal logic.
$endgroup$
– spaceisdarkgreen
Feb 18 at 16:54