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.

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.

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.

A contractionless semilattice semantics

1987 ◽  
Vol 52 (2) ◽  
pp. 526-529 ◽  
Author(s):  
Steve Giambrone ◽  
Robert K. Meyer ◽  
Alasdair Urquhart
Keyword(s):  
Natural Deduction ◽  
Model Structure ◽  
Commutative Monoid ◽  
Central Idea ◽  
Relevant Implication ◽  
Relevant Logics ◽  
Gentzen System ◽  
The Way

Semilattice semantics for relevant logics were discovered independently by Routley and Urquhart over 10 years ago. A semilattice semantics was first published in [10], where the weak theory of implication of [8] and [3] (i.e., R →, the pure implication fragment of the system R of relevant implication) is shown to be consistent and complete with respect to it. That result was extended in [11], But the semantics is explored in greatest detail in [12]. As reported in [4], Fine outfitted the positive semilattice semantics for R+ with a suitable Hilbert-style axiomatisation. (We refer to the system as ◡R+.) In 1980 Charlwood supplied a subscripted system of natural deduction. (See [1] and [2].) A subscripted Gentzen system was devised in [5] and [6].Obviously, the central idea of the semilattice semantics is to impose relevant-style valuations on a semilattice (with an identity) used as the underlying model structure. However, in [12] the contractionless semantics are obtained (quite reasonably) by dropping the idempotence postulate and thus changing the relatively simple semilattice structure into a commutative monoid. Here we show that the semilattice structure can be regained for positive, contractionless relevant implication. Although we have no proofs as yet, we think that this semantics will pave the way for showing completeness for the corresponding subscripted Gentzen and natural deduction systems, as well as the Hilbert-style axiomatization, ◡RW+.

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 Boolean Conservative Extension Results for some Modal Relevant Logics

2010 ◽  
Vol 8 ◽  
Author(s):  
Edwin D. Mares ◽  
Koji Tanaka
Keyword(s):  
Conservative Extension ◽  
Relevant Logics

This paper shows that a collection of modal relevant logics are conservatively extended by the addition of Boolean negation.

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