An axiomatic version of positive semilattice relevance logic

1981 ◽  
Vol 46 (2) ◽  
pp. 233-239 ◽  
Author(s):  
G. Charlwood
Keyword(s):  
Natural Deduction ◽  
Relevance Logic ◽  
Truth Conditions ◽  
Completeness Proof ◽  
Relevant Implication ◽  
Soundness And Completeness ◽  
Minimal Modification ◽  
Positive Relevance

In [8] and [9] Urquhart presented the semilattice semantics for a relevance logic with conjunction and disjunction. These semantics combined the simplest known semantics for relevant implication, with minimal modification of the truth conditions for conjunction and disjunction. A slightly different approach leads to the distinct positive relevance logic of [7] and [5]. Sound and complete axiomatic logics for the semilattice semantics were readily available, so long as disjunction was left out.The purpose of this paper is to report the remedy of this lack. In [1] the author developed work of Fine ([3], announced in [4]) and Prawitz [6] to show soundness and completeness of an axiomatic logic and two natural deduction logics, with respect to Urquhart's semantics. Thus Prawitz' positive relevance logic is equivalent to the semilattice logic, rather than the logic of [5]. We present here the axiomatic logic and show its equivalence to the semilattice semantics.In §1 the languages and logic are given, along with a few proof-theoretic remarks. In §2 the semantics are defined, and the soundness proof is sketched. In §3, the completeness proof is given.

scholarly journals On Polymorphic Sessions and Functions

2021 ◽  
Vol 43 (2) ◽  
pp. 1-55
Author(s):  
Bernardo Toninho ◽  
Nobuko Yoshida
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Linear Formulation ◽  
Session Types ◽  
Logical Foundation ◽  
Π Calculus ◽  
Soundness And Completeness ◽  
System F ◽  
Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Multiplicative conjunction and an algebraic meaning of contraction and weakening

1998 ◽  
Vol 63 (3) ◽  
pp. 831-859 ◽  
Author(s):  
A. Avron
Keyword(s):  
Classical Logic ◽  
Linear Logic ◽  
Substructural Logics ◽  
Interesting Property ◽  
Relevance Logic ◽  
Proper Subset ◽  
Algebraic Structures ◽  
Elimination Rule ◽  
First Case ◽  
Soundness And Completeness

AbstractWe show that the elimination rule for the multiplicative (or intensional) conjunction Λ is admissible in many important multiplicative substructural logics. These include LLm (the multiplicative fragment of Linear Logic) and RMIm (the system obtained from LLm by adding the contraction axiom and its converse, the mingle axiom.) An exception is Rm (the intensional fragment of the relevance logic R, which is LLm together with the contraction axiom). Let SLLm and SRm be, respectively, the systems which are obtained from LLm and Rm by adding this rule as a new rule of inference. The set of theorems of SRm is a proper extension of that of Rm, but a proper subset of the set of theorems of RMIm. Hence it still has the variable-sharing property. SRm has also the interesting property that classical logic has a strong translation into it. We next introduce general algebraic structures, called strong multiplicative structures, and prove strong soundness and completeness of SLLm relative to them. We show that in the framework of these structures, the addition of the weakening axiom to SLLm corresponds to the condition that there will be exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there will be exactly one nondesignated element (in the first case we get the system BCKm, in the second - the system SRm). Various other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts.

scholarly journals Hybrid Deduction–Refutation Systems

Axioms ◽  
2019 ◽  
Vol 8 (4) ◽  
pp. 118 ◽  
Author(s):  
Valentin Goranko
Keyword(s):  
Propositional Logic ◽  
Proof Theory ◽  
Natural Deduction ◽  
Basic Theory ◽  
Logical System ◽  
Classical Propositional Logic ◽  
Deductive Systems ◽  
Refutation Systems ◽  
Soundness And Completeness

Hybrid deduction–refutation systems are deductive systems intended to derive both valid and non-valid, i.e., semantically refutable, formulae of a given logical system, by employing together separate derivability operators for each of these and combining ‘hybrid derivation rules’ that involve both deduction and refutation. The goal of this paper is to develop a basic theory and ‘meta-proof’ theory of hybrid deduction–refutation systems. I then illustrate the concept on a hybrid derivation system of natural deduction for classical propositional logic, for which I show soundness and completeness for both deductions and refutations.

Natural deduction and sequent calculus for intuitionistic relevant logic

1987 ◽  
Vol 52 (3) ◽  
pp. 665-680 ◽  
Author(s):  
Neil Tennant
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Deductive System ◽  
Relevant Logic ◽  
Relevance Logic ◽  
Minimal Logic ◽  
Disjunctive Syllogism

Relevance logic began in an attempt to avoid the so-called fallacies of relevance. These fallacies can be in implicational form or in deductive form. For example, Lewis's first paradox can beset a system in implicational form, in that the system contains as a theorem the formula (A & ∼A) → B; or it can beset it in deductive form, in that the system allows one to deduce B from the premisses A, ∼A.Relevance logic in the tradition of Anderson and Belnap has been almost exclusively concerned with characterizing a relevant conditional. Thus it has attacked the problem of relevance in its implicational form. Accordingly for a relevant conditional → one would not have as a theorem the formula (A & ∼A) → B. Other theorems even of minimal logic would also be lacking. Perhaps most important among these is the formula (A → (B → A)). It is also a well-known feature of their system R that it lacks the intuitionistically valid formula ((A ∨ B) & ∼A) → B (disjunctive syllogism).But it is not the case that any relevance logic worth the title even has to concern itself with the conditional, and hence with the problem in its implicational form. The problem arises even for a system without the conditional primitive. It would still be an exercise in relevance logic, broadly construed, to formulate a deductive system free of the fallacies of relevance in deductive form even if this were done in a language whose only connectives were, say, &, ∨ and ∼. Solving the problem of relevance in this more basic deductive form is arguably a precondition for solving it for the conditional, if we suppose (as is reasonable) that the relevant conditional is to be governed by anything like the rule of conditional proof.

An environment machine for the λμ-calculus

1998 ◽  
Vol 8 (6) ◽  
pp. 637-669 ◽  
Author(s):  
PHILIPPE de GROOTE
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Soundness And Completeness ◽  
Head Normal Form

We introduce a natural deduction-like formalisation of Parigot's λμ-calculus. From this, we derive an environment machine that allows any well-typed λμ-term to be reduced to its weak head normal form. The soundness and completeness of the machine is proved.

scholarly journals De Finettian Logics of Indicative Conditionals Part II: Proof Theory and Algebraic Semantics

2021 ◽  
Author(s):  
Paul Égré ◽  
Lorenzo Rossi ◽  
Jan Sprenger
Keyword(s):  
Proof Theory ◽  
Future Research ◽  
Algebraic Semantics ◽  
Sequent Calculi ◽  
Truth Conditions ◽  
Indicative Conditionals ◽  
Tarski Algebra ◽  
Soundness And Completeness ◽  
Tableau Calculi ◽  
The One

AbstractIn Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti (1936) and Reichenbach (1935, 1944) on the one hand, and by Cooper (Inquiry, 11, 295–320, 1968) and Cantwell (Notre Dame Journal of Formal Logic, 49, 245–260, 2008) on the other. Here we provide the proof theory for the resulting logics and , using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: allows for algebraic completeness, but not for the construction of a canonical model, while fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects.

scholarly journals A Logic for Vagueness

2010 ◽  
Vol 8 ◽  
Author(s):  
John Slaney
Keyword(s):  
Natural Deduction ◽  
Kripke Semantics ◽  
Substructural Logic ◽  
Relational Semantics ◽  
Deduction System ◽  
First Order ◽  
Natural Deduction System ◽  
Soundness And Completeness ◽  
Propositional System

This paper presents F, substructural logic designed to treat vagueness. Weaker than Lukasiewicz’s infinitely valued logic, it is presented first in a natural deduction system, then given a Kripke semantics in the manner of Routley and Meyer's ternary relational semantics for R and related systems, but in this case, the points are motivated as degrees to which the truth could be stretched. Soundness and completeness are proved, not only for the propositional system, but also for its extension with first-order quantifiers. The first-order models allow not only objects with vague properties, but also objects whose very existence is a matter of degree.

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.

Sign in / Sign up

Export Citation Format

Share Document