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.     

Classical proof forestry

Classical proof forests are a proof formalism for first-order classical logic based on Herbrand’s Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of first-order and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or ‘bureaucracy’.This paper presents classical proof forests as a graphical proof formalism and investigates the possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given.Cut-elimination, in the form of a weak normalisation theorem, is obtained using a modified version of the rewrite relation inspired by the game-theoretic interpretation of the forests. It is conjectured that the modified reduction relation is, in fact, strongly normalising.     

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     

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.     

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.      

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.     

A minimal classical sequent calculus free of structural rules

Gentzen’s classical sequent calculus has explicit structural rules for contraction and weakening. They can be absorbed (in a right-sided formulation) by replacing the axiom P,¬P by Γ,P,¬P for any context Γ, and replacing the original disjunction rule with Γ,A,B implies Γ,A∨B.This paper presents a classical sequent calculus which is also free of contraction and weakening, but more symmetrically: both contraction and weakening are absorbed into conjunction, leaving the axiom rule intact. It uses a blended conjunction rule, combining the standard context-sharing and context-splitting rules: Γ,Δ,A and Γ,Σ,B implies Γ,Δ,Σ,A∧B. We refer to this system as minimal sequent calculus.We prove a minimality theorem for the propositional fragment : any propositional sequent calculus S (within a standard class of right-sided calculi) is complete if and only ifS contains (that is, each rule of is derivable in S). Thus one can view as a minimal complete core of Gentzen’s .     

Interpolation property for bicartesian closed categories

Summary We show that proofs in the intuitionistic propositional logic factor through interpolants-in this way we prove a stronger interpolation property than the usual one which gives only the existence of interpolants.Translating that to categorical terms, we show that Pushouts (bipushouts) of bicartesian closed categories have the interpolation property (Theorem 3.2).     

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.     

The bounded proof property via step algebras and step frames

The paper introduces semantic and algorithmic methods for establishing a variant of the analytic subformula property (called ‘the bounded proof property’, bpp) for modal propositional logics. The bpp is much weaker property than full cut-elimination, but it is nevertheless sufficient for establishing decidability results. Our methodology originated from tools and techniques developed on one side within the algebraic/coalgebraic literature dealing with free algebra constructions and on the other side from classical correspondence theory in modal logic. As such, our approach is orthogonal to recent literature based on proof-theoretic methods and, in a way, complements it.     

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.     

Proof internalization in generalized Frege systems for classical logic

We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.     

Cut elimination and strong separation for substructural logics: An algebraic approach

We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on (associative) substructural logics over the full Lambek Calculus (see, for example, Ono (2003) [34], Galatos and Ono (2006) [18], Galatos et al. (2007) [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show that the logic associated with and is algebraizable, with the variety of residuated lattice-ordered groupoids with unit serving as its equivalent algebraic semantics.Overcoming technical complications arising from the lack of associativity, we introduce a generalized version of a logical matrix and apply the method of quasicompletions to obtain an algebra and a quasiembedding from the matrix to the algebra. By applying the general result to specific cases, we obtain important logical and algebraic properties, including the cut elimination of and various extensions, the strong separation of , and the finite generation of the variety of residuated lattice-ordered groupoids with unit.     

Ordered groups with a conucleus

Our work proposes a new paradigm for the study of various classes of cancellative residuated lattices by viewing these structures as lattice-ordered groups with a suitable operator (a conucleus). One consequence of our approach is the categorical equivalence between the variety of cancellative commutative residuated lattices and the category of abelian lattice-ordered groups endowed with a conucleus whose image generates the underlying group of the lattice-ordered group. In addition, we extend our methods to obtain a categorical equivalence between -algebras and product algebras with a conucleus. Among the other results of the paper, we single out the introduction of a categorical framework for making precise the view that some of the most interesting algebras arising in algebraic logic are related to lattice-ordered groups. More specifically, we show that these algebras are subobjects and quotients of lattice-ordered groups in a “quantale like” category of algebras.     

Two applications of Boolean models

Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. These models are a slight variation of ordinary first-order models, where truth values are now regular ideals of a given Boolean algebra. Two examples are presented: a simple conservativity result and Herbrand's theorem. Received December 5, 1995     

Normal deduction in the intuitionistic linear logic

We describe a natural deduction system NDIL for the second order intuitionistic linear logic which admits normalization and has a subformula property. NDIL is an extension of the system for !-free multiplicative linear logic constructed by the author and elaborated by A. Babaev. Main new feature here is the treatment of the modality !. It uses a device inspired by D. Prawitz' treatment of S4 combined with a construction introduced by the author to avoid cut-like constructions used in -elimination and global restrictions employed by Prawitz. Normal form for natural deduction is obtained by Prawitz translation of cut-free sequent derivations. Received: March 29, 1996     

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     

Weak effect algebras

Weak effect algebras are based on a commutative, associative and cancellative partial addition; they are moreover endowed with a partial order which is compatible with the addition, but in general not determined by it. Every BL-algebra, i.e. the Lindenbaum algebra of a theory of Basic Logic, gives rise to a weak effect algebra; to this end, the monoidal operation is restricted to a partial cancellative operation. We examine in this paper BL-effect algebras, a subclass of the weak effect algebras which properly contains all weak effect algebras arising from BL-algebras. We describe the structure of BL-effect algebras in detail. We thus generalise the well-known structure theory of BL-algebras. Namely, we show that BL-effect algebras are subdirect products of linearly ordered ones and that linearly ordered BL-effect algebras are ordinal sums of generalised effect algebras. The latter are representable by means of linearly ordered groups. This research was partially supported by the German Science Foundation (DFG) as part of the Collaborative Research Center “Computational Intelligence” (SFB 531).     

Kripke models for classical logic

We introduce a notion of the Kripke model for classical logic for which we constructively prove the soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.     

Algebraic proof theory for substructural logics: Cut-elimination and completions

We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.We introduce the substructural hierarchy — a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that a stronger form of cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N₂ in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent calculus rules, are also provided.Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.