Description of all functions definable by formulæ of the 2nd order intuitionistic propositional calculus on some linear Heyting algebras
D. Pataraia · Journal of Applied Non-Classical Logics · 2006
Explicit description of maps definable by formulæ of the second order intuitionistic propositional calculus is given on two classes of linear Heyting algebras—the dense ones and the ones which possess successors. As a consequence, it is shown that over these classes every formula is equivalent to a quantifier free formula in the dense case, and to a formula with quantifiers confined to the applications of the successor in the second case.