We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...) all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)

Continuing work initiated by Jónsson, Daigneault, Pigozzi and others; Maksimova proved that a normal modal logic (with a single unary modality) has the Craig interpolation property iff the corresponding class of algebras has the superamalgamation property (cf. [Mak 91], [Mak 79]). The aim of this paper is to extend the latter result to a large class of logics. We will prove that the characterization can be extended to all algebraizable logics containing Boolean fragment and having a certain kind of local (...) deduction property. We also extend this characterization of the interpolation property to arbitrary logics under the condition that their algebraic counterparts are discriminator varieties. We also extend Maksimova's result to normal multi-modal logics with arbitrarily many, not necessarily unary modalities, and to not necessarily normal multi-modal logics with modalities of ranks smaller than 2, too.The problem of extending the above characterization result to no n-normal non-unary modal logics remains open. (shrink)