>>16683319 (OP)
Its the following system of abreviations: Let $L$ be a first-order language. We add to $L$ two unary predicate $W$,a binary predicate $M$, a binary predicate $\leq$, and for every n-place relation symbol $R(x_1,...,x_n)$, a $(n+1)$-place relation symbol $R^*(y, x_1,...,x_n)$. We pick a new set of variables $\Omega:= \{w_1,w_2,w_3...\}$ and define:
1°) $w \Vdash R(t_1,...t_n):= R^*(w,t_1...,t_n)$ for every $w \in \Omega$, every relation symbol $R$ and every terms of the original language $t_1,...,t_n$ (not containing letters from $\Omega$)
2°) $w \Vdash \perp$:= \perp
3°) $w \Vdash A \to B:= (w \Vdash A) \to (W \Vdash B)$
4°) $w \Vdash \forall x C:= \forall x, M(w,x) \to (w \Vdash C)$
5°) $w \Vdash \Box D:= \forall v, W(v) \to w \leq v \to v \Vdash D$
If you add the axioms saying that $\le$ id a preorder and $M$ is increasing (i.e. $\forall x, a, b, W(a) \to W(b) \to M(a,x) \to a \leq b \to M(b,x)$) then the set of theorems of modal logic S4 can be interpreted in the system above (with classical logic).
