Translations from natural deduction to sequent calculus

Gentzen's “Untersuchungen” [1] gave a translation from natural deduction to sequent calculus with the property that normal derivations may translate into derivations with cuts. Prawitz in [8] gave a translation that instead produced cut‐free derivations. It is shown that by writing all elimination rules in the manner of disjunction elimination, with an arbitrary consequence, an isomorphic translation between normal derivations and cut‐free derivations is achieved. The standard elimination rules do not permit a full normal form, which explains the cuts in Gentzen's translation. Likewise, it is shown that Prawitz' translation contains an implicit process of cut elimination.     

New sequent calculi for Visser's Formal Propositional Logic

Two cut‐free sequent calculi which are conservative extensions of Visser's Formal Propositional Logic (FPL) are introduced. These satisfy a kind of subformula property and by this property the interpolation theorem for FPL are proved. These are analogies to Aghaei‐Ardeshir's calculi for Visser's Basic Propositional Logic.     

A spatial modal logic with a location interpretation

A spatial modal logic (SML) is introduced as an extension of the modal logic S4 with the addition of certain spatial operators. A sound and complete Kripke semantics with a natural space (or location) interpretation is obtained for SML. The finite model property with respect to the semantics for SML and the cut‐elimination theorem for a modified subsystem of SML are also presented. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Finite Models of Some Substructural Logics

We give a proof of the finite model property (fmp) of some fragments of commutative and noncommutative linear logic: the Lambek calculus, BCI, BCK and their enrichments, MALL and Cyclic MALL. We essentially simplify the method used in [4] for proving fmp of BCI and the Lambek ca culus and in [5] for proving fmp of MALL. Our construction of finite models also differs from that used in Lafont [8] in his proof of fmp of MALL (we do not use cut elimination).     

Synthesized substructural logics

A mechanism for combining any two substructural logics (e.g. linear and intuitionistic logics) is studied from a proof‐theoretic point of view. The main results presented are cut‐elimination and simulation results for these combined logics called synthesized substructural logics. (© 2007 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Dual‐Context Sequent Calculus and Strict Implication

We introduce a dual‐context style sequent calculus which is complete with respectto Kripke semantics where implication is interpreted as strict implication in the modal logic K. The cut‐elimination theorem for this calculus is proved by a variant of Gentzen's method.     

Generating facets for the cut polytope of a graph by triangular elimination

The cut polytope of a graph arises in many fields. Although much is known about facets of the cut polytope of the complete graph, very little is known for general graphs. The study of Bell inequalities in quantum information science requires knowledge of the facets of the cut polytope of the complete bipartite graph or, more generally, the complete k-partite graph. Lifting is a central tool to prove certain inequalities are facet inducing for the cut polytope. In this paper we introduce a lifting operation, named triangular elimination, applicable to the cut polytope of a wide range of graphs. Triangular elimination is a specific combination of zero-lifting and Fourier–Motzkin elimination using the triangle inequality. We prove sufficient conditions for the triangular elimination of facet inducing inequalities to be facet inducing. The proof is based on a variation of the lifting lemma adapted to general graphs. The result can be used to derive facet inducing inequalities of the cut polytope of various graphs from those of the complete graph. We also investigate the symmetry of facet inducing inequalities of the cut polytope of the complete bipartite graph derived by triangular elimination.      

Monotone Proofs of the Pigeon Hole Principle

We study the complexity of proving the Pigeon Hole Principle (PHP)in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We prove a size‐depth trade‐off upper bound for monotone proofs of the standard encoding of the PHP as a monotone sequent. At one extreme of the trade‐off we get quasipolynomia ‐size monotone proofs, and at the other extreme we get subexponential‐size bounded‐depth monotone proofs. This result is a consequence of deriving the basic properties of certain monotone formulas computing the Boolean threshold functions. We also consider the monotone sequent expressing the Clique‐Coclique Principle (CLIQUE) defined by Bonet, Pitassi and Raz [9]. We show that monotone proofs for this sequent can be easily reduced to monotone proofs of the one‐to‐one and onto PHP, and so CLIQUE also has quasipolynomia ‐size monotone proofs. As a consequence of our results, Resolution, Cutting Planes with polynomially bounded coefficients, and Bounded‐Depth Frege are exponentially separated from the monotone Gentzen Calculus. Finally, a simple simulation argument implies that these results extend to the Intuitionistic Gentzen Calculus. Our results partially answer some questions left open by P. Pudlák.     

Functorial bounds for cut elimination inL βω . I

The purpose of this article is to establish the relation between the new concepts of ₂ ¹ -Logic, introduced by Girard [G4] and the traditional approach of cut elimination, in particular with respect to the bounds obtained: The bounds for the cut elimination theorem are given explicitly in the form of dilators. In particular, the bound obtained in the final theorem is the bilatorV, which is a functorial version of the Veblen hierarchy employed in the classical case.     

Cut‐elimination Theorems for Some Infinitary Modal Logics

In this article, a cut‐free system TLM_ω1 for infinitary propositional modal logic is proposed which is complete with respect to the class of all Kripke frames.The system TLM_ω1 is a kind of Gentzen style sequent calculus, but a sequent of TLM_ω1 is defined as a finite tree of sequents in a standard sense. We prove the cut‐elimination theorem for TLM_ω1 via its Kripke completeness.     

Space of valuations

The general framework of this paper is a reformulation of Hilbert’s program using the theory of locales, also known as formal or point-free topology [P.T. Johnstone, Stone Spaces, in: Cambridge Studies in Advanced Mathematics, vol. 3, 1982; Th. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic 124 (1–3) (2003) 71–106; G. Sambin, Intuitionistic formal spaces–a first communication, in: D. Skordev (Ed.), Mathematical Logic and its Applications, Plenum, New York, 1987, pp. 187–204]. Formal topology presents a topological space, not as a set of points, but as a logical theory which describes the lattice of open sets. The application to Hilbert’s program is then the following. Hilbert’s ideal objects are represented by points of such a formal space. There are general methods to “eliminate” the use of points, close to the notion of forcing and to the “elimination of choice sequences” in intuitionist mathematics, which correspond to Hilbert’s required elimination of ideal objects. This paper illustrates further this general program on the notion of valuations. They were introduced by Dedekind and Weber [R. Dedekind, H. Weber, Theorie des algebraischen Funktionen einer Veränderlichen, J. de Crelle t. XCII (1882) 181–290] to give a rigorous presentation of Riemann surfaces. It can be argued that it is one of the first example in mathematics of point-free representation of spaces [N. Bourbaki, Eléments de Mathématique. Algèbre commutative, Hermann, Paris, 1965, Chapitre 7]. It is thus of historical and conceptual interest to be able to represent this notion in formal topology.     

A finitely convergent algorithm for bilinear programming problems using polar cuts and disjunctive face cuts

A finite algorithm is presented in this study for solving Bilinear programs. This is accomplished by developing a suitable cutting plane which deletes at least a face of a polyhedral set. At an extreme point, a polar cut using negative edge extensions is used. At other points, disjunctive cuts are adopted. Computational experience on test problems in the literature is provided.This paper is based upon work supported by the National Science Foundation under Grant No. ENG-77-23683.     

Classical linear logics with mix separation principle

Variants of classical linear logics are presented based on the modal version of new structural rule !?mingle instead of the known rules !weakening and ?weakening. The cut‐elimination theorems, the completeness theorems (with respect to Girard's phase models) and a characteristic property named the mix separation principle are proved for these logics.     

High‐girth cubic graphs are homomorphic to the Clebsch graph

We give a (computer assisted) proof that the edges of every graph with maximum degree 3 and girth at least 17 may be 5‐colored (possibly improperly) so that the complement of each color class is bipartite. Equivalently, every such graph admits a homomorphism to the Clebsch graph (Fig. 1 ). Hopkins and Staton [J Graph Theory 6(2) (1982), 115–121] and Bondy and Locke [J Graph Theory 10(4) (1986), 477–504] proved that every (sub)cubic graph of girth at least 4 has an edge‐cut containing at least of the edges. The existence of such an edge‐cut follows immediately from the existence of a 5‐edge‐coloring as described above; so our theorem may be viewed as a coloring extension of their result (under a stronger girth assumption). Every graph which has a homomorphism to a cycle of length five has an above‐described 5‐edge‐coloring; hence our theorem may also be viewed as a weak version of Ne?et?il's Pentagon Problem (which asks whether every cubic graph of sufficiently high girth is homomorphic to C₅). Copyright © 2011 Wiley Periodicals, Inc. J Graph Theory 66: 241—259, 2011     

Many-Place Sequent Calculi for Finitely-Valued Logics

In this paper, we study multiplicative extensions of propositional many-place sequent calculi for finitely-valued logics arising from those introduced in Sect. 5 of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, 2004) through their translation by means of singularity determinants for logics and restriction of the original many-place sequent language. Our generalized approach, first of all, covers, on a uniform formal basis, both the one developed in Sect. 5 of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, 2004) for singular finitely-valued logics (when singularity determinants consist of a variable alone) and conventional Gentzen-style (i.e., two-place sequent) calculi suggested in Pynko (Bull Sect Logic 33(1):23–32, 2004) for finitely-valued logics with equality determinant. In addition, it provides a universal method of constructing Tait-style (i.e., one-place sequent) calculi for finitely-valued logics with singularity determinant (in particular, for Łukasiewicz finitely-valued logics) that fits the well-known Tait calculus (Lecture Notes in Mathematics, Springer, Berlin, 1968) for the classical logic. We properly extend main results of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, 2004) and explore calculi under consideration within the framework of Sect. 7 of Pynko (Arch Math Logic 45:267–305, 2006), generalizing the results obtained in Sect. 7.5 of Pynko (Arch Math Logic 45:267–305 2006) for two-place sequent calculi associated with finitely-valued logics with equality determinant according to Pynko (Bull Sect Logic 33(1):23–32, 2004). We also exemplify our universal elaboration by applying it to some denumerable families of well-known finitely-valued logics.     

Duplication of directed graphs and exponential blow up of proofs

We develop a combinatorial model to study the evolution of graphs underlying proofs during the process of cut elimination. Proofs are two-dimensional objects and differences in the behavior of their cut elimination can often be accounted for by differences in their two-dimensional structure. Our purpose is to determine geometrical conditions on the graphs of proofs to explain the expansion of the size of proofs after cut elimination. We will be concerned with exponential expansion and we give upper and lower bounds which depend on the geometry of the graphs. The lower bound is computed passing through the notion of universal covering for directed graphs.

In this paper we present ground material for the study of cut elimination and structure of proofs in purely combinatorial terms. We develop a theory of duplication for directed graphs and derive results on graphs of proofs as corollaries.     

CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT

The aim of this paper is to extend the semantic analysis of tense logic in Rescher/Urquhart [3] to propositional dynamic logic without*. For this we develop a nested sequential calculus whose axioms and rules directly reflect the steps in the semantic analysis. It is shown that this calculus, with the cut rule omitted, is complete with respect to the standard semantics. It follows that cut elimination does hold for this nested sequential calculus. MSC: 03B45.     

Full Models for Positive Modal Logic

The positive fragment of the local modal consequence relation defined by the class of all Kripke frames is studied in the context of Abstract Algebraic Logic. It is shown that this fragment is non‐protoalgebraic and that its class of canonically associated algebras according to the criteria set up in [7] is the class of positive modal algebras. Moreover its full models are characterized as the models of the Gentzen calculus introduced in [3].     

On some logical points of fuzzy conditional decision making

The paper deals with some properties of PL (Probability Logic) and FL (Fuzzy Logic). FL is derived from PL by means of choosing the connectives such that the logical system created is truth-functional. From many alternatives the usual connectives of FL emerged. As is known, PL is not truth-functional. Conditionality is considered by means of implication and using a fuzzy counterpart of conditional probability. In that way some basic tools are created for Bayesian-like decision making in a fuzzy environment. The analysis shows that the implication and the conditional probability-like counterpart are not necessarily the same thing. A labelling system is introduced in fuzzy-valued FL such that a finite set of non-negative integers forms the set of truth-values, which actually are fuzzy sets of the unit interval [0,1]. In this way new quantitative expressions are obtained for each qualitative linguistic variable. In doing so, the system preserves fuzziness. Some general rules of inference are also considered.     

A physical space approach to wave equation bilinear estimates

Bilinear estimates for the wave equation in Minkowski space are normally proven using the Fourier transform and Plancherel’s theorem. However, such methods are difficult to carry over to non-flat situations (such as wave equations with rough metrics or connections with non-zero curvature). In this note, we describe an alternative physical space approach which relies on vector fields, energy estimates as well as tube localization, splitting into coarse and fine scales, and induction on scales (in the spirit of Wolff [29], [30]).