Consider the problem which set V of propositional variables suffices for whenever, where, and ⊢c and ⊢i denote derivability in classical and intuitionistic implicational logic, respectively. We give a direct proof that stability for the final propositional variable of the (implicational) formula A is sufficient; as a corollary one obtains Glivenko's theorem. Conversely, using Glivenko's theorem one can give an alternative proof of our result. As an alternative to stability we then consider the Peirce formula. It is an (...) easy consequence of the result above that adding a single instance of the Peirce formula suffices to move from classical to intuitionistic derivability. Finally we consider the question whether one could do the same for minimal logic. Given a classical derivation of a propositional formula not involving ⊥, which instances of the Peirce formula suffice as additional premises to ensure derivability in minimal logic? We define a set of such Peirce formulas, and show that in general an unbounded number of them is necessary. (shrink)

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)

A constructive proof is given which shows that every nonrecursive r.e. many-one degree is represented by the family of decision problems for partial implicational propositional calculi whose well-formed formulas contain at most two distinct variable symbols.

We consider the notion of structural completeness with respect to arbitrary (finitary and/or infinitary) inferential rules. Our main task is to characterize structurally complete intermediate logics. We prove that the structurally complete extension of any pure implicational in termediate logic C can be given as an extension of C with a certain family of schematically denned infinitary rules; the same rules are used for each C. The cardinality of the family is continuum and, in the case of (the pure (...) implicational fragment of) intuitionistic logic, the family cannot be reduced to a countable one. It means that the structurally complete extension of the intuitionistic logic is not countably axiomatizable by schematic rules. (shrink)

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)

I present a new syntactical method for proving the Interpolation Theorem for the implicational fragment of intuitionistic logic and its substructural subsystems. This method, like Prawitz’s, works on natural deductions rather than sequent derivations, and, unlike existing methods, always finds a ‘strongest’ interpolant under a certain restricted but reasonable notion of what counts as an ‘interpolant’.

Matthew Spinks [35] introduces implicative BCSK-algebras, expanding implicative BCK-algebras with an additional binary operation. Subdirectly irreducible implicative BCSK-algebras can be viewed as flat posets with two operations coinciding only in the 1- and 2-element cases, each, in the latter case, giving the two-valued implication truth-function. We introduce the resulting logic (for the general case) in terms of matrix methodology in §1, showing how to reformulate the matrix semantics as a Kripke-style possible worlds semantics, thereby displaying the distinction between the two (...) implications in the more familiar language of modal logic. In §§2 and 3 we study, from this perspective, the fragments obtained by taking the two implications separately, and – after a digression (in §4) on the intuitionistic analogue of the material in §3 – consider them together in §5, closing with a discussion in §6 of issues in the theory of logical rules. Some material is treated in three appendices to prevent §§1–6 from becoming overly distended. (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)

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)

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.

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 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)

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)

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)

C5.ω is obtained by adding, schematically, to the strict-implicational fragment C5 of S5 the axiom → ) → . This paper presents a fully general proof that neither C5.ω nor any of a descending chain of its extensions is complete with respect to any class of frames, correcting the garbled details of a version skeched in an earlier paper , 201-208).

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)

The genome revolution has provided the basis for many new applications in diverse areas such as health, food and agriculture, and forensics. While standard DNA profiling has become the paramount form of identification in forensics, expansion of genomic applications is being considered and tested to provide more descriptive information to facilitate the capture of perpetrators. Two major applications are being explored and tested: 1) ancestry profiling from which race can be inferred; and 2) profiling for physical traits to provide a (...) genetic-based description or sketch. The use and incorporation of these new applications raises several logistical questions and ethical issues. This article will explore some of the policy implications in the use of expanded genome profiling for forensics purposes. (shrink)