An evaluation method, similar to the two-valued one for the classical logic, is introduced to give a decision procedure for some of intermediate logics. The logics treated here are obtained from some logics by adding the axiom av a.

The intermediate logics have been classified into slices (cf. Hosoi [1]), but the detailed structure of slices has been studied only for the first two slices (cf. Hosoi and Ono [2]). In order to study the structure of slices, we give a method of a finer classification of slices & n (n 3). Here we treat only the third slice as an example, but the method can be extended to other slices in an obvious way. It is proved that each (...) subslice contains continuum of logics. A characterization of logics in each subslice is given in terms of the form of models. (shrink)

We give a Gentzen-type formulation GQ for the intermediate logic LQ and prove the cut-elimination theorem on it, where LQ is the propositional logic obtained from the intuitionistic propositional logic LI by adding the axioms of the form AV A.