of propositional formulas that are valid in H is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its Lindenbaum–Tarski algebra, which is then a Heyting algebra. An intuitionistic Kripke frame F is a partially ordered set, and a Kripke model M is a Kripke frame with valuation such that is an upper subset of F. The set of propositional formulas that are valid in F is an intermediate logic. Given an intermediate logic L it is possible to construct a Kripke model M such that the logic of M is L (this construction is called the canonical model). A Kripke frame with this property may not exist, but a general frame always does. Relation to modal logics Let A be a propositional formula. The Gödel–Tarski translation of A is defined recursively as follows: If M is a modal logic extending S4 then ρM = {A | T(A) ∈ M} is a superintuitionistic logic, and M is called a modal companion of ρM. In particular: IPC = ρS4 KC = ρS4.2 LC = ρS4.3 CPC = ρS5 For every intermediate logic L there are many modal logics M such that L = ρM. See also List of logic systems References Toshio Umezawa. On logics intermediate between intuitionistic and classical predicate logic. Journal of Symbolic Logic, 24(2):141–153, June 1959. Alexander Chagrov, Michael Zakharyaschev. Modal Logic. Oxford University Press, 1997. Systems of formal logic Propositional calculus Non-classical logic