Valuation Semantics for S4

This expository paper presents an application, to the modal logic S4, of the valuation semantics technique proposed by Lopari & cacute; for the basic normal modal logic K. In previous works we presented a valuation semantics for the minimal temporal logic Kt and several other systems modal and temporal logic. How to deal with S4, however, was left as an open problem-although we arrived at a working definition of A1,& mldr;,An\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$A_1,\ldots ,A_n$$\end{document}-valuations, we were not able to prove an important lemma for correctness. In this paper we solve this, presenting valuations for S4.