Cut Elimination in the Presence of Axioms

1998 ◽  
Vol 4 (4) ◽  
pp. 418-435 ◽  
Author(s):  
Sara Negri ◽  
Jan von Plato
Keyword(s):  
Structural Analysis ◽  
Wide Class ◽  
Predicate Logic ◽  
Free Variable ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Pure Logic ◽  
Suitable Form

AbstractA way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate logic with equality in which also cuts on the equality axioms are eliminated.

Frame definability, canonicity and cut elimination in common sense modal predicate logics

2020 ◽  
Author(s):  
Takahiro Sawasaki ◽  
Katsuhiko Sano
Keyword(s):  
Common Sense ◽  
Predicate Logic ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Axiom Schema ◽  
Modal Predicate Logics ◽  
Modal Predicate Logic

Abstract The paper presents semantically complete Hilbert-style systems for some variants of common sense modal predicate logic proposed by van Benthem and further developed by Seligman. The paper also investigates frame definability in the logics and shows what axiom schema is canonical in the logics. In addition to these semantic investigations on the logics, the paper provides the sequent calculi for some of the logics which enjoy cut elimination theorem.

UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS

2014 ◽  
Vol 7 (3) ◽  
pp. 455-483 ◽  
Author(s):  
MAJID ALIZADEH ◽  
FARZANEH DERAKHSHAN ◽  
HIROAKIRA ONO
Keyword(s):  
Propositional Logic ◽  
Predicate Logic ◽  
Interpolation Property ◽  
Substructural Logics ◽  
Substructural Logic ◽  
Sequent Calculi ◽  
Structural Rule ◽  
Modal Propositional Logic ◽  
Uniform Interpolation ◽  
Classical Predicate

AbstractUniform interpolation property of a given logic is a stronger form of Craig’s interpolation property where both pre-interpolant and post-interpolant always exist uniformly for any provable implication in the logic. It is known that there exist logics, e.g., modal propositional logic S4, which have Craig’s interpolation property but do not have uniform interpolation property. The situation is even worse for predicate logics, as classical predicate logic does not have uniform interpolation property as pointed out by L. Henkin.In this paper, uniform interpolation property of basic substructural logics is studied by applying the proof-theoretic method introduced by A. Pitts (Pitts, 1992). It is shown that uniform interpolation property holds even for their predicate extensions, as long as they can be formalized by sequent calculi without contraction rules. For instance, uniform interpolation property of full Lambek predicate calculus, i.e., the substructural logic without any structural rule, and of both linear and affine predicate logics without exponentials are proved.

The consistency of arithmetic

2021 ◽  
pp. 268-311
Author(s):  
Paolo Mancosu ◽  
Sergio Galvan ◽  
Richard Zach
Keyword(s):  
Simple Proof ◽  
Sequent Calculus ◽  
Cut Elimination ◽  
Successor Function ◽  
Cut Rule ◽  
Original Proof ◽  
First Order ◽  
Successive Elimination ◽  
Pure Logic ◽  
Classical Arithmetic

This chapter opens the part of the book that deals with ordinal proof theory. Here the systems of interest are not purely logical ones, but rather formalized versions of mathematical theories, and in particular the first-order version of classical arithmetic built on top of the sequent calculus. Classical arithmetic goes beyond pure logic in that it contains a number of specific axioms for, among other symbols, 0 and the successor function. In particular, it contains the rule of induction, which is the essential rule characterizing the natural numbers. Proving a cut-elimination theorem for this system is hopeless, but something analogous to the cut-elimination theorem can be obtained. Indeed, one can show that every proof of a sequent containing only atomic formulas can be transformed into a proof that only applies the cut rule to atomic formulas. Such proofs, which do not make use of the induction rule and which only concern sequents consisting of atomic formulas, are called simple. It is shown that simple proofs cannot be proofs of the empty sequent, i.e., of a contradiction. The process of transforming the original proof into a simple proof is quite involved and requires the successive elimination, among other things, of “complex” cuts and applications of the rules of induction. The chapter describes in some detail how this transformation works, working through a number of illustrative examples. However, the transformation on its own does not guarantee that the process will eventually terminate in a simple proof.

Gentzen sequent calculi for some intuitionistic modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 596-623
Author(s):  
Zhe Lin ◽  
Minghui Ma
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Intuitionistic Propositional Logic ◽  
Propositional Language ◽  
Intuitionistic Modal Logics ◽  
Subformula Property ◽  
Gentzen Sequent Calculus

Abstract Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond ,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond ,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

scholarly journals The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them

2020 ◽  
Vol 20 (6) ◽  
pp. 990-1005
Author(s):  
Ekaterina Komendantskaya ◽  
Dmitry Rozplokhas ◽  
Henning Basold
Keyword(s):  
Cut Elimination ◽  
Horn Clause ◽  
Sequent Calculi ◽  
New Normal ◽  
Novel Method

AbstractIn sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen’s classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.

scholarly journals Proof theory for quantified monotone modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 478-506
Author(s):  
Sara Negri ◽  
Eugenio Orlandelli
Keyword(s):  
Proof Theory ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Completeness Proof ◽  
First Order ◽  
Constant Domains ◽  
Normal Modal Logics ◽  
Order Extension

Abstract This paper provides a proof-theoretic study of quantified non-normal modal logics (NNML). It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames. In particular, the completeness proof constructs a formal derivation for derivable sequents and a countermodel for non-derivable ones, and gives a semantic proof of the admissibility of cut.

An intensional type theory: motivation and cut-elimination

2001 ◽  
Vol 66 (1) ◽  
pp. 383-400 ◽  
Author(s):  
Paul C Gilmore
Keyword(s):  
Type Theory ◽  
Proof Theory ◽  
Predicate Logic ◽  
Order Term ◽  
Higher Order ◽  
Cut Elimination ◽  
Consistency Proof ◽  
Completeness Proof ◽  
Higher Order Term

AbstractBy the theory TT is meant the higher order predicate logic with the following recursively defined types:(1) 1 is the type of individuals and [] is the type of the truth values:(2) [τ1…..τn] is the type of the predicates with arguments of the types τ1…..τn.The theory ITT described in this paper is an intensional version of TT. The types of ITT are the same as the types of TT, but the membership of the type 1 of individuals in ITT is an extension of the membership in TT. The extension consists of allowing any higher order term, in which only variables of type 1 have a free occurrence, to be a term of type 1. This feature of ITT is motivated by a nominalist interpretation of higher order predication.In ITT both well-founded and non-well-founded recursive predicates can be defined as abstraction terms from which all the properties of the predicates can be derived without the use of non-logical axioms.The elementary syntax, semantics, and proof theory for ITT are defined. A semantic consistency proof for ITT is provided and the completeness proof of Takahashi and Prawitz for a version of TT without cut is adapted for ITT: a consequence is the redundancy of cut.

scholarly journals Rule-Generation Theorem and its Applications

2018 ◽  
Vol 47 (4) ◽  
Author(s):  
Andrzej Indrzejczak
Keyword(s):  
Case Studies ◽  
General Theorem ◽  
Rule Generation ◽  
Sequent Calculi ◽  
Generation Theorem ◽  
Pure Logic

In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some case studies for illustration.

Sign in / Sign up

Export Citation Format

Share Document