The Journal of Symbolic Logic

Research Article

The superintuitionistic predicate logic of finite Kripke frames is not recursively axiomatizable

Dmitrij Skvortsov

All-Russian Institute of Scientific and Technical Information, Molodogvardejskaja 22, Korp. 3, KV. 29, 121351, Moscow, Russia, E-mail:


We prove that an intermediate predicate logic characterized by a class of finite partially ordered sets is recursively axiomatizable iff it is “finite”, i.e., iff it is characterized by a single finite partially ordered set. Therefore, the predicate logic LFin of the class of all predicate Kripke frames with finitely many possible worlds is not recursively axiomatizable.

(Received July 02 2004)

(Accepted November 04 2004)