On Intermediate Predicate Logics of some Finite Kripke Frames,I. Levelwise Uniform Trees

An intermediate predicate logic L is called finite iff it is characterized by a finite partially ordered set M, i.e., iff L is the logic of the class of all predicate Kripke frames based on M. In this paper we study axiomatizability of logics of this kind. Namely, we consider logics characterized by finite trees M of a certain type (levelwise uniform trees) and establish the finite axiomatizability criterion for this case.     

Axiomatic Extensions of IMT3 Logic

In this paper we characterize, classify and axiomatize all axiomatic extensions of the IMT3 logic. This logic is the axiomatic extension of the involutive monoidal t-norm logic given by ¬φ³ ∨ φ. For our purpose we study the lattice of all subvarieties of the class IMT3, which is the variety of IMTL-algebras given by the equation ¬(x³) ∨ x ≈ ?, and it is the algebraic counterpart of IMT3 logic. Since every subvariety of IMT3 is generated by their totally ordered members, we study the structure of all IMT3-chains in order to determine the lattice of all subvarieties of IMT3. Given a family of IMT3-chains the number of elements of the largest odd finite subalgebra in the family and the number of elements of the largest even finite subalgebra in the family turns out to be a complete classifier of the variety generated. We obtain a canonical set of generators and a finite equational axiomatization for each subvariety and, for each corresponding logic, a finite set of characteristic matrices and a finite set of axioms.     

On Finite Models of the Lambek Calculus

We study a class of finite models for the Lambek Calculus with additive conjunction and with and without empty antecedents. The class of models enables us to prove the finite model property for each of the above systems, and for some axiomatic extensions of them. This work strengthens the results of [3] where only product-free fragments of these systems are considered. A characteristic feature of this approach is that we do not rely on cut elimination in opposition to e.g. [5], [9].     

Algebraic Kripke Sheaf Semantics for Non-Classical Predicate Logics

In so-called Kripke-type models, each sentence is assigned either to true or to false at each possible world. In this setting, every possible world has the two-valued Boolean algebra as the set of truth values. Instead, we take a collection of algebras each of which is attached to a world as the set of truth values at the world, and obtain an extended semantics based on the traditional Kripke-type semantics, which we call here the algebraic Kripke semantics. We introduce algebraic Kripke sheaf semantics for super-intuitionistic and modal predicate logics, and discuss some basic properties. We can state the Gödel-McKinsey-Tarski translation theorem within this semantics. Further, we show new results on super-intuitionistic predicate logics. We prove that there exists a continuum of super-intuitionistic predicate logics each of which has both of the disjunction and existence properties and moreover the same propositional fragment as the intuitionistic logic.     

On Extensions of Intermediate Logics by Strong Negation

In this paper we will study the properties of the least extension n() of a given intermediate logic by a strong negation. It is shown that the mapping from to n() is a homomorphism of complete lattices, preserving and reflecting finite model property, frame-completeness, interpolation and decidability. A general characterization of those constructive logics is given which are of the form n (). This summarizes results that can be found already in [13,14] and [4]. Furthermore, we determine the structure of the lattice of extensions of n(LC).