I'm confused about the expectation of what a proof in modal logic is supposed to look like, because the texts I've seen so far have proofs that look more like a proof out of a math text and not something, say, out of a book on introductory propositional logic.

I've got a specific problem in mind, and am wondering if my proof is correct.

Show that $\vDash \square p \to \sim \sim \square p$, this will be true if for any world $w$ in any model $M$ we have that $\vDash_w^M \square p \to \sim \sim \square p$. Now this is true iff either $\nvDash_w^M \square p$ or $\vDash_w^M \sim \sim \square p$ equivalently iff either $\vDash_w^M \sim\square p$ or $\vDash_w^M \sim \sim \square p$

Obviously this is true.... but it doesn't really seem any more obvious that the initial problem (at least to me).

The notes I'm studying are https://mally.stanford.edu/notes.pdf and the rules for determining if $\vDash_w^M \varphi$ are discussed on page 14 of these.

Thank you for any help.

  • $\begingroup$ To clarify, this is obvious.... but if I had to prove that say $p \vee q \leftrightarrow q \vee p$ simply saying it's obvious isn't a proof... although the proof is easy, it takes some work to actually show it "officially" $\endgroup$ – Squirtle Oct 16 '17 at 22:55

To complete this at a fully formal level, I the starting point needs to be: either $\vDash_w^M \square p$ or $\not\vDash_w^M \square p$. (This is, I think, a baseline "obvious" fact on purely formal grounds, more obvious than "either $\vDash_w^M \square p$ or $\vDash_w^M\sim\square p$", which depends on the "meaning" of $\sim$). As you observed, the conditional is true provided that either $\not\vDash_w^M \square p$ or $\vDash_w^M \sim\sim\square p$, so if $\not\vDash_w^M \square p$, then we're done.

So, the remaining step would be showing that if $\vDash_w^M \square p$, then $\vDash_w^M \sim\sim\square p$. Do you see how to establish that? (The rules on that page give a way of establishing this just by pushing symbols around, without any appeal to what a double-negation "means".)

  • $\begingroup$ thanks. But I guess my problem is precisely establishing "if $\vDash_w^M \square p$, then $\vDash_w^M \sim\sim\square p$". I am also a little confused by what I can do with the "not" on the outside of rule 2, and what exactly to think about "We say $\varphi$ is false at $w$ in $M$ iff $\nvDash_w^M \varphi$" What I want to do is the following: $\vDash_w^M \sim \sim \square p$ is equivalent to $\nvDash_w^M \sim \square p$ which is equivalent to $\sim \vDash_w^M \sim \square p$ which is equivalent to $\sim \nvDash_w^M \square p$ which is equivalent to $\sim \sim \vDash_w^M \square p$ $\endgroup$ – Squirtle Oct 18 '17 at 16:00
  • $\begingroup$ and by double negation this last thing is equivalent to $\vDash_w^M \square p$. This seems too obvious..... it feels wrong..... For one $\sim$ is part of the language, whereas $vDash_w^M$ is part of the metalanguage (which also includes English). So perhaps, rather than pushing out $\sim$, I should push out "not". $\endgroup$ – Squirtle Oct 18 '17 at 16:02
  • $\begingroup$ Yes, I think the distinction between object-language and meta-language is important here, which is why I'm uncomfortable writing things like $\sim\vDash \sim\square p$. One way of thinking about Rule 3 is that it lets us push the $\sim$ out into a "not", the way that you want to do it. The English meaning of "not" tells us that "not not $\vDash \square p$" is the same as "$\vDash \square p$"; it's Rule 3 that lets us connect this to the sentence $\sim\sim\square p$ in the object language. $\endgroup$ – Gregory J. Puleo Oct 18 '17 at 22:51
  • $\begingroup$ Cool. It's good to hear my intuition is making sense. I think in my notes I'll be lazy and just let write $\sim$ rather than "not" but I'll keep in mind that it's part of the metalanguage and not the same as $\sim$ from the language. $\endgroup$ – Squirtle Oct 19 '17 at 3:11

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.