Intermediate logical systems, or “intermediate logics” as they are often called, are systems between intuitionistic and classical logic in deductive strength. Axiomatic versions of intermediate logical systems are obtained by the addition of different, classically valid axioms to intuitionistic logic. A drawback of this approach is that the proof-theoretic properties of axiomatic systems are weak.

In this chapter, we shall study intermediate logical systems by various methods: One is to translate well-known natural deduction rules into sequent calculus. Another is to add axioms in the style of the rule of excluded middle of Chapter 5 and the nonlogical rules of Chapter 6. We have seen that failure of the strict subformula property is no obstacle to structural proof analysis: It is sufficient to have some limit to the weight of formulas that can disappear in a derivation. A third approach to intermediate logical systems is to relax the right implication rule of multisuccedent intuitionistic sequent calculus by permitting formulas of certain types to appear in the succedent of its premiss, in addition to the single formula of the intuitionistic rule.

From a result of Gödel (1932) it follows that there is an infinity of nonequivalent intermediate logical systems. Some of these arise from natural axioms, such as the law of double negation, the weak law of excluded middle, etc.

There are approaches to intermediate logical systems, in which some property such as validity of an interpolation theorem or some property of algebraic models is assumed. The general open problem behind these researches concerns the structure of the implicational lattice of intuitionistic logic (in the first place, propositional logic).