Exact definition of SAT problem in S4

Question

I kind of know what SAT problem is and I need the exact formal description of this problem for S4 logic. I am trying to prove this problem is PSPACE-Complete! Any help would be very much appreciated!

Answer 1

Welcome to MSE!

In general, if we are given a logic $\mathcal{L}$ (which includes a notion of semantics), we can ask the $\mathcal{L}\mathsf{SAT}$ problem¹:

If you give me a $\mathcal{L}$-formula $\phi$, is there a model $\mathfrak{M}$ which thinks that $\phi$ is true?

A solution for $\mathcal{L}\mathsf{SAT}$ takes in a formula $\phi$ as input and either outputs a model $\mathfrak{M} \models \phi$ or outputs a ($\mathcal{L}$-)proof that $\phi$ is not satisfiable.

So in your case, a solution to the $\mathsf{S4~SAT}$ problem takes in a sentence in $\mathsf{S4}$ and either outputs

• a (reflexive and transitive) model $\mathfrak{M}$ with a world $w \in \mathfrak{M}$ so that $(\mathfrak{M},w) \models \phi$
• an $\mathsf{S4}$ proof of $\lnot \phi$

The classic reference for proving $\mathsf{PSPACE}$ hardness of this problem is Ladner's paper "The computational complexity of provability in systems of modal propositional logic".

¹: There is definitely a law school joke to be made here...

---

I hope this helps ^_^