Abstract
In [Ono 1987] H. Ono put the question about axiomatizing the intermediate predicate logicLFin characterized by the class of all finite Kripke frames (Problem 4,P41). It was established in [Skvortsov 1988] thatLFin is not recursively axiomatizable. One can easily show that for any finite posetM, the predicate logic characterized byM is recursively axiomatizable, and its axiomatization can be constructed effectively fromM. Namely, the set of formulas belonging to this logic is recursively enumerable, since it is embeddable in the two-sorted classical predicate calculusCPC 2 (the definition of the truth in a Kripke model may be expressed by a formula ofCPC 2). Thus the logicLFin is II 02 -arithmetical.
Here we give a more explicit II 02 -description ofLFin: it is presented as the intersection of a denumerable sequence of finitely axiomatizable Kripke-complete logics. Namely, we give an axiomatization of the logicLB n P + m characterized by the class of all posets of the finite height ⩽m and the finite branching ⩽n. A finite axiomatization of the predicate logicLP + m characterized by the class of all posets of the height ⩽m is known from [Yokota 1989] (this axiomatics is essentially first-order; the standard propositional axiom of the height ⩽m is not sufficient [Ono 1983]). We prove thatLB n P + m =(LP + m +B n),B n being the propositional axiom of the branching ⩽n (see [Gabbay, de Jongh 1974]).
Our terminology and notations mainly correspond to [Ono 1987].
Similar content being viewed by others
References
Corsi, G., 1992, ‘Completeness Theorem for Dummett'sLC Quantified and some of its Extensions’,Studia Logica 51, No. 2, 317–335.
Corsi, G. andS. Ghilardi, 1989, ‘Directed Frames’,Archive for Math. Logic 29, No. 1, 53–67.
Gabbay, D. 1981, ‘Semantical Investigations in Heyting's Intuitionistic Logic’,Synthese Library 148.
Gabbay, D. andG. de Jongh, 1974, ‘Sequence of Decidable Finitely Axiomatizable Intermediate Logics with the Disjunction Property’,Journal of Symbolic Logic 39, No. 1, 67–78.
Ghiraldi, S., 1989, ‘Presheaf Semantics and Independence Results for some Non-clasical First-order Logics’,Archive for Math. Logic 29, No. 2, 125–136.
Ghiraldi, S., 1991, ‘Incompleteness Results in Kripke Semantics’,Journal of Symbolic Logic 56, No. 2, 517–538.
Komori, Y., 1983, ‘Some Results on the Superintuitionistic Predicate Logics’,Reports on Math. Logic 15, 13–31.
Ono, H., 1983, ‘Model Extension Theorem and Craig's Interpolation Theorem for Intermediate Predicate Logics’,Reports on Math. Logic 15, 41–58.
Ono, H., 1987, ‘Some Problems in Intermediate Predicate Logics’,Reports on Math. Logic 21, 55–67.
Ono, H., 1988, ‘On Finite Linear Intermediate Predicate Logics’,Studia Logica 47, No. 4, 391–399.
Shehtman V. andD. Skvortsov, 1990, ‘Semantics of Non-classical First-ordered Predicate Logics’, in:Mathematical Logic, Proc. of Summer school and conference in math. logic, Heyting'88, P. Petkov (ed.), Plenum Press, N.Y. 105–116.
Shimura, T., 1993, ‘Kripke Completeness of some Intermediate Predicate Logics with the Axiom of Consist Domain and a Variant of Canonical Formulas’,Studia Logica 52, No. 1, 23–40.
Skvortsov, D., 1988, ‘On Axiomatizability of some Intermediate Predicate Logics’ (Summary),Reports on Math. Logic 22, 115–116.
Yokota, S., 1989, ‘Axiomatization of the First-order Intermediate Logics of Bounded Kripkean Heights, I’,Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 35, No. 5, 414–421.
Yokota, S., 1991, ‘Axiomatization of the First-order Intermediate Logics of Bounded Kripkean Heights, II’,Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 37, No. 1, 17–26.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Skvortsov, D. On the predicate logics of finite Kripke frames. Stud Logica 54, 79–88 (1995). https://doi.org/10.1007/BF01058533
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01058533