We establish the “contraction-elimination theorem” which means that if a sequent Γ A is provable in the implicational fragment of the Gentzen's sequent calculus LK and if it satisfies a certain condition on the number of the occurrences of propositional variables, then it is provable without the right contraction rule. By this theorem, we get the following.1. If an implicational formula A is a theorem of classical logic and is not a theorem of intuitionistic logic, then there is (...) a propositional variable which occurs at least once positively and at least twice negatively in A → a) → a).2. If an implicational formula A is a theorem of intuitionistic logic and is not a theorem of BCK-logic, then there is a propositional variable which occurs at least twice positively and at least once negatively in A → a → b).We prove the contraction-elimination theorem by a fully syntactical method, which has some analogy with Gentzen's cut-elimination. (shrink)

Shortest possible axiomatizations for the implicational fragments of the modal logics S4 and S5 are reported. Among these axiomatizations is included a shortest single axiom for implicational S4—which to our knowledge is the first reported single axiom for that system—and several new shortest single axioms for implicational S5. A variety of automated reasoning strategies were essential to our discoveries.

In this paper we consider the implicational fragment of Abelian logic \ . We show that although the Abelian groups provide an semantics for the set of theorems of \ they do not for the associated consequence relation. We then show that the consequence relation is not algebraizable in the sense of Blok and Pigozzi . In the second part of the paper, we investigate an extension of \ in the same language and having the same set of theorems (...) and show that this new consequence relation is algebraizable with the Abelian groups as its equivalent algebraic semantics. Finally, we show that although \ is not algebraizable, it is order-algebraizable in the sense of Raftery. (shrink)

In the context of implicational tonoid logics, this paper investigates analogues of Birkhoff’s two theorems, the so-called subdirect representation and varieties theorems, and of Mal’cev’s quasi-varieties theorem. More precisely, we first recall the class of implicational tonoid logics. Next, we establish the subdirect product representation theorem for those logics and then consider some more related results such as completeness. Thirdly, we consider the varieties theorem for them. Finally, we introduce an analogue of Mal’cev’s quasi-varieties theorem for algebras.

The standard deduction theorem or introduction rule for implication, for classical logic is also valid for intuitionistic logic, but just as with predicate logic, other rules of inference have to be restricted if the theorem is to hold for weaker implicational logics.In this paper we look in detail at special cases of the Gentzen rule for and show that various subsets of these in effect constitute deduction theorems determining all the theorems of many well known as well as not (...) well known implicational logics. In particular systems of rules are given which are equivalent to the relevance logics E,R, T, P-W and P-W-I. (shrink)

In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. (...) We then show that for most of the systems under consideration the labelling mechanism can be avoided by choosing an appropriate way of structuring theories. One peculiar feature of our proof systems is the use of restart rules which allow to re-ask the original goal of a deduction. In case of K, K4, S4 and G, we can eliminate such a rule, without loosing completeness. In all the other cases, by dropping such a rule, we get an intuitionistic variant of each system. The present results are part of a larger project of a goal directed proof theory for non-classical logics; the purpose of this project is to show that most implicational logics stem from slight variations of a unique deduction method, and from different ways of structuring theories. Moreover, the proof systems we present follow the logic programming style of deduction and seem promising for proof search [Gabbay and Reyle 84, Miller et al. 91]. (shrink)

The introduction and elimination rules for material implication in natural deduction are not complete with respect to the implicational fragment of classical logic. A natural way to complete the system is through the addition of a new natural deduction rule corresponding to Peirce's formula → A) → A). E. Zimmermann [6] has shown how to extend Prawitz' normalization strategy to Peirce's rule: applications of Peirce's rule can be restricted to atomic conclusions. The aim of the present paper is to (...) extend Seldin's normalization strategy to Peirce's rule by showing that every derivation Π in the implicational fragment can be transformed into a derivation Π' such that no application of Peirce's rule in Π' occurs above applications of →-introduction and →-elimination. As a corollary of Seldin's normalization strategy we obtain a form of Glivenko's theorem for the classical {→}-fragment. (shrink)

The authors of [MOC 00] conjectured that intuitionistic and classical logics are asymptotically identical. Their conjecture concerns the implicational parts of these logics over k variables and is trivially true for k = 1, because implicational parts of intuitionistic and classical logics over one variable are identical. So, it seems to be interesting to investigate the appropriate fragments of these logics for k = 2. The result is obtained by reducing the problem to the same one of Dummett's (...) intermediate linear logic of two variables. Actually, this paper shows the existence of the density of this logic and demonstrates that the linear calculus covers a substantial part of classical propositional one. (shrink)

A four-valued matrix is presented which validates all theorems of the implicational fragment, IF, of the classical sentential calculus in which at most two distinct sentence letters occur. The Wajsberg/Diamond-McKinsley Theorem for IF follows as a corollary: every complete set of axioms (with substitution and detachment as rules) must include at least one containing occurrences of three or more distinct sentence letters. Additionally, the matrix validates all IF theses built from nine or fewer occurrences of connectives and letters. So (...) the classic result of Jagkovski for the full sentential calculus -that every complete axiom set must contain either two axioms of length at least nine or else one of length at least eleven-can be improved in the implicational case: every complete axiom set for IF must contain at least one axiom eleven or more characters long. Both results are "best possible", and both apply as well to most subsystems of IF, e.g., the implicational fragments of the standard relevance logics, modal logics, the relatives of implicational intutionism, and logics in the Lukasiewicz family. (shrink)

The aim of this paper is to show that the implicational fragment BKof the intuitionistic propositional calculus (IPC) without the rules of exchange and contraction has the finite model property with respect to the quasivariety of left residuation algebras (its equivalent algebraic semantics). It follows that the variety generated by all left residuation algebras is generated by the finite left residuation algebras. We also establish that BKhas the finite model property with respect to a class of structures that constitute (...) a Kripke-style relational semantics for it. The results settle a question of Ono and Komori [OK85]. (shrink)

This paper argues that superiority comparatives in Mandarin Chinese are all phrasal comparatives that can be directly interpreted, and makes a new suggestion of taking the bǐ-phrase (‘compare-phrase’) to be an adjunct and one constituent, but with bǐ-shells. This syntactic analysis allows one to combine into one phrase various compared constituents that would otherwise not be analyzed as forming a phrase by themselves. Semantically, in extension of work by Heim as well as Bhatt and Takahashi, bǐ is taken to compare (...) two sequences of arguments of a gradable predicate along the dimension given by that predicate. It is also suggested that comparatives across languages may be subject to three parameters: (i) argument-dependent comparison vs. non-argument dependent comparison, (ii) phrasal comparison vs. clausal comparison, and (iii) monoadic comparison vs. dyadic comparison. (shrink)

LetL 3 c be the smallest set of propositional formulas, which containsCpCqpCCCpqCrqCCqpCrpCCCpqCCqrqCCCpqppand is closed with respect to substitution and detachment. Let $\mathfrak{M}_3^c $ be Łukasiewicz’s three-valued implicational matrix defined as follows:cxy=min (1,1−x+y), where $x,y \in \{ 0,\tfrac{1}{2},1\}$ . In this paper the following theorem is proved: $$L_3^c = E( \mathfrak{M}_3^c )$$ The idea used in the proof is derived from Asser’s proof of completeness of the two-valued propositional calculus. The proof given here is based on the Pogorzelski’s deduction theorem (...) fork-valued propositional calculi and on Lindenbaum’s theorem. (shrink)

A minimal theorem in a logic L is an L-theorem which is not a non-trivial substitution instance of another L-theorem. Komori (1987) raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system NJ. The answer has been known to be partially positive and generally negative. It is shown here that a minimal implicational theorem A in intuitionistic logic has a unique -normal proof in NJ whenever A is (...) provable without non-prime contraction. The non-prime contraction rule in NJ is the implication introduction rule whose cancelled assumption differs from a propositional variable and appears more than once in the proof. Our result improves the known partial positive solutions to Komori's problem. Also, we present another simple example of a minimal implicational theorem in intuitionistic logic which does not have a unique -normal proof in NJ. (shrink)