Proofs with monotone cuts

Atserias, Galesi, and Pudlák have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK (or equivalently, in Frege systems). We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut‐formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.     

On transformations of constant depth propositional proofs

This paper studies the complexity of constant depth propositional proofs in the cedent and sequent calculus. We discuss the relationships between the size of tree-like proofs, the size of dag-like proofs, and the heights of proofs. The main result is to correct a proof construction in an earlier paper about transformations from proofs with polylogarithmic height and constantly many formulas per cedent.     

Decidability and Specker sequences in intuitionistic mathematics

A bounded monotone sequence of reals without a limit is called a Specker sequence. In Russian constructive analysis, Church's Thesis permits the existence of a Specker sequence. In intuitionistic mathematics, Brouwer's Continuity Principle implies it is false that every bounded monotone sequence of real numbers has a limit. We claim that the existence of Specker sequences crucially depends on the properties of intuitionistic decidable sets. We propose a schema (which we call ED ) about intuitionistic decidability that asserts “there exists an intuitionistic enumerable set that is not intuitionistic decidable” and show that the existence of a Specker sequence is equivalent to ED . We show that ED is consistent with some certain well known axioms of intuitionistic analysis as Weak Continuity Principle, bar induction, and Kripke Schema. Thus, the assumption of the existence of a Specker sequence is conceivable in intuitionistic analysis. We will also introduce the notion of double Specker sequence and study the existence of them (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Bounded linear-time temporal logic: A proof-theoretic investigation

Propositional and first-order bounded linear-time temporal logics (BLTL and FBLTL, respectively) are introduced by restricting Gentzen type sequent calculi for linear-time temporal logics. The corresponding Robinson type resolution calculi, RC and FRC for BLTL and FBLTL respectively are obtained. To prove the equivalence between FRC and FBLTL, a temporal version of Herbrand theorem is used. The completeness theorems for BLTL and FBLTL are proved for simple semantics with both a bounded time domain and some bounded valuation conditions on temporal operators. The cut-elimination theorems for BLTL and FBLTL are also proved using some theorems for embedding BLTL and FBLTL into propositional (first-order, respectively) classical logic. Although FBLTL is undecidable, its monadic fragment is shown to be decidable.     

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.     

Prefixed tableaus and nested sequents

Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational variants of each other, roughly in the same way that Gentzen sequent calculi and tableaus are notational variants. This immediately gives rise to new modal nested sequent systems which may be of independent interest. We discuss some of these, including those for some justification logics that include standard modal operators.     

Consistency proof via pointwise induction

We show that the consistency of the first order arithmetic follows from the pointwise induction up to the Howard ordinal. Our proof differs from U. Schmerl [Sc]: We do not need Girard's Hierarchy Comparison Theorem. A modification on the ordinal assignment to proofs by Gentzen and Takeuti [T] is made so that one step reduction on proofs exactly corresponds to the stepping down in ordinals. Also a generalization to theories of finitely iterated inductive definitions is proved. Received May 30, 1996     

Categorical abstract algebraic logic: Gentzen π ‐institutions and the deduction‐detachment property

Given a π ‐institution I , a hierarchy of π ‐institutions I ^{(n )} is constructed, for n ≥ 1. We call I ^{(n )} the n‐th order counterpart of I . The second‐order counterpart of a deductive π ‐institution is a Gentzen π ‐institution, i.e. a π ‐institution associated with a structural Gentzen system in a canonical way. So, by analogy, the second order counterpart I ⁽²⁾ of I is also called the “Gentzenization” of I . In the main result of the paper, it is shown that I is strongly Gentzen , i.e. it is deductively equivalent to its Gentzenization via a special deductive equivalence, if and only if it has the deduction‐detachment property . (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

On two fragments with negation and without implication of the logic of residuated lattices

The logic of (commutative integral bounded) residuated lattices is known under different names in the literature: monoidal logic [26], intuitionistic logic without contraction [1], H_BCK [36] (nowadays called by Ono), etc. In this paper we study the -fragment and the -fragment of the logical systems associated with residuated lattices, both from the perspective of Gentzen systems and from that of deductive systems. We stress that our notion of fragment considers the full consequence relation admitting hypotheses. It results that this notion of fragment is axiomatized by the rules of the sequent calculus for the connectives involved. We also prove that these deductive systems are non-protoalgebraic, while the Gentzen systems are algebraizable with equivalent algebraic semantics the varieties of pseudocomplemented (commutative integral bounded) semilatticed and latticed monoids, respectively. All the logical systems considered are decidable.     

Some remarks on lengths of propositional proofs

We survey the best known lower bounds on symbols and lines in Frege and extended Frege proofs. We prove that in minimum length sequent calculus proofs, no formula is generated twice or used twice on any single branch of the proof. We prove that the number of distinct subformulas in a minimum length Frege proof is linearly bounded by the number of lines. Depthd Frege proofs ofm lines can be transformed into depthd proofs ofO(m ^d+1) symbols. We show that renaming Frege proof systems are p-equivalent to extended Frege systems. Some open problems in propositional proof length and in logical flow graphs are discussed. Supported in part by NSF grant DMS-9205181     

On extreme points of bounded sets of generalized finite sequence spaces

The Linear Independence Extreme Point Theorem and Opposite Sign Theorem of semiinfinite programming provide algebraic characterizations of unbounded infinite dimensional convex polyhedral sets in terms of their extreme points. The Charnes, Kortanek, and Raike purification algorithm, which transforms any non-extreme point to an extreme point having objective function value at least as great, is based upon the constructive proofs of these two theorems. In this paper these extreme point characterizations are extended to additionally constrained, bounded convex polyhedral constraint sets of semi-infinite programming. It is shown that each of these bounded sets is spanned by a possibly infinite number of extreme points, and as before the proofs are constructive, thereby expanding the range of applicability of the purification algorithm to these cases.     

Bounded arithmetic,proof complexity and two papers of Parikh

This article surveys R. Parikh's work on feasibility, bounded arithmetic and the complexity of proofs. We discuss in depth two of Parikh's papers on these subjects and some of the subsequent progress in the areas of feasible arithmetic and lengths of proofs.     

具有N-各向异性拉普拉斯算子的超线性问题的先验界

通过改进Brezis和Merle的方法,结合Moser-Trudinger不等式,移动平面方法及比较原理,得到了方程-Q_Nu=f(u),u∈W_0~(1,N)(Ω)的正解的先验界,其中Ω是R~N中的一个有界光滑区域,非线性项f至多具有指数型增长.     

Powerset Residuated Algebras and Generalized Lambek Calculus

We prove a representation theorem for (abstract) residuated algebras: each residuated algebra is isomorphically embeddable into a powerset residuated algebra. As a consequence, we obtain a completeness theorem for the Generalized Lambek Calculus. We use a Labelled Deductive System which generalizes the one used by Buszkowski [4] and Pankrat'ev [17] in completeness theorems for the Lambek Calculus.     

Existence results for degenerate p(x)-Laplace equations with Leray-Lions type operators

We show the existence and multiplicity of solutions to degenerate p(x)-Laplace equations with Leray-Lions type operators using direct methods and critical point theories in Calculus of Variations and prove the uniqueness and nonnegativeness of solutions when the principal operator is monotone and the nonlinearity is nonincreasing. Our operator is of the most general form containing all previous ones and we also weaken assumptions on the operator and the nonlinearity to get the above results. Moreover, we do not impose the restricted condition on p(x) and the uniform monotonicity of the operator to show the existence of three distinct solutions.     

Proof complexity of propositional default logic

Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen??s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti??s enhanced calculus for skeptical default reasoning.     

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.     

带极大单调图的半线性抛物型方程的零能控性(英文)

本文讨论非线性项带一个极大单调图的半线性抛物型方程系统的零能控性.文中利用Kakutani不动点定理和线性抛物型方程的能控性得到该系统是零能控的,如果控制作用在内部区域上.由此,还得到该系统是零能控的,如果控制施加在一部分边界上.     

Tree-depth and vertex-minors

In a recent paper Kwon and Oum (2014), Kwon and Oum claim that every graph of bounded rank-width is a pivot-minor of a graph of bounded tree-width (while the converse has been known true already before). We study the analogous questions for “depth” parameters of graphs, namely for the tree-depth and related new shrub-depth. We show how a suitable adaptation of known results implies that shrub-depth is monotone under taking vertex-minors, and we prove that every graph class of bounded shrub-depth can be obtained via vertex-minors of graphs of bounded tree-depth. While we exhibit an example that pivot-minors are generally not sufficient (unlike Kwon and Oum (2014)) in the latter statement, we then prove that the bipartite graphs in every class of bounded shrub-depth can be obtained as pivot-minors of graphs of bounded tree-depth.