Sets out the basic theory of normal modal and temporal propositional logics; applies this theory to logics of discrete (integer), dense (rational), and continuous (real) time, to the temporal logic of henceforth, next, and until, and to the propositional dynamic logic of regular programs.

We will define cut-free Gentzen-style systems for the modal propositional logics $S4.3 \vee \square)$ and $S4.3Grz \supset A)\supset A)$, and give a syntactical proof of the cut-elimination theorem. As its application, we will give a syntactical proof of the McKinsey-Tarski correspondence between $S_\omega$ and S4.3 and its extension.