Gentzenizations of relevant logics without distribution. II

1996 ◽  
Vol 61 (2) ◽  
pp. 379-401 ◽  
Author(s):  
Ross T. Brady
Keyword(s):  
Relevant Logic ◽  
Decidability Result ◽  
Structural Rules ◽  
Relevant Logics ◽  
The One ◽  
Interpolation Result

In Part I, we produced a Gentzenization L6LBQ of the distributionless relevant logic LBQ, which contained just the one structural connective ‘:’ and no structural rules. We compared it with the corresponding “right-handed” system and then proved interpolability and decidability of LBQ. Knowledge of Part I is presupposed.In Part II of this paper, we will establish Gentzenizations, with appropriate interpolation and decidability results, for the further distributionless logics LDWQ, LTWQo, LEWQot, LRWQ, LRWKQ and LRQ, using essentially the same methods as were used for LBQ in Part I. LRWQ has been Gentzenized by Grishin [2], but the interpolation result is new and the decidability result is proved by a substantial simplification of his method. LR has been Gentzenized and shown to be decidable by Meyer in [5], by extending a method of Kripke in [3], and McRobbie has proved interpolation for it in [4], but here the Gentzenization and interpolation results are extended to quantifiers.We axiomatize these logics as follows. The primitives and formation rules are as before, except that LTWQ and LEWQ require the extra primitive ‘o’, a 2-place connective (called ‘fusion’), and LEWQ also requires ‘t’, a sentential constant.

Simple Gentzenizations for the normal formulae of contraction-less logics

1996 ◽  
Vol 61 (4) ◽  
pp. 1321-1346
Author(s):  
Ross T. Brady
Keyword(s):  
Relevant Logic ◽  
Conservative Extension ◽  
Structural Rules ◽  
Relevant Logics ◽  
Innovative Method ◽  
Gentzen System ◽  
Branching Rules ◽  
Good Range

In [1], we established Gentzenizations for a good range of relevant logics with distribution, but, in the process, we added inversion rules, which involved extra structural connectives, and also added the sentential constant t. Instead of eliminating them, we used conservative extension results to relate them back to the original logics. In [4], we eliminated the inversion rules and t and established a much simpler Gentzenization for the weak sentential relevant logic DW, and also for its quantificational extension DWQ, but a restriction to normal formulae (defined below) was required to enable these results to be proved. This method was quite general and hope was expressed about extending it to other relevant logics.In this paper, we develop an innovative method, which makes essential use of this restriction to normality, to establish two simple Gentzenizations for the normal formulae of the slightly weaker logic B, and then extend the method to other sentential contraction-less logics. To obtain the first of these Gentzenizations, for the logics B and DW, we remove the two branching rules (F&) and (T∨), together with the structural connective ‘,’, to simplify the elimination of the inversion rules and t. We then eliminate the rules (T&) and (F∨), thus reducing the Gentzen system to one containing only ˜ and → and their four associated rules, and reduce the remaining types of structures to four simple finite types. Subsequently, we re-introduce (T&) and (F∨), and also (F&) and (T∨), to obtain the second Gentzenization, which contains ‘,’ but no structural rules.

Proof Theory of the Cut Rule

2018 ◽  
Author(s):  
J. R. B. Cockett ◽  
R. A. G. Seely
Keyword(s):  
Proof Theory ◽  
Graphical Representation ◽  
Basic Component ◽  
Graphical Representations ◽  
Mathematical Language ◽  
Basic Logic ◽  
Cut Rule ◽  
Structural Rules ◽  
The One ◽  
Categorical Semantics

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.

scholarly journals Boolean negation and non-conservativity II: The variable-sharing property

2020 ◽  
Author(s):  
Tore Fjetland Øgaard
Keyword(s):  
Classical Logic ◽  
Relevant Logic ◽  
Relevant Logics ◽  
Acute Form ◽  
Vast Range ◽  
Boolean Extension

Abstract Many relevant logics are conservatively extended by Boolean negation. Not all, however. This paper shows an acute form of non-conservativeness, namely that the Boolean-free fragment of the Boolean extension of a relevant logic need not always satisfy the variable-sharing property. In fact, it is shown that such an extension can in fact yield classical logic. For a vast range of relevant logic, however, it is shown that the variable-sharing property, restricted to the Boolean-free fragment, still holds for the Boolean extended logic.

scholarly journals Boolean negation and non-conservativity I: Relevant modal logics

2020 ◽  
Author(s):  
Tore Fjetland Øgaard
Keyword(s):  
Relevant Logic ◽  
Modal Logics ◽  
Modal Operator ◽  
Relevant Logics ◽  
Theoretic Proof

Abstract Many relevant logics can be conservatively extended by Boolean negation. Mares showed, however, that E is a notable exception. Mares’ proof is by and large a rather involved model-theoretic one. This paper presents a much easier proof-theoretic proof which not only covers E but also generalizes so as to also cover relevant logics with a primitive modal operator added. It is shown that from even very weak relevant logics augmented by a weak K-ish modal operator, and up to the strong relevant logic R with a S5 modal operator, all fail to be conservatively extended by Boolean negation. The proof, therefore, also covers Meyer and Mares’ proof that NR—R with a primitive S4-modality added—also fails to be conservatively extended by Boolean negation.

scholarly journals A non-transitive relevant implication corresponding to classical logic consequence

2019 ◽  
Vol 16 (2) ◽  
pp. 10
Author(s):  
Peter Verdée ◽  
Inge De Bal ◽  
Aleksandra Samonek
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Modus Ponens ◽  
Relevant Logic ◽  
Object Language ◽  
Cut Rule ◽  
Consequence Relation ◽  
Relevant Implication ◽  
Relevant Logics ◽  
Traditional Sense

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.

scholarly journals Arithmetic Formulated Relevantly

2021 ◽  
Vol 18 (5) ◽  
pp. 154-288
Author(s):  
Robert Meyer
Keyword(s):  
Intuitionistic Logic ◽  
Natural Deduction ◽  
Relevant Logic ◽  
Peano Arithmetic ◽  
Critical Problem ◽  
First Order ◽  
Order Form ◽  
Relevant Implication ◽  
Relevant Logics ◽  
Natural Way

The purpose of this paper is to formulate first-order Peano arithmetic within the resources of relevant logic, and to demonstrate certain properties of the system thus formulated. Striking among these properties are the facts that (1) it is trivial that relevant arithmetic is absolutely consistent, but (2) classical first-order Peano arithmetic is straightforwardly contained in relevant arithmetic. Under (1), I shall show in particular that 0 = 1 is a non-theorem of relevant arithmetic; this, of course, is exactly the formula whose unprovability was sought in the Hilbert program for proving arithmetic consistent. Under (2), I shall exhibit the requisite translation, drawing some Goedelian conclusions therefrom. Left open, however, is the critical problem whether Ackermann’s rule γ is admissible for theories of relevant arithmetic. The particular system of relevant Peano arithmetic featured in this paper shall be called R♯. Its logical base shall be the system R of relevant implication, taken in its first-order form RQ. Among other Peano arithmetics we shall consider here in particular the systems C♯, J♯, and RM3♯; these are based respectively on the classical logic C, the intuitionistic logic J, and the Sobocinski-Dunn semi-relevant logic RM3. And another feature of the paper will be the presentation of a system of natural deduction for R♯, along lines valid for first-order relevant theories in general. This formulation of R♯ makes it possible to construct relevantly valid arithmetical deductions in an easy and natural way; it is based on, but is in some respects more convenient than, the natural deduction formulations for relevant logics developed by Anderson and Belnap in Entailment.

scholarly journals What Hamblin’s Formal Dialectic Tells About the Medieval Logical Disputation

2017 ◽  
Vol 23 (1) ◽  
pp. 151-176
Author(s):  
А.М. Павлова
Keyword(s):  
Cognitive Agents ◽  
Rational Agents ◽  
Structural Rules ◽  
Different Types ◽  
Full Picture ◽  
The One

In this paper we reconstruct a famous Severin Boethius’s reasoning according to the idea of the medieval obligationes disputation mainly focusing on the formalizations proposed by Ch. Hamblin. We use two different formalizations of the disputation: first with the help of Ch. Hamblin’s approach specially designed to formalize such logical debates; second, on the basis of his formal dialectics. The two formalizations are used to analyze the logical properties of the rules of the medieval logical disputation and that of their formal dialectic’s counterparts. Our aim is to to show that Hamblin’s formal dialectic is a communicative protocol for rational agents whose structural rules may differ, thus, varying its normative character. By means of comparing Hamblin’s reconstructions with the one proposed by C. Dutilh-Novaes we are able to justify the following conclusions: (1) the formalization suggested by Hamblin fails to reconstruct the full picture of the disputation because it lacks in some the details of it; (2) Hamblin’s formal dialectic and the medieval logical disputation are based on different logical theories; (3) medieval logical disputation, represented by the formalization of C. Dutilh-Novaes, and the two ones of Hamblin encode different types of cognitive agents. DOI: 10.21146/2074-1472-2017-23-1-151-176

scholarly journals Relevant Logics Obeying Component Homogeneity

2018 ◽  
Vol 15 (2) ◽  
pp. 301 ◽  
Author(s):  
Roberto Ciuni ◽  
Damian Szmuc ◽  
Thomas Macaulay Ferguson
Keyword(s):  
Sufficient Conditions ◽  
Relevant Logic ◽  
The Other ◽  
Consequence Relations ◽  
Sequent Calculi ◽  
Characterization Result ◽  
General Characterization ◽  
Relevant Logics ◽  
Necessary And Sufficient ◽  
Open Issues

This paper discusses three relevant logics (S*fde , dS*fde , crossS*fde) that obey Component Homogeneity - a principle that Goddard and Routley introduce in their project of a logic of significance. The paper establishes two main results. First, it establishes a general characterization result for two families of logic that obey Component Homogeneity - that is, we provide a set of necessary and sufficient conditions for their consequence relations. From this, we derive characterization results for S*fde , dS*fde , crossS*fde. Second, the paper establishes complete sequent calculi for S*fde , dS*fde , crossS*fde. Among the other accomplishments of the paper, we generalize the semantics from Bochvar, Hallden, Deutsch and Daniels, we provide a general recipe to define (a given family of) containment logics, we explore the single-premise/single-conclusion fragment of S*fde , dS*fde , crossS*fde and the connections between crossS*fde and the logic Eq of equality by Epstein. Also, we present S*fde  as a relevant logic of meaninglessness that follows the main philosophical tenets of Goddard and Routley, and we briefly examine three further systems that are closely related to our main logics. Finally, we discuss Routley's criticism to containment logic in light of our results, and overview some open issues.

There exists an uncountable set of pretabular extensions of the relevant logic R and each logic of this set is generated by a variety of finite height

2008 ◽  
Vol 73 (4) ◽  
pp. 1249-1270 ◽  
Author(s):  
Kazimierz Swirydowicz
Keyword(s):  
Relevant Logic ◽  
Philosophical Logic ◽  
Relevant Logics ◽  
Finite Height

AbstractIn Handbook of Philosophical Logic M. Dunn formulated a problem of describing pretabular extensions of relevant logics (cf. M. Dunn [1984], p. 211; M. Dunn, G. Restall [2002], p. 79). The main result of this paper is described in the title.

scholarly journals Basic Relevant Theories for Combinators at Levels I and II

2005 ◽  
Vol 3 ◽  
Author(s):  
Koushik Pal ◽  
Robert K. Meyer
Keyword(s):  
Relevant Logic ◽  
Semantic Completeness ◽  
Relevant Logics ◽  
Level Ii ◽  
Level I

The system B+ is the minimal positive relevant logic. B+ is trivially extended to B+T on adding a greatest truth (Church constant) T. If we leave ∨ out of the formation apparatus, we get the fragment B∧T. It is known that the set of ALL B∧T theories provides a good model for the combinators CL at Level-I, which is the theory level. Restoring ∨ to get back B+T was not previously fruitful at Level-I, because the set of all B+T theories is NOT a model of CL. It was to be expected from semantic completeness arguments for relevant logics that basic combinator laws would hold when restricted to PRIME B+T theories. Overcoming some previous difficulties, we show that this is the case, at Level I. But this does not form a model for CL. This paper also looks for corresponding results at Level-II, where we deal with sets of theories that we call propositions. We adapt work by Ghilezan to note that at Level-II also there is a model of CL in B∧T propositions. However, the corresponding result for B+T propositions extends smoothly to Level-II only in part. Specifically, only some of the basic combinator laws are proved here. We accordingly leave some work for the reader.

Sign in / Sign up

Export Citation Format

Share Document