Sequent calculus proof theory of intuitionistic apartness and order relations

Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity results for the theories of constructive order over the usual theories of order. Received: 4 December 1997     

The polynomial bounds of proof complexity in Frege systems

The concept of a determinative set of variables for a propositional formula was introduced by one of the authors, which made it possible to distinguish the set of hard-determinable formulas. The proof complexity of a formula of this sort has exponential lower bounds in some proof systems of classical propositional calculus (cut-free sequent system, resolution system, analytic tableaux, cutting planes, and bounded Frege systems). In this paper we prove that the property of hard-determinability is insufficient for obtaining a superpolynomial lower bound of proof lines (sizes) in Frege systems: an example of a sequence of hard-determinable formulas is given whose proof complexities are polynomially bounded in every Frege system.     

Gentzen’s consistency proof without heightlines

This paper gives a Gentzen-style proof of the consistency of Heyting arithmetic in an intuitionistic sequent calculus with explicit rules of weakening, contraction and cut. The reductions of the proof, which transform derivations of a contradiction into less complex derivations, are based on a method for direct cut-elimination without the use of multicut. This method treats contractions by tracing up from contracted cut formulas to the places in the derivation where each occurrence was first introduced. Thereby, Gentzen’s heightline argument, which introduces additional cuts on contracted compound cut formulas, is avoided. To show termination of the reduction procedure an ordinal assignment based on techniques of Howard for Gödel’s T is used.     

A focused approach to combining logics

We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut-elimination holds in such fragments. From cut-elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical-linear hybrid logics.     

Some properties and an application of multivariate exponential polynomials

In the paper, the authors introduce a notion “multivariate exponential polynomials” which generalize exponential numbers and polynomials, establish explicit formulas, inversion formulas, and recurrence relations for multivariate exponential polynomials in terms of the Stirling numbers of the first and second kinds with the help of the Faà di Bruno formula, two identities for the Bell polynomials of the second kind, and the inversion theorem for the Stirling numbers of the first and second kinds, construct some determinantal inequalities and product inequalities for multivariate exponential polynomials with the aid of some properties of completely monotonic functions and other known results, derive the logarithmic convexity and logarithmic concavity for multivariate exponential polynomials, and finally find an application of multivariate exponential polynomials to white noise distribution theory by confirming that multivariate exponential polynomials satisfy conditions for sequences required in white noise distribution theory.     

Plethystic Exponential Polynomials and Plethystic Stirling Numbers

In this article we introduce a plethystic generalization of the exponential polynomials and their umbral inverses. We obtain recursive formulas for both families of polynomials, and use them to get recursions for the plethystic Stirling numbers of the first and second kind and for the plethystic Bell numbers. Finally, we apply Bergeron's S-species to obtain a Dobinsky formula for the plethystic exponential polynomials and a close formula for the plethystic Stirling numbers of the second kind.     

Distributive-Lattice Semantics of Sequent Calculi with Structural Rules

The goal of the paper is to develop a universal semantic approach to derivable rules of propositional multiple-conclusion sequent calculi with structural rules, which explicitly involve not only atomic formulas, treated as metavariables for formulas, but also formula set variables (viz., metavariables for finite sets of formulas), upon the basis of the conception of model introduced in (Fuzzy Sets Syst 121(3):27–37, 2001). One of the main results of the paper is that any regular sequent calculus with structural rules has such class of sequent models (called its semantics) that a rule is derivable in the calculus iff it is sound with respect to each model of the semantics. We then show how semantics of admissible rules of such calculi can be found with using a method of free models. Next, our universal approach is applied to sequent calculi for many-valued logics with equality determinant. Finally, we exemplify this application by studying sequent calculi for some of such logics.      

Deep sequent systems for modal logic

We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen’s sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, weakening and contraction are admissible. All systems admit a straightforward terminating proof search procedure as well as a syntactic cut elimination procedure.      

A constructive semantics for non‐deducibility

This paper provides a constructive topological semantics for non‐deducibility of a first order intuitionistic formula. Formal topology theory, in particular the recently introduced notion of a binary positivity predicate, and co‐induction are two needful tools. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

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.     

Proof analysis in intermediate logics

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the G?del–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the explanation of the rules.     

Three ways of recognizing inessential formulas in sequents

The first method is based on the familiar method of lowering thinnings downwards and is a further development of the lemmas on weeding of [1]. The second method is based on the use of sufficiently wide classes of sequents, for which derivability in the intuitionistic predicate calculus coincides with derivability in the classical predicate calculus and the familiar property of disjunction is true. By this method one can get, e.g., a syntactic proof of the following assertion. If the positive formula A is derivable in the theory of groups under additional assumptions of the form then A is also derivable in the theory of groups without these assumptions. As the third method there is proposed a syntactically formulated test for the conservativeness of extensions of intuitionistic axiomatic theories. With the help of this test one can get, for example, a syntactic proof of the hereditary undecidability of the intuitionistic theory of equality, with additional axioms which are the formula, all formulas of the form and all negations of formulas derivable in the classical predicate calculus.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 88, pp. 163–175, 1979.     

命题逻辑公式的压缩表示及其相应的形式系统

提出一种将命题逻辑公式压缩表示的方法--公式的压缩图,给出相应的形式系统,并证明该系统的证明效率比传统相继式演算系统Gentzen\{cut}有指数级的提高,从而为命题逻辑提供了一种新的有效的推理系统.     

Cut-free formulations for a quantified logic of here and there

A predicate extension SQHT⁼ of the logic of here-and-there was introduced by V. Lifschitz, D. Pearce, and A. Valverde to characterize strong equivalence of logic programs with variables and equality with respect to stable models. The semantics for this logic is determined by intuitionistic Kripke models with two worlds (here and there) with constant individual domain and decidable equality. Our sequent formulation has special rules for implication and for pushing negation inside formulas. The soundness proof allows us to establish that SQHT⁼ is a conservative extension of the logic of weak excluded middle with respect to sequents without positive occurrences of implication. The completeness proof uses a non-closed branch of a proof search tree. The interplay between rules for pushing negation inside and truth in the “there” (non-root) world of the resulting Kripke model can be of independent interest. We prove that existence is definable in terms of remaining connectives.     

Order-enriched categorical models of the classical sequent calculus

It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. Starting from a convenient formulation of the well-known categorical semantics of linear classical sequent proofs, we give models of weakening and contraction that do not collapse. Cut-reduction is interpreted by a partial order between morphisms. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination. We show soundness and completeness via initial models built from proof nets, and describe models built from sets and relations.     

Uniform interpolation and the existence of sequent calculi

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus $\mathsf{G4ip}$ for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of $\mathsf{K}$ and $\mathsf{KD}$ (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.     

Natural deduction with general elimination rules

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates. Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. Received: 1 December 1998 / Revised version: 30 June 2000 / Published online: 18 July 2001     

A proof of Markov's theorem for polynomials on Banach spaces

Our object is to present an independent proof of the extension of V.A. Markov's theorem to Gâteaux derivatives of arbitrary order for continuous polynomials on any real normed linear space. The statement of this theorem differs little from the classical case for the real line except that absolute values are replaced by norms. Our proof depends only on elementary computations and explicit formulas and gives a new proof of the classical theorem as a special case. Our approach makes no use of the classical polynomial inequalities usually associated with Markov's theorem. Instead, the essential ingredients are a Lagrange interpolation formula for the Chebyshev nodes and a Christoffel-Darboux identity for the corresponding bivariate Lagrange polynomials. We use these tools to extend a single variable inequality of Rogosinski to the case of two real variables. The general Markov theorem is an easy consequence of this.     

Labeled sequent calculus for justification logics

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for $\mathsf{S4LPN}$ based on Artemov–Fitting models.