A b s t r a c t. We will define cut-free Gentzen-style systems for the modal propositional logics $S4.3 (=S4+ \square(\square A \supset B)\vee \square(\square B \supset A))$ and $S4.3Grz(=S4.3+\square(\square (A \supset \square A) \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.