The proofs of α → α in P – W

1996 ◽  
Vol 61 (1) ◽  
pp. 195-211 ◽  
Author(s):  
Sachio Hirokawa
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Syntactic Structure ◽  
Modus Ponens ◽  
Relevant Logic

AbstractThe syntactic structure of the system of pure implicational relevant logic P − W is investigated. This system is defined by the axioms B = (b → c) → (a → b) → a → c, B′ = (a → b) → (b → c)→ a → c, I = a → a, and the rules of substitution and modus ponens. A class of λ-terms, the closed hereditary right-maximal linearλ-terms, and a translation of such λ-terms M to BB′ I-combinators M+ is introduced. It is shown that a formula a is provable in P − W if and only if α is a type of some λ-term in this class. Hence these λ-terms represent proof figures in the Natural Deduction version of P − W.Errol Martin (1982) proved that no formula with form α → α is provable in P − W without using the axiom I. We show that a β-normal form λ-term M in the class is η reducible to λx.x if the translated BB′ I-combinator M+ contains I. Using this theorem and Martin's result, we prove that a λ-term in the class is βη-reducible to λx.x if the λ-term has a type α → α. Hence the structure of proofs of α → α in P − W is determined.

Normalization theorems for full first order classical natural deduction

1991 ◽  
Vol 56 (1) ◽  
pp. 129-149 ◽  
Author(s):  
Gunnar Stålmarck
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Full System ◽  
Strong Normalization ◽  
Logical Constants ◽  
Restricted Version ◽  
First Order ◽  
Form Theorem ◽  
Normalization Theorem ◽  
Normal Form Theorem

In this paper we prove the strong normalization theorem for full first order classical N.D. (natural deduction)—full in the sense that all logical constants are taken as primitive. We also give a syntactic proof of the normal form theorem and (weak) normalization for the same system.The theorem has been stated several times, and some proofs appear in the literature. The first proof occurs in Statman [1], where full first order classical N.D. (with the elimination rules for ∨ and ∃ restricted to atomic conclusions) is embedded in a system for second order (propositional) intuitionistic N.D., for which a strong normalization theorem is proved using strongly impredicative methods.A proof of the normal form theorem and (weak) normalization theorem occurs in Seldin [1] as an extension of a proof of the same theorem for an N.D.-system for the intermediate logic called MH.The proof of the strong normalization theorem presented in this paper is obtained by proving that a certain kind of validity applies to all derivations in the system considered.The notion “validity” is adopted from Prawitz [2], where it is used to prove the strong normalization theorem for a restricted version of first order classical N.D., and is extended to cover the full system. Notions similar to “validity” have been used earlier by Tait (convertability), Girard (réducibilité) and Martin-Löf (computability).In Prawitz [2] the N.D. system is restricted in the sense that ∨ and ∃ are not treated as primitive logical constants, and hence the deductions can only be seen to be “natural” with respect to the other logical constants. To spell it out, the strong normalization theorem for the restricted version of first order classical N.D. together with the well-known results on the definability of the rules for ∨ and ∃ in the restricted system does not imply the normalization theorem for the full system.

A sequent calculus for type assignment

1977 ◽  
Vol 42 (1) ◽  
pp. 11-28 ◽  
Author(s):  
Jonathan P. Seldin
Keyword(s):  
Normal Form ◽  
Main Part ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Cut Elimination ◽  
Type Assignment ◽  
Image Position ◽  
Atomic Type

The sequent calculus formulation (L-formulation) of the theory of functionality without the rules allowing for conversion of subjects of [3, §14E6] fails because the (cut) elimination theorem (ET) fails. This can be most easily seen by the fact that it is easy to prove in the systemandbut not (as is obvious if α is an atomic type [an F-simple])The error in the “proof” of ET in [14, §3E6], [3, §14E6], and [7, §9C] occurs in Stage 3, where it is implicitly assumed that if [x]X ≡ [x] Y then X ≡ Y. In the above counterexample, we have [x]x ≡ ∣ ≡ [x](∣x) but x ≢ ∣x. Since the formulation of [2, §9F] is not really satisfactory (for reasons stated in [3, §14E]), a new seguent calculus formulation is needed for the case in which the rules for subject conversions are not present. The main part of this paper is devoted to presenting such a formulation and proving it equivalent to the natural deduction formulation (T-formulation). The paper will conclude in §6 with some remarks on the result that every ob (term) with a type (functional character) has a normal form.The conventions and definitions of [3], especially of §12D and Chapter 14, will be used throughout the paper.

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.

scholarly journals The number of proofs for a BCK-formula

1993 ◽  
Vol 58 (2) ◽  
pp. 626-628 ◽  
Author(s):  
Yuichi Komori ◽  
Sachio Hirokawa
Keyword(s):  
Normal Form ◽  
Modus Ponens ◽  
Basic Notion ◽  
Type Assignment ◽  
Natural Deduction System ◽  
Cartesian Closed Categories ◽  
Image Position ◽  
Coherence Theorem ◽  
Cartesian Closed ◽  
Necessary And Sufficient

In this note, we give a necessary and sufficient condition for a BCK-formula to have the unique normal form proof.We call implicational propositional formulas formulas for short. BCK-formulas are the formulas which are derivable from axioms B = (a → b) → (c → a) → c → b, C = (a→b→c)→b→a→c, and K = a→b→a by substitution and modus ponens. It is known that the property of being a BCK-formula is decidable (Jaskowski [11, Theorem 6.5], Ben-Yelles [3, Chapter 3, Theorem 3.22], Komori [12, Corollary 6]). The set of BCK-formulas is identical to the set of provable formulas in the natural deduction system with the following two inference rules.Here γ occurs at most once in (→I). By the formulae-as-types correspondence [10], this set is identical to the set of type-schemes of closed BCK-λ-terms. (See [5].) A BCK-λ-term is a λ-term in which no variable occurs twice. Basic notion concerning the type assignment system can be found [4]. Uniqueness of normal form proofs has been known for balanced formulas. (See [2,14].) It is related to the coherence theorem in cartesian closed categories. A formula is balanced when no variable occurs more than twice in it. It was shown in [8] that the proofs of balanced formulas are BCK-proofs. Relevantly balanced formulas were defined in [9], and it was proved that such formulas have unique normal form proofs. Balanced formulas are included in the set of relevantly balanced formulas.

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.

Implicational logics in natural deduction systems

1982 ◽  
Vol 47 (1) ◽  
pp. 184-186 ◽  
Author(s):  
E.G.K. López-Escobar
Keyword(s):  
Natural Deduction ◽  
Short Note ◽  
Direct Proof ◽  
Modus Ponens ◽  
Implicational Logics

In 1959 M. Dummett [3] introduced the logic LC obtained by adding the axiom ACpqCqp to the formalization of the intuitionistic prepositional calculus having modus ponens and substitution as its rules of inference. Later on R. A. Bull [1] showed, by quite a roundabout way, that the implicational theses of LC were precisely the theses of the implicational calculus obtained by adding the axiom CCCpqrCCCqprr to the system of positive implication. In 1964 Bull [2] gave another proof, this time using results of Birkhoff concerning subdirectly reducible algebras.The aim of this short note is to emphasize that the use of Gentzen's natural deduction systems (see Prawitz [4]) allows us to give a much more direct proof.

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 The D-Completeness of T→

2010 ◽  
Vol 8 ◽  
Author(s):  
R. K. Meyer ◽  
M. W. Bunder
Keyword(s):  
Modus Ponens ◽  
Relevant Logic ◽  
Condensed Detachment ◽  
Minimal Form

A Hilbert-style version of an implicational logic can be represented by a set of axiom schemes and modus ponens or by the corresponding axioms, modus ponens and substitution. Certain logics, for example the intuitionistic implicational logic, can also be represented by axioms and the rule of condensed detachment, which combines modus ponens with a minimal form of substitution. Such logics, for example intuitionistic implicational logic, are said to be D-complete. For certain weaker logics, the version based on condensed detachment and axioms (the condensed version of the logic) is weaker than the original. In this paper we prove that the relevant logic T[→], and any logic of which this is a sublogic, is D-complete.

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.

Proofs, Snakes and Ladders

Dialogue ◽  
1974 ◽  
Vol 13 (4) ◽  
pp. 723-731 ◽  
Author(s):  
Alasdair Urquhart
Keyword(s):  
Normal Form ◽  
Intuitionistic Logic ◽  
Natural Deduction ◽  
Tree Structure ◽  
Deduction System ◽  
Syntactical Structure ◽  
Form Theorem ◽  
Structural Identity ◽  
Natural Deduction System ◽  
Normal Form Theorem

Anyone who has worked at proving theorems of intuitionistic logic in a natural deduction system must have been struck by the way in which many logical theorems “prove themselves.” That is, proofs of many formulas can be read off from the syntactical structure of the formulas themselves. This observation suggests that perhaps a strong structural identity may underly this relation between formulas and their proofs. A formula can be considered as a tree structure composed of its subformulas (Frege 1879) and by the normal form theorem (Gentzen 1934) every formula has a normalized proof consisting of its subformulas. Might we not identify an intuitionistic theorem with (one of) its proof(s) in normal form?

Sign in / Sign up

Export Citation Format

Share Document