Inferentialism and Relevance

This paper provides an inferentialist motivation for a logic belonging in the connexive family, by borrowing elements from the bilateralist interpretation for Classical Logic without the Cut rule, proposed by David Ripley. The paper focuses on the relation between inferentialism and relevance, through the exploration of what we call relevant assertion and denial, showing that a connexive system emerges as a symptom of this interesting link. With the present attempt we hope to broaden the available interpretations for connexive logics, showing they can be rightfully motivated in terms of certain relevantist constraints imposed on assertion and denial.

The consistency of 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.

On Proof Complexities Relations in Some Systems of Propositional Calculus

The number of linear proofs steps for some sets of formulas is compared in the folowing systems of propositional calculus: PK – seguent system with cut rule, PK— - the same system without cut rule, SPK – the same system with substitution rule, QPK – the same system with quantifier rules. The number of steps of tree-like proofs in the same systems for some considered set of formulas is compared from Alessandra Carbone in [1] and some distinctive property of the system QPK is revealed: QPK has an exponential speed-up over the systems SPK and PK, which, in their turn, have an exponential speed-up over the system PK—. This result drew the heavy interest for the study of the system QPK. In this work for linear proofs steps in the same systems the other relations are received: it is showed that the system QPK has no preference over the system SPK, it is showed also that for the considered formula sets the system PK has no preference over the system PK—, which, in its turn, has no preference over the monotone system PMon. It is proved also, that the same results are reliable for some other sets of formulas and for other systems as well.

ON NON-MONOTONOUS PROPERTIES OF SOME CLASSICAL AND NONCLASSICAL PROPOSITIONAL PROOF SYSTEMS

We investigate the relations between the proof lines of non-minimal tautologies and its minimal tautologies for the Frege systems, the sequent systems with cut rule and the systems of natural deductions of classical and nonclassical logics. We show that for these systems there are sequences of tautologies ψn, every one of which has unique minimal tautologies φn such that for each n the minimal proof lines of φn are an order more than the minimal proof lines of ψn.

A cut-free labelled sequent calculus for dynamic epistemic logic

Dynamic epistemic logic is a logic that is aimed at formally expressing how a person’s knowledge changes. We provide a cut-free labelled sequent calculus ($\textbf{GDEL}$) on the background of existing studies of Hilbert-style axiomatization $\textbf{HDEL}$ of dynamic epistemic logic and labelled calculi for public announcement logic. We first show that the $cut$ rule is admissible in $\textbf{GDEL}$ and show that $\textbf{GDEL}$ is sound and complete for Kripke semantics. Moreover, we show that the basis of $\textbf{GDEL}$ is extended from modal logic K to other familiar modal logics including S5 with keeping the admissibility of cut, soundness and completeness.

A Modified Subformula Property for the Modal Logic S4.2

The modal logic S4.2 is S4 with the additional axiom ◊□A ⊃ □◊A. In this article, the sequent calculus GS4.2 for this logic is presented, and by imposing an appropriate restriction on the application of the cut-rule, it is shown that, every GS4.2-provable sequent S has a GS4.2-proof such that every formula occurring in it is either a subformula of some formula in S, or the formula □¬□B or ¬□B, where □B occurs in the scope of some occurrence of □ in some formula of S. These are just the K5-subformulas of some formula in S which were introduced by us to show the modied subformula property for the modal logics K5 and K5D (Bull Sect Logic 30(2): 115–122, 2001). Some corollaries including the interpolation property for S4.2 follow from this. By slightly modifying the proof, the finite model property also follows.

A non-transitive relevant implication corresponding to classical logic consequence

In this paper we first develop a logic independent account of relevant implication. We propose a stipulative denition of what it means for a multiset of premises to relevantly L-imply a multiset of conclusions, where L is a Tarskian consequence relation: the premises relevantly imply the conclusions iff there is an abstraction of the pair <premises, conclusions> such that the abstracted premises L-imply the abstracted conclusions and none of the abstracted premises or the abstracted conclusions can be omitted while still maintaining valid L-consequence. Subsequently we apply this denition to the classical logic (CL) consequence relation to obtain NTR-consequence, i.e. the relevant CL-consequence relation in our sense, and develop a sequent calculus that is sound and complete with regard to relevant CL-consequence. We present a sound and complete sequent calculus for NTR. In a next step we add rules for an object language relevant implication to thesequent calculus. The object language implication reflects exactly the NTR-consequence relation. One can see the resulting logic NTR-> as a relevant logic in the traditional sense of the word. By means of a translation to the relevant logic R, we show that the presented logic NTR is very close to relevance logics in the Anderson-Belnap-Dunn-Routley-Meyer tradition. However, unlike usual relevant logics, NTR is decidable for the full language, Disjunctive Syllogism (A and ~AvB relevantly imply B) and Adjunction (A and B relevantly imply A&B) are valid, and neither Modus Ponens nor the Cut rule are admissible.

Non-Analytic Tableaux for Chellas's Conditional Logic CK and Lewis's Logic of Counterfactuals VC

Priest has provided a simple tableau calculus for Chellas's conditional logic Ck. We provide rules which, when added to Priest's system, result in tableau calculi for Chellas's CK and Lewis's VC. Completeness of these tableaux, however, relies on the cut rule.

Cuts for circular proofs

One of the authors introduced in [1] a calculus ofcircular proofs for studying the computability arising from thefollowing categorical operations: finite products and coproducts,initial algebras, final coalgebras. The calculus of[1] is cut-free; yet, even if sound and complete forprovability, it lacks an important property for the semantics ofproofs, namely fullness w.r.t. the class of natural categorical modelscalled μ-bicomplete category in [2].We fix, with this work, this problem by adding the cut rule to thecalculus. To this goal, we need to modifying the syntacticalconstraints on the cycles of proofs so to ensure soundness of thecalculus and at same time local termination of cut-elimination. Theenhanced proof system fully represents arrows of the intended model, afree μ-bicomplete category. We also describe a cut-eliminationprocedure as a model of computation arising from the above mentionedcategorical operations. The procedure constructs a cut-freeproof-tree with infinite branches out of a finite circular proof withcuts.[1] Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors, FoSSaCS, volume 2303 of Lecture Notes in Computer Science, pages 357–371. Springer, 2002.[2] Luigi Santocanale. μ-bicomplete categories and parity games. Theoretical Informatics and Applications, 36:195–227, September 2002.

Proof Theory of the Cut Rule

This chapter describes the categorical proof theory of the cut rule, a very basic component of any sequent-style presentation of a logic, assuming a minimum of structural rules and connectives, in fact, starting with none. It is shown how logical features can be added to this basic logic in a modular fashion, at each stage showing the appropriate corresponding categorical semantics of the proof theory, starting with multicategories, and moving to linearly distributive categories and *-autonomous categories. A key tool is the use of graphical representations of proofs (“proof circuits”) to represent formal derivations in these logics. This is a powerful symbolism, which on the one hand is a formal mathematical language, but crucially, at the same time, has an intuitive graphical representation.