For intermediate logics, there is obtained in the paper an algebraic equivalent of the disjunction propertyDP. It is proved that the logic of finite binary trees is not maximal among intermediate logics withDP. Introduced is a logicND, which has the only maximal extension withDP, namely, the logicML of finite problems.

A family of prepositional logics is considered to be intermediate between the intuitionistic and classical ones. The generalized interpolation property is defined and proved is the following.Theorem on interpolation. For every intermediate logic L the following statements are equivalent:(i) Craig's interpolation theorem holds in L, (ii) L possesses the generalized interpolation property, (iii) Robinson's consistency statement is true in L.

Three variants of Beth's definability theorem are considered. Let L be any normal extension of the provability logic G. It is proved that the first variant B1 holds in L iff L possesses Craig's interpolation property. If L is consistent, then the statement B2 holds in L iff L = G + {0}. Finally, the variant B3 holds in any normal extension of G.