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     

A logic of implications in algebra and coalgebra

Implications in a category can be presented as epimorphisms: an object satisfies the implication iff it is injective with respect to that epimorphism. G. Ro?u formulated a logic for deriving an implication from other implications. We present two versions of implicational logics: a general one and a finitary one (for epimorphisms with finitely presentable domains and codomains). In categories Alg Σ of algebras on a given signature our logic specializes to the implicational logic of R. Quackenbush. In categories Coalg H of coalgebras for a given accessible endofunctor H of sets we derive a logic for implications in the sense of P. Gumm.     

Homology of proof-nets

This work defines homology groups for proof-structures in multiplicative linear logic (see [Gir1], [Gir2], [Dan]). We will show that these groups characterize proof-nets among arbitrary proof-structures, thus obtaining a new correctness criterion and of course a new polynomial algorithm for testing correctness. This homology also bears information on sequentialization. An unexpected geometrical interpretation of the linear connectives is given in the last section. This paper exclusively focuses onabstract proof-structures, i.e. paired-graphs. The relation with actual proofs is investigated in [Gir1], [Gir2], [Dan], [Ret] and [Tro].     

Subgroups of bounded residue in ultraproducts of finite groups

We consider a variety of linearity generalizations: finitary linearizability, local linearizability, and so on. The natural partial ordering on the set of classes of generalized linear groups under examination is described in full. Criteria for abstract groups to be finitary linearized in terms of ultraproducts of linear and finite groups are proven. Examples of nilpotent groups are given which have not faithful finitary linear representations by automorphisms of vector spaces over a field. Translated fromAlgebra i Logika, Vol. 36, No. 5, pp. 531–542, September–October, 1997.     

Dynamic linear time temporal logic

A simple extension of the propositional temporal logic of linear time is proposed. The extension consists of strengthening the until operator by indexing it with the regular programs of propositional dynamic logic. It is shown that DLTL, the resulting logic, is expressively equivalent to the monadic second-order theory of ω-sequences. In fact, a sublogic of DLTL which corresponds to propositional dynamic logic with a linear time semantics is already expressively complete. We show that DLTL has an exponential time decision procedure and admits a finitary axiomatization. We also point to a natural extension of the approach presented here to a distributed setting.     

Random variables and integral logic

We study model theory of random variables using finitary integral logic. We prove definability of some probability concepts such as having F(u) as distribution function, independence and martingale property. We then deduce Kolmogorov's existence theorem from the compactness theorem.     

How accessible are categories of algebras?

For locally finitely presentable categories it is well known that categories of F-algebras, where F is a finitary endofunctor, are also locally finitely presentable. We prove that this generalizes to locally finitely multipresentable categories. But it fails, in general, for finitely accessible categories: we even present an example of a strongly finitary functor F (one that preserves finitely presentable objects) whose category of F-algebras is not finitely accessible. On the other hand, categories of F-algebras are proved to be ω₁-accessible for all strongly finitary functors—and it is an open problem whether this holds for all finitary functors.     

Self-reference and the acyclicity of rational choice

Guided by an analogy between the logic of truth and the logic of a rationally choosing agent, I propose for the latter a principle of acyclicity, which blocks paradoxical self-referring reasoning. Certain decision-theoretic paradoxes are used to illustrate what can happen when acyclicity is violated. The principle, however, is argued for directly on grounds of coherence. Among its consequences are certain decision-theoretic rules, as well as a guiding line for setting Bayesian prior probabilities. From this perspective I discuss in the last two sections Prisoner's Dilemma and Newcomb's Paradox.     

On the acyclicity of integral funnels

The condition of acyclicity of the solution set of the Cauchy problem for an ordinary differential equation can be used in the theory of boundary value problems.However, the acyclicity of a funnel does not imply the acyclicity of sections of the funnel for a fixed time. There exist acyclic integral funnels whose time sections are not acyclic. In the present paper, we show that there is a relationship in the reverse direction: the acyclicity of time sections of integral funnels implies the acyclicity of the funnels themselves. This fact can simplify the application of existence theorems for boundary value problems to specific equations.     

Free products of finitary skew linear groups

We give two very different proofs of the following result. Let {G _γ:λɛΛ : λ ∈ Λ} be a family of finitary skew linear groups of the same characteristic p ≧ 0. Then the free product of the G _γ is isomorphic to some finitary skew linear group of characteristic p. This extends recent work of R. J. H. Minty on the skew linear case and of O. Puglisi on the finitary linear case.     

Coeffective Numbers of Riemannian 8-Manifolds with Holonomy in Spin(7)

We introduce a differential complex of coeffective type for anySpin(7)-manifold M locally conformal to aRiemannian 8-manifold with holonomy contained in Spin(7).Local properties of this complex, such as ellipticity and acyclicity,are studied. The relationship between the coeffective cohomology ofM and the topology of the manifold is discussed in the caseof M having a subgroup of Spin(7) as aholonomy group.     

On the intersection of infinite matroids

We show that the infinite matroid intersection conjecture of Nash-Williams implies the infinite Menger theorem proved by Aharoni and Berger in 2009.We prove that this conjecture is true whenever one matroid is nearly finitary and the second is the dual of a nearly finitary matroid, where the nearly finitary matroids form a superclass of the finitary matroids.In particular, this proves the infinite matroid intersection conjecture for finite-cycle matroids of 2-connected, locally finite graphs with only a finite number of vertex-disjoint rays.     

A Decision Procedure for Nonperiodic Sequents of the First-Order Linear Temporal Logic

A deduction-based decision procedure is presented for the nonperiodic D-sequents of the first-order linear temporal logic. The D-sequents are obtained from D ₂-sequents [7], [8] by removing the periodicity condition. The deductive procedure proposed consists of decidable deductive procedures that replace infinitary and finitary induction rules for the temporal operator ``always'. The soundness and completeness of the deduction-based decision procedure proposed is proved.     

N.A. Vasil’ev’s Logical Ideas and the Categorical Semantics of Many-Valued Logic

Here we suggest a formal using of N.A. Vasil’ev’s logical ideas in categorical logic: the idea of “accidental” assertion is formalized with topoi and the idea of the notion of nonclassical negation, that is not based on incompatibility, is formalized in special cases of monoidal categories. For these cases, the variant of the law of “excluded n-th” suggested by Vasil’ev instead of the tertium non datur is obtained in some special cases of these categories. The paraconsistent law suggested by Vasil’ev is also demonstrated with linear and tensor logics but in a form weaker than he supposed. As we have, in fact, many truth-values in linear logic and topos logic, the admissibility of the traditional notion of inference in the categorical interpretation of linear and intuitionistic proof theory is discussed.     

Relational systems with trivial endomorphisms and polymorphisms

A finitary relation ? and a finitary function f on some set A are said to be compatible one with the other if ? is a subalgebra of a suitable direct power of (A, f). In this paper properties for relational systems (A, Q) are derived in order to guarantee that every (finitary) function compatible with all relations of Q must be a projection or constant. The connection to interpolation properties is demonstrated and some open problems are stated.     

线性逻辑和态极逻辑引论(Ⅰ)

《线性逻辑和态极逻辑引论》一文概述了由Girard分别于1986和2001所创建的线性逻辑和态极逻辑.线性逻辑和态极逻辑汲取于计算机科学并反之应用于其中,从根本上对数理逻辑进行了彻底的审视.全文分为两部分.本文是文章的第一部分,致力于线性逻辑的联结词、证明规则、可判定性性质和模型.文章的第二部分将研究证明网并简要介绍态极逻辑.证明网是证明的图式表示,是线性逻辑的主要创新之一.     

Irreducible and transitive locally-nilpotent by abelian finitary groups

We show that a locally-nilpotent by abelian group that is either a transitive finitary permutation group on an infinite set or an irreducible finitary skew linear group of infinite dimension, is a p-group for some suitably chosen prime p.     

Lawlessness and rank restrictions in certain finitary groups

We give two applications of the recent classification of locally finite simple finitary skew linear groups. We show that certain irreducible finitary skew linear groups of infinite dimension generate the variety of all groups and have infinite Prüfer rank.

     

Free products of finitary linear groups

In this note we show that the free product of any family of groups which are finitary linear over fields of the same characteristic , is still finitary linear over a field of characteristic .

     

线性逻辑和态极逻辑引论(Ⅱ)

本文是《线性逻辑和态极逻辑引论》一文的第二部分。文章致力于证明网(第1节)和态极逻辑(第2,3,4和5节)证明网部分尽管局限于其积线性逻辑框架,但仍不失其重要性。线性逻辑和态极逻辑均为Girard所创建,近期所发展起来的态极逻辑旨在于进一步揭示计算和逻辑的基本交互作用的本质。我们希望本文能对这一新的理论带来一些计算机科学方面的启示。