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