Is there a kind of modal logic that models boolean satisfiability?

Question

For example, if $p$ is a boolean proposition depending on truth values $q_1, q_2 \dots ,q_n$, can we add a modal operator such that $\diamond p$ holds if and only if there exists some boolean valuation of $q_1,q_2, \dots q_n$ such that $p$ is true, and $\square p $ holds precisely when $p$ is true for any valuation of $q_1, q_2 \dots ,q_n$, thus defining a sort of modal logic of satisfiability? If so, has this sort of system been studied. What is it called?

Answer 1

(I am sorry if I failed to understand the question.)

Do you mean, that p is a boolean formula, built from variables $q_1, ...,q_n$, boolean operators and parentheses? If yes, then for some model and state $M$ and $w$: $(M,w) \models\Diamond \varphi$ (I will use $\varphi$ instead of $p$ to avoid ambiguity) iff for some state $v: R(w,v)$ and $(M, v) \models \varphi$. So, diamond modality says, that if $\Diamond \varphi$ holds in the current state, then there is a successor-state, where $\varphi$ holds (i.e. propositional variables in $\varphi$ has the valuation, which makes $\varphi$ true). The reverse direction is the same.

If $\varphi$ is true for every valuation of propositional variables, then $\varphi$ is a tautology, i.e. it holds in every possible world. So is $\square \varphi$, if there are no dead-end worlds in the given frame (i.e. the frame is serial).

Personally, I don't think there is such a modal logic of satisfiability. The desired properties could be obtained in the frame with $2^n$ states, where $n$ is the number of considered propositional variables. In a such kind of frames, we would have worlds for all possible valuations of propositional variables (something like a truth-table), and diamond and box operators has the same usual meaning. (The frame should be serial!)