Algebraic semantics for superintuitionistic predicate logics

We construct a unified algebraic semantics for superintuitionistic predicate logics. Assigned to each predicate logic is some deductive system of a propositional language which is kept fixed throughout all predicate superintuitionistic ones. Given that system, we build up a variety of algebras w.r.t. which a given logic is proved to be strongly complete. Supported by the Russian Arts Foundation (RAF), grant No. 97-03-04089a. Translated fromAlgebra i Logika, Vol. 38, No. 1, pp. 68–95, January–February, 1999.     

Predicate superintuitionistic logics without interpolation

Predicate superintuitionistic logics are considered. We prove that all such logics that contain a logic characterized by frames whose domains are all finite and are contained in the classical logic of finite domains do not have the interpolation and Beth properties. It is also established that the interpolation property is not shared by all predicate superintuitionistic logics which contain a logic characterized by frames whose domains of nonfinal worlds are all finite and which are contained in a logic characterized by all two-element frames with finite constant domains. Supported by the Competitive Basic Research Center of St. Petersburg State University, grant No. 93-1-88-12. Translated fromAlgebra i Logika, Vol. 35, No. 1, pp. 105–117, January–February, 1996.     

Superintuitionistic logics and the projective beth property

It is proved that in superintuitionistic logics, the projective Beth property follows from the Craig interpolation property, but the converse does not hold. A criterion is found which allows us to reduce the problem asking whether the projective Beth property is valid in superintuitionistic logics to suitable properties of varieties of pseudoboolean algebras. It is shown that the principle of variable separation follows from the projective Beth property. On the other hand, the interpolation property in a logic L implies the projective Beth property in Δ(L). Supported by RFFR grants No. 96-01-01552 and No. 99-01-00600. Translated fromAlgebra i Logika, Vol. 38, No. 6, pp. 680–696, November–December, 1999.     

The Projective Beth Property and Interpolation in Positive and Related Logics

We look at the interplay between the projective Beth property in non-classical logics and interpolation. Previously, we proved that in positive logics as well as in superintuitionistic and modal ones, the projective Beth property PB2 follows from Craig's interpolation property and implies the restricted interpolation property IPR. Here, we show that IPR and PB2 are equivalent in positive logics, and also in extensions of the superintuitionistic logic KC and of the modal logic Grz.2. Supported by RFBR grant No. 06-01-00358, by INTAS grant No. 04-77-7080, and by the Council for Grants (under RF President) and State Aid of Fundamental Science Schools, project NSh-2069.2003.1. __________ Translated from Algebra i Logika, Vol. 45, No. 1, pp. 85–113, January–February, 2006.     

Restricted interpolation property in superintuitionistic logics

The restricted interpolation property IPR in modal and superintuitionistic logics is investigated. It is proved that in superintuitionistic logics of finite slices and in finite-slice extensions of the Grzegorczyk logic, the property IPR is equivalent to the projective Beth property PB2. Supported by RFBR (project No. 06-01-00358) and by the Council for Grants (under RF President) and State Aid of Leading Scientific Schools (grant NSh-335.2008.1). Translated from Algebra i Logika, Vol. 48, No. 1, pp. 54-89, January-February, 2009.     

ON SOME INTERPRETATIONS OF CLASSICAL LOGIC

In distinction from the well-known double-negation embeddings of the classical logic we consider some variants of single-negation embeddings and describe some classes of superintuitionistic first-order predicate logics in which the classical first-order calculus is interpretable in such a way. Also we find the minimal extensions of Heyting's logic in which the classical predicate logic can be embedded by means of these translations.     

Table admissible inference rules

A recursive basis of inference rules is described which are instantaneously admissible in all table (residually finite) logics extending one of the logics Int and Grz. A rather simple semantic criterion is derived to determine whether a given inference rule is admissible in all table superintuitionistic logics, and the relationship is established between admissibility of a rule in all table (residually finite) superintuitionistic logics and its truth values in Int. Translated from Algebra i Logika, Vol. 48, No. 3, pp. 400–414, May–June, 2009.     

The relation between intuitionistic and classical modal logics

Intuitionistic propositional logicInt and its extensions, known as intermediate or superintuitionistic logics, in many respects can be regarded as just fragments of classical modal logics containingS4. The main aim of this paper is to construct a similar correspondence between intermediate logics augmented with modal operators—we call them intuitionistic modal logics—and classical polymodal logics We study the class of intuitionistic polymodal logics in which modal operators satisfy only the congruence rules and so may be treated as various sorts of □ and ◇. Supported by the Alexander von Humboldt Foundation. Translated fromAlgebra i Logika, Vol. 36, No. 2, pp. 121–155, March–April, 1997.     

Joint consistency in extensions of the minimal logic

Analogs of Robinson’s theorem on joint consistency are found which are equivalent to the weak interpolation property (WIP) in extensions of Johansson’s minimal logic J. Although all propositional superintuitionistic logics possess this property, there are J-logics without WIP. It is proved that the problem of the validity of WIP in J-logics can be reduced to the same problem over the logic Gl obtained from J by adding the tertium non datur. Some algebraic criteria for validity of WIP over J and Gl are found.     

Intermediate predicate logic without the beth property

It is shown that a logic J _fd ^* characterized by all Kripke frames the domains of all nonmaximal worlds of which are finite lacks the Beth property. The logic is the first example of an intermediate superintuitionistic logic without the Beth property. The interpolation and the Beth properties are also proved missing in all predicate superintuitionistic logics which contain J _fd ^* and are contained in a logic characterized by frames of the form〈N _n , ≤,{Dk}k∈N n〉. Supported by the Russian Foundation for Humanities, grant No. 97-03-04089. Translated fromAlgebra i Logika, Vol. 37, No. 1, pp. 107–117, January–February, 1998.     

Interpolation in superintuitionistic predicate logics with equality

It is shown that the Craig interpolation property and the Beth property are preserved under passage from a superintuitionistic predicate logic to its extension via standard axioms for equality, and under adding formulas of pure equality as new axioms. We find an infinite independent set of formulas which, though not equivalent to formulas of pure equality, may likewise be added as new axiom schemes without loss of the interpolation, or Beth, property. The formulas are used to construct a continuum of logics with equality, which are intermediate between the intuitionistic and classical ones, having the interpolation property. Moreover, an equality-free fragment of the logics constructed is an intuitionistic predicate logic, and formulas of pure equality satisfy all axioms of the classical predicate logic. Supported by RFFR grant No. 96-01-01552. Translated fromAlgebra i Logika, Vol. 36, No. 5, pp. 543–561, September–October, 1997.     

Proof complexity of intuitionistic implicational formulas

We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions.In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrube? (2007), generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Je?ábek (2009), can be realized by implicational tautologies.     

Complexity of admissible rules

We investigate the computational complexity of deciding whether a given inference rule is admissible for some modal and superintuitionistic logics. We state a broad condition under which the admissibility problem is coNEXP-hard. We also show that admissibility in several well-known systems (including GL, S4, and IPC) is in coNE, thus obtaining a sharp complexity estimate for admissibility in these systems. The research was done while the author was visiting the Department of Philosophy of the Utrecht University. Supported by grant IAA1019401 of GA AV ČR     

Projective beth properties in modal and superintuitionistic logics

Projective Beth properties in superintuitionistic and normal modal logics are considered. Their interrelations and connections with interpolation properties of the logics are established. Algebraic counterparts for the projective Beth properties are found out. Supported by the Russian Humanitarian Science Foundation, grant No. 97-03-04089. Translated fromAlgebra i Logika, Vol. 38, No. 3, pp. 316–333, May–June, 1999.     

Fuzzy logics with modalities

We explore the basic fuzzy logic BL as well as propositional fuzzy logics with modalities □ and ◊ and a total accessibility relation. Formulations and proofs are given to replacement theorems for BL. A basic calculus of modal fuzzy logic is introduced. For this calculus and its extensions, we prove replacement and deduction theorems. Supported by RFBR grant No. 06-01-00358, by INTAS grant No. 04-77-7080, and by the Council for Grants (under RF President) and State Aid of Fundamental Science Schools, project NSh-4787.2006.1. __________ Translated from Algebra i Logika, Vol. 45, No. 6, pp. 731–757, November–December, 2006.     

A method of proving interpolation in paraconsistent extensions of the minimal logic

The interpolation property in extensions of Johansson’s minimal logic is investigated. The construction of a matched product of models is proposed, which allows us to prove the interpolation property in a number of known extensions of the minimal logic. It is shown that, unlike superintuitionistic, positive, and negative logics, a sum of J-logics with the interpolation property CIP may fail to possess _CIP, nor even the restricted interpolation property. Supported by RFBR grant No. 06-01-00358, by INTAS grant No. 04-77-7080, and by the Council for Grants (under RF President) and State Aid of Fundamental Science Schools, project NSh-4787.2006.1. __________ Translated from Algebra i Logika, Vol. 46, No. 5, pp. 627–648, September–October, 2007.     

The Skolemization of prenex formulas in intermediate logics

The skolem class of a logic consists of the formulas for which the derivability of the formula is equivalent to the derivability of its Skolemization. In contrast to classical logic, the skolem classes of many intermediate logics do not contain all formulas. In this paper it is proven for certain classes of propositional formulas that any instance of them by (independent) predicate sentences in prenex normal form belongs to the skolem class of any intermediate logic complete with respect to a class of well-founded trees. In particular, all prenex sentences belong to the skolem class of these logics, and this result extends to the constant domain versions of these logics.     

The Beth property and interpolation in lattice-based algebras and logics

We deal with logics based on lattices with an additional unary operation. Interrelations of different versions of interpolation, the Beth property, and amalgamation, as they bear on modal logics and varieties of modal algebras, superintuitionistic logics and varieties of Heyting algebras, positive logics and varieties of implicative lattices, have been studied in many works. Sometimes these relations can and sometimes cannot be extended to the logics without implication considered in the paper. Supported by INTAS (grant No. 04-77-7080) and by RFBR (grant No. 06-01-00358). Supported by INTAS grant No. 04-77-7080. __________ Translated from Algebra i Logika, Vol. 47, No. 3, pp. 307–334, May–June, 2008.     

Independent bases for admissible rules in pretable logics

Independent bases of admissible inference rules are studied; namely, we treat inference rules in pretable modal logics over S4, and in pretable superintuitionistic logics. The Maksimova-Esakia-Meskhi theorem holds that there exist exactly five pretable S4-logics and precisely three pretable superintuitionistic ones. We argue that all pretable modal logics and all pretable super-intuitionistic logics have independent bases for admissible inference rules. Supported by RFFR, and Rybakov’s part, by the Turkish Scientific Technical Research Council (TUBITAK, Ankara). Translated fromAlgebra i Logika, Vol. 39, No. 2, pp. 206–226, March–April, 2000.