Prefinitely axiomatizable modal and intermediate logics

A logic Λ bounds a property P if all proper extensions of Λ have P while Λ itself does not. We construct logics bounding finite axiomatizability and logics bounding finite model property in the lattice of intermediate logics and in the lattice of normal extensions of K4.3. MSC: 03B45, 03B55.     

A Modal Logic That is Complete with Respect to Strictly Linearly Ordered <Emphasis Type="Italic">A</Emphasis>-Models

An axiomatization is furnished for a polymodal logic of strictly linearly ordered A-frames: for frames of this kind, we consider a language of polymodal logic with two modal operators, □_< and □_≺. In the language, along with the operators, we introduce a constant β, which describes a basis subset. In the language with the two modal operators and constant β, an Lα-calculus is constructed. It is proved that such is complete w.r.t. the class of all strictly linearly ordered A-frames. Moreover, it turns out that the calculus in question possesses the finite-model property and, consequently, is decidable. __________ Translated from Algebra i Logika, Vol. 44, No. 5, pp. 560–582, September–October, 2005. Supported by RFBR grant No. 03-06-80178, by the Council for Grants (under RF President) and State Aid of Fundamental Science Schools, project NSh-2069.2003.1, and by INTAS grant No. 04-77-7080.     

Quantum logics with the Riesz Interpolation Property

We study the quantum logics which satisfy the Riesz Interpolation Property. We call them the RIP logics. We observe that the class of RIP logics is considerable large—it contains all lattice quantum logics and, also, many (infinite) non‐lattice ones. We then find out that each RIP logic can be enlarged to an RIP logic with a preassigned centre. We continue, showing that the “nearly” Boolean RIP logics must be Boolean algebras. In a somewhat surprising contrast to this, we finally show that the attempt for the σ‐complete formulation of this result fails: We show by constructing an example that there is a non‐Boolean nearly Boolean σ‐RIP logic. As a result, there are interesting σ‐RIP logics which are intrinsically close to Boolean σ‐algebras. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Extensions of Hałkowska–Zajac's three-valued paraconsistent logic

 As it was proved in [4, Sect. 3], the poset of extensions of the propositional logic defined by a class of logical matrices with equationally-definable set of distinguished values is a retract, under a Galois connection, of the poset of subprevarieties of the prevariety generated by the class of the underlying algebras of the defining matrices. In the present paper we apply this general result to the three-valued paraconsistent logic proposed by Hałkowska–Zajac [2]. Studying corresponding prevarieties, we prove that extensions of the logic involved form a four-element chain, the only proper consistent extensions being the least non-paraconsistent extension of it and the classical logic. RID="ID=" <E5>Mathematics Subject Classification (2000):</E5> 03B50, 03B53, 03G10 RID="ID=" <E5>Key words or phrases:</E5> Many-valued logic &ndash; Paraconsistent logic &ndash; Extension &ndash; Prevariety &ndash; Distributive lattice Received 12 August 2000 / Published online: 25 February 2002 RID=" ID=" <E5>Mathematics Subject Classification (2000):</E5> 03B50, 03B53, 03G10 RID=" ID=" <E5>Key words or phrases:</E5> Many-valued logic &ndash; Paraconsistent logic &ndash; Extension &ndash; Prevariety &ndash; Distributive lattice     

Axiomatization and Polynomial Solvability of Strictly Positive Fragments of Certain Modal Logics

The fragment of the language of modal logic that consists of all implications A → B, where A and B are built from variables, the constant ⊤ (truth), and the connectives ∧ and ◊₁,◊₂,...,◊ _m . For the polymodal logic S5 _m (the logic of m equivalence relations) and the logic K4.3 (the logic of irreflexive linear orders), an axiomatization of such fragments is found and their algorithmic decidability in polynomial time is proved.

     

La connaissance commune en logique modale

The problem of Common Knowledge will be considered in two classes of models: a class K.* of Kripke models and a class S of Scott models. Two modal logic systems will be defined. Those systems, KC and MC, include an axiomatisation of Common Knowledge. We prove determination of each system by the corresponding class of models. MSC: 03B45, 68T25.     

The Lattice of Deductive Systems on Hilbert Algebras

The concept of deductive system on a Hilbert algebra was introduced by A. Diego. We show that the set Ded A of all deductive systems on a Hilbert algebra A forms an algebraic lattice which is distributive.AMS Classification (2000): 06F35, 03G25, 08A30     

Local computation in linear logic

This work deals with the exponential fragment of Girard's linear logic ([3]) without the contraction rule, a logical system which has a natural relation with the direct logic ([10], [7]). A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be introduced in a natural manner. Its main properties — normalizability and confluence — has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism ([6]) with respect to the logical system in question. MSC: 03B40, 03F05.     

Algebraic axiomatization of tense intuitionistic logic

We introduce two unary operators G and H on a relatively pseudocomplemented lattice which form an algebraic axiomatization of the tense quantifiers “it is always going to be the case that” and “it has always been the case that”. Their axiomatization is an extended version for the classical logic and it is in accordance with these operators on many-valued Łukasiewicz logic. Finally, we get a general construction of these tense operators on complete relatively pseudocomplemented lattice which is a power lattice via the so-called frame.     

A simplified functorial construction of the veblen hierarchy

We give a simple and elementary proof of the following result of Girard and Vauzeilles which is proved in [5]: “The binary Veblen function ψ: On × On — On is a dilator.” Our proof indicates the intimate connection between the traditional theory of ordinal notation systems and Girard's theory of denotation systems. MSC: 03F15.     

A new correctness criterion for multiplicative non-commutative proof nets

 We introduce a new correctness criterion for multiplicative non commutative proof nets which can be considered as the non-commutative counterpart to the Danos-Regnier criterion for proof nets of linear logic. The main intuition relies on the fact that any switching for a proof net (obtained by mutilating one premise of each disjunction link) can be naturally viewed as a series-parallel order variety (a cyclic relation) on the conclusions of the proof net. Received: 8 November 2000 / Revised version: 21 June 2001 / Published online: 2 September 2002 Research supported by the EU TMR Research Programme ``Linear Logic and Theoretical Computer Science'. Mathematics Subject Classification (2000): 03F03, 03F07, 03F52, 03B70 Key words or phrases: Linear and non-commutative logic – Proof nets – Series-parallel orders and order varieties     

The modal logic of the countable random frame

 We study the modal logic M L ^r of the countable random frame, which is contained in and `approximates' the modal logic of almost sure frame validity, i.e. the logic of those modal principles which are valid with asymptotic probability 1 in a randomly chosen finite frame. We give a sound and complete axiomatization of M L ^r and show that it is not finitely axiomatizable. Then we describe the finite frames of that logic and show that it has the finite frame property and its satisfiability problem is in EXPTIME. All these results easily extend to temporal and other multi-modal logics. Finally, we show that there are modal formulas which are almost surely valid in the finite, yet fail in the countable random frame, and hence do not follow from the extension axioms. Therefore the analog of Fagin's transfer theorem for almost sure validity in first-order logic fails for modal logic. Received: 1 May 2000 / Revised version: 29 July 2001 / Published online: 2 September 2002 Mathematics Subject Classification (2000): 03B45, 03B70, 03C99 Key words or phrases: Modal logic – Random frames – Almost sure frame validity – Countable random frame – Axiomatization – Completeness     

Ultrapowers as sheaves on a category of ultrafilters

In the paper we investigate the topos of sheaves on a category of ultrafilters. The category is described with the help of the Rudin-Keisler ordering of ultrafilters. It is shown that the topos is Boolean and two-valued and that the axiom of choice does not hold in it. We prove that the internal logic in the topos does not coincide with that in any of the ultrapowers. We also show that internal set theory, an axiomatic nonstandard set theory, can be modeled in the topos.Mathematics Subject Classification (2000): Primary 03G30, 03C20, Secondary 03E05, 03E70, 03H05The author would like to thank the Mittag-Leffler Institute for partial suport.     

Hilbert's ϵ-operator in intuitionistic type theories

We investigate Hilbert's ?-calculus in the context of intuitionistic type theories, that is, within certain systems of intuitionistic higher-order logic. We determine the additional deductive strength conferred on an intuitionistic type theory by the adjunction of closed ?-terms. We extend the usual topos semantics for type theories to the ?-operator and prove a completeness theorem. The paper also contains a discussion of the concept of “partially defined” ?-term. MSC: 03B15, 03B20, 03G30.     

Join-semilattices whose sections are residuated PO-monoids

We generalize the concept of an integral residuated lattice to join-semilattices with an upper bound where every principal order-filter (section) is a residuated semilattice; such a structure is called a sectionally residuated semilattice. Natural examples come from propositional logic. For instance, implication algebras (also known as Tarski algebras), which are the algebraic models of the implication fragment of the classical logic, are sectionally residuated semilattices such that every section is even a Boolean algebra. A similar situation rises in case of the Lukasiewicz multiple-valued logic where sections are bounded commutative BCK-algebras, hence MV-algebras. Likewise, every integral residuated (semi)lattice is sectionally residuated in a natural way. We show that sectionally residuated semilattices can be axiomatized as algebras (A, r, →, ⇝, 1) of type 〈3, 2, 2, 0〉 where (A, →, ⇝, 1) is a {→, ⇝, 1}-subreduct of an integral residuated lattice. We prove that every sectionally residuated lattice can be isomorphically embedded into a residuated lattice in which the ternary operation r is given by r(x, y, z) = (x · y) ∨ z. Finally, we describe mutual connections between involutive sectionally residuated semilattices and certain biresiduation algebras. This work was supported by the Czech Government via the project MSM6198959214.     

The Maximal Closed Classes of Unary Functions in p-Valued Logic

In many-valued logic the decision of functional completeness is a basic and important problem, and the thorough solution to this problem depends on determining all maximal closed sets in the set of many-valued logic functions. It includes three famous problems, i.e., to determine all maximal closed sets in the set of the total, of the partial and of the unary many-valued logic functions, respectively. The first two problems have been completely solved ([1], [2], [8]), and the solution to the third problem boils down to determining all maximal subgroups in the k-degree symmetric group S_k, which is an open problem in the finite group theory. In this paper, all maximal closed sets in the set of unary p-valued logic functions are determined, where p is a prime. Mathematics Subject Classification: 03B50, 20B35.     

A normalizing system of natural deduction for intuitionistic linear logic

 The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for -formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cut-free derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cut-elimination. Received: 10 October 2000 / Revised version: 26 July 2001 / Published online: 2 September 2002 Mathematics Subject Classification (2000): 03F52, 03F05 Keywords or phrases: Linear logic – Natural deduction – General elimination rules     

A simplified proof of arithmetical completeness theorem for provability logic GLP

We present a simplified proof of Japaridze’s arithmetical completeness theorem for the well-known polymodal provability logic GLP. The simplification is achieved by employing a fragment J of GLP that enjoys a more convenient Kripke-style semantics than the logic considered in the papers by Ignatiev and Boolos. In particular, this allows us to simplify the arithmetical fixed point construction and to bring it closer to the standard construction due to Solovay.