Non-axiomatizable second order intuitionistic propositional logic Original Research Article

The second order intuitionistic propositional logic characterized by the class of all “principal” Kripke frames (i.e. frames with the quantifiers ranging over all upward-closed sets) is non-recursively axiomatizable, as well as any logic of a class of principal Kripke frames containing every finite frame.