Dtjytyk

Most cost effective thermostat setting: consistent temperature vs. lowest temperature possible

A Cautionary Suggestion

Combining an idiom with a metonymy

Why Choose Less Effective Armour Types?

Do I need life insurance if I can cover my own funeral costs?

Define, (actually define) the "stability" and "energy" of a compound

In a future war, an old lady is trying to raise a boy but one of the weapons has made everyone deaf

Existence of subset with given Hausdorff dimension

Could the Saturn V actually have launched astronauts around Venus?

How to deal with taxi scam when on vacation?

What is a^b and (a&b)<<1?

Sailing the cryptic seas

What options are left, if Britain cannot decide?

Professor being mistaken for a grad student

Why doesn't using two cd commands in bash script execute the second command?

How Could an Airship Be Repaired Mid-Flight

It's a yearly task, alright

Does Mathematica reuse previous computations?

The difference between「N分で」and「後N分で」

how to draw discrete time diagram in tikz

Why do passenger jet manufacturers design their planes with stall prevention systems?

Can a druid choose the size of its wild shape beast?

A sequence that has integer values for prime indexes only:

How do anti-virus programs start at Windows boot?

$vdashphi land diamondpsi to diamond(psilanddiamondphi)$ in KB

Showing $vdash phito square diamond phi$A Natural-Deduction proof of $ { neg N,neg N to L,D leftrightarrow neg N } vdash (L lor A) land D $.Natural deduction proof of $p rightarrow q vdash lnot(p land lnot q)$Proving $ lnot (A Rightarrow B) vDash A land lnot B $A real-world interpretation for ${neg(phileftrightarrowpsi)}vdash((negphi)leftrightarrowpsi)$How to prove $lnot(pto q)vdash p landlnot q$If $Sigma Cup ${$phi$}$ vdash theta$ and $Sigma Cup ${$lnotphi$}$ vdash theta$ then $Sigma vdash theta.$Assuming $Sigma vdash eta$, what is the deduction for $Sigma vdash negeta rightarrow eta$?Axiomatic proof of $vdash p rightarrow ((prightarrow q) rightarrow q)$Formal Deduction (logic) Question: $lnot C, (B to lnot C) to A vdash (A to C) to F$Prove $vdash neg(square Fland p)$ in $KD$

1

$begingroup$

I've been trying to prove $vdashphi land diamondpsi to diamond(psilanddiamond phi)$ in natural deduction where it's allowed to use $phito square diamond phi$ and/or $diamondsquarephitophi$ (that is, in $KB)$, but I failed. How can one prove this? I'm not including my work because it consists of dozens of pages and doesn't lead anywhere...

logic propositional-calculus natural-deduction formal-proofs modal-logic

share|cite|improve this question

asked Mar 10 at 22:28

user643175user643175

846

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  You've listed the axiom B, but when you say "in natural deduction", I guess you're also including the rules of the modal logic K?
  $endgroup$
  – Alex Kruckman
  Mar 10 at 22:55
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @AlexKruckman Wikipedia says "K := no conditions", so I'm not sure what rules of K you mean.
  $endgroup$
  – user643175
  Mar 10 at 23:03
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  The necessitation rule and the distribution axiom.
  $endgroup$
  – Alex Kruckman
  Mar 10 at 23:04
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @AlexKruckman Yes, they are included. By "natural deduction" I meant the natural deduction system which includes box-subproofs and diamond-subproofs; and then those axioms can be proven.
  $endgroup$
  – user643175
  Mar 10 at 23:06
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Ok. If you want to ask for a proof in a particular system, it's good practice to include a link to the precise rules of that system. Every logic has a wide variety of proof systems!
  $endgroup$
  – Alex Kruckman
  Mar 10 at 23:09
  

  
  
  
  

add a comment | 

1

$begingroup$

I've been trying to prove $vdashphi land diamondpsi to diamond(psilanddiamond phi)$ in natural deduction where it's allowed to use $phito square diamond phi$ and/or $diamondsquarephitophi$ (that is, in $KB)$, but I failed. How can one prove this? I'm not including my work because it consists of dozens of pages and doesn't lead anywhere...

logic propositional-calculus natural-deduction formal-proofs modal-logic

share|cite|improve this question

asked Mar 10 at 22:28

user643175user643175

846

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  You've listed the axiom B, but when you say "in natural deduction", I guess you're also including the rules of the modal logic K?
  $endgroup$
  – Alex Kruckman
  Mar 10 at 22:55
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @AlexKruckman Wikipedia says "K := no conditions", so I'm not sure what rules of K you mean.
  $endgroup$
  – user643175
  Mar 10 at 23:03
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  The necessitation rule and the distribution axiom.
  $endgroup$
  – Alex Kruckman
  Mar 10 at 23:04
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @AlexKruckman Yes, they are included. By "natural deduction" I meant the natural deduction system which includes box-subproofs and diamond-subproofs; and then those axioms can be proven.
  $endgroup$
  – user643175
  Mar 10 at 23:06
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Ok. If you want to ask for a proof in a particular system, it's good practice to include a link to the precise rules of that system. Every logic has a wide variety of proof systems!
  $endgroup$
  – Alex Kruckman
  Mar 10 at 23:09
  

  
  
  
  

add a comment | 

$begingroup$

I've been trying to prove $vdashphi land diamondpsi to diamond(psilanddiamond phi)$ in natural deduction where it's allowed to use $phito square diamond phi$ and/or $diamondsquarephitophi$ (that is, in $KB)$, but I failed. How can one prove this? I'm not including my work because it consists of dozens of pages and doesn't lead anywhere...

logic propositional-calculus natural-deduction formal-proofs modal-logic

share|cite|improve this question

asked Mar 10 at 22:28

user643175user643175

846

$endgroup$

share|cite|improve this question

asked Mar 10 at 22:28

user643175user643175

846

share|cite|improve this question

asked Mar 10 at 22:28

user643175user643175

846

asked Mar 10 at 22:28

user643175user643175

846

asked Mar 10 at 22:28

user643175user643175

846

1 Answer
1

active

oldest

votes

3

$begingroup$

Here's a sketch of the idea, which I'll leave to you to translate into a formal proof in your system, if you care to.

Let's assume $phi$ and $lozenge psi$. From B and modus ponens, we get $squarelozenge phi$, so we get $(squarelozengephi land lozenge psi)$

Now as an instance of the distribution axiom K, we have: $$square (lozenge phi rightarrow lnot psi) rightarrow (square lozenge phi rightarrow square lnot psi)$$

The contrapositive of this implication is: $$lnot (squarelozenge phi rightarrow square lnot psi) rightarrow lozenge lnot (lozenge phi rightarrow lnot psi)$$

Turning $lnot (prightarrow q)$ into $pland lnot q$ in two places, we get: $$(squarelozenge phi land lozenge psi) rightarrow lozenge (psi land lozenge phi)$$

Finally, by modus ponens, we get $$lozenge (psi land lozenge phi)$$

share|cite|improve this answer

answered Mar 10 at 23:14

Alex KruckmanAlex Kruckman

28k32658

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Thanks! It seems I'd have never come up with the idea of considering $square (lozenge phi rightarrow lnot psi) rightarrow (square lozenge phi rightarrow square lnot psi)$.
  $endgroup$
  – user643175
  Mar 10 at 23:41
  

  
  
  
  

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
});


}
});

draft saved

draft discarded

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

Name

Email

Required, but never shown

StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3143000%2fvdash-phi-land-diamond-psi-to-diamond-psi-land-diamond-phi-in-kb%23new-answer', 'question_page');
}
);

Post as a guest

Name

Email

Required, but never shown

3

$begingroup$

Here's a sketch of the idea, which I'll leave to you to translate into a formal proof in your system, if you care to.

Let's assume $phi$ and $lozenge psi$. From B and modus ponens, we get $squarelozenge phi$, so we get $(squarelozengephi land lozenge psi)$

Now as an instance of the distribution axiom K, we have: $$square (lozenge phi rightarrow lnot psi) rightarrow (square lozenge phi rightarrow square lnot psi)$$

The contrapositive of this implication is: $$lnot (squarelozenge phi rightarrow square lnot psi) rightarrow lozenge lnot (lozenge phi rightarrow lnot psi)$$

Turning $lnot (prightarrow q)$ into $pland lnot q$ in two places, we get: $$(squarelozenge phi land lozenge psi) rightarrow lozenge (psi land lozenge phi)$$

Finally, by modus ponens, we get $$lozenge (psi land lozenge phi)$$

share|cite|improve this answer

answered Mar 10 at 23:14

Alex KruckmanAlex Kruckman

28k32658

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Thanks! It seems I'd have never come up with the idea of considering $square (lozenge phi rightarrow lnot psi) rightarrow (square lozenge phi rightarrow square lnot psi)$.
  $endgroup$
  – user643175
  Mar 10 at 23:41
  

  
  
  
  

add a comment | 

3

$begingroup$

Here's a sketch of the idea, which I'll leave to you to translate into a formal proof in your system, if you care to.

Let's assume $phi$ and $lozenge psi$. From B and modus ponens, we get $squarelozenge phi$, so we get $(squarelozengephi land lozenge psi)$

Now as an instance of the distribution axiom K, we have: $$square (lozenge phi rightarrow lnot psi) rightarrow (square lozenge phi rightarrow square lnot psi)$$

The contrapositive of this implication is: $$lnot (squarelozenge phi rightarrow square lnot psi) rightarrow lozenge lnot (lozenge phi rightarrow lnot psi)$$

Turning $lnot (prightarrow q)$ into $pland lnot q$ in two places, we get: $$(squarelozenge phi land lozenge psi) rightarrow lozenge (psi land lozenge phi)$$

Finally, by modus ponens, we get $$lozenge (psi land lozenge phi)$$

share|cite|improve this answer

answered Mar 10 at 23:14

Alex KruckmanAlex Kruckman

28k32658

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Thanks! It seems I'd have never come up with the idea of considering $square (lozenge phi rightarrow lnot psi) rightarrow (square lozenge phi rightarrow square lnot psi)$.
  $endgroup$
  – user643175
  Mar 10 at 23:41
  

  
  
  
  

add a comment | 

$begingroup$

Here's a sketch of the idea, which I'll leave to you to translate into a formal proof in your system, if you care to.

Let's assume $phi$ and $lozenge psi$. From B and modus ponens, we get $squarelozenge phi$, so we get $(squarelozengephi land lozenge psi)$

Now as an instance of the distribution axiom K, we have: $$square (lozenge phi rightarrow lnot psi) rightarrow (square lozenge phi rightarrow square lnot psi)$$

The contrapositive of this implication is: $$lnot (squarelozenge phi rightarrow square lnot psi) rightarrow lozenge lnot (lozenge phi rightarrow lnot psi)$$

Turning $lnot (prightarrow q)$ into $pland lnot q$ in two places, we get: $$(squarelozenge phi land lozenge psi) rightarrow lozenge (psi land lozenge phi)$$

Finally, by modus ponens, we get $$lozenge (psi land lozenge phi)$$

share|cite|improve this answer

answered Mar 10 at 23:14

Alex KruckmanAlex Kruckman

28k32658

$endgroup$

share|cite|improve this answer

answered Mar 10 at 23:14

Alex KruckmanAlex Kruckman

28k32658

answered Mar 10 at 23:14

Alex KruckmanAlex Kruckman

28k32658

answered Mar 10 at 23:14

Alex KruckmanAlex Kruckman

28k32658