I've been trying to prove $\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$ in natural deduction where it's allowed to use $\phi\to \square \diamond \phi$ and/or $\diamond\square\phi\to\phi$ (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...

  • $\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

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 $\square\lozenge \phi$, so we get $(\square\lozenge\phi \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 (\square\lozenge \phi \rightarrow \square \lnot \psi) \rightarrow \lozenge \lnot (\lozenge \phi \rightarrow \lnot \psi)$$

Turning $\lnot (p\rightarrow q)$ into $p\land \lnot q$ in two places, we get: $$(\square\lozenge \phi \land \lozenge \psi) \rightarrow \lozenge (\psi \land \lozenge \phi)$$

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

  • $\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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.