1

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.

Squirtle
  • 6,698
  • 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" – Squirtle Oct 16 '17 at 22:55

1 Answers1

0

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".)

Gregory J. Puleo
  • 6,443
  • 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$

     – Squirtle Oct 18 '17 at 16:00
  • 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". – Squirtle Oct 18 '17 at 16:02
  • 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. – Gregory J. Puleo Oct 18 '17 at 22:51
  • 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. – Squirtle Oct 19 '17 at 03:11