Reports on Mathematical Logic

No. 25 (1991)

Tatsuya SHIMURA

CUT-FREE SYSTEMS FOR THE MODAL LOGIC S4.3 AND S4.3GRZ

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.