##
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.

Back to Main Menu