This paper studies a propositional logic which is obtained by interpreting implication as formal provability. It is also the logic of finite irreflexive Kripke Models.A Kripke Model completeness theorem is given and several completeness theorems for interpretations into Provability Logic and Peano Arithmetic.

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only a limited possibility to use structural rules. Following the literature, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this ▽ as a modality, but rather as the meet of the marked formula with a special type Q. In this (...) way we can make the specific structural behaviour of marked formulas more explicit. The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the 'strong' system in the hybrid one. (shrink)

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only alimited possibility to use structural rules. Following the literture, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this as a modality, but rather as themeet of the marked formula with a special typeQ. In this way we can make (...) the specific structural behaviour of marked formulas more explicit.The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the strong system in the hybrid one. (shrink)

We introduce structural rules mingle, and investigatetheorem-equivalence, cut- eliminability, decidability, interpolabilityand variable sharing property for sequent calculi having the mingle.These results include new cut-elimination results for the extendedlogics: FLm (full Lambek logic with the mingle), GLm(Girard's linear logic with the mingle) and Lm (Lambek calculuswith restricted mingle).

The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the structural (...) rules. Next, Hubert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.The first part of the paper, which follows, contains the first two sections, which deal with sequent-systems and Hubert-formulations. The second part, due to appear in the next issue of this journal, will contain the third section, which deals with groupoid models. (shrink)

The purpose of this paper is to connect the proof theory and the model theory of a family of prepositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related to BCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the (...) structural rules. Next, Hilbert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.Below is the sequel to the first part of the paper, which appeared in the previous issue of this journal (vol. 47 (1988), pp. 353–386). The first part contained sections on sequent-systems and Hilbert-formulations, and here is the third section on groupoid models. This second part is meant to be read in conjunction with the first part. (shrink)

We investigate the semantics of the logical systems obtained by introducing the modalities and into the family of substructural implication logics (including relevant, linear and intuitionistic implication). Then, in the spirit of the LDS (Labelled Deductive Systems) methodology, we "import" this semantics into the classical proof system KE. This leads to the formulation of a uniform labelled refutation system for the new logics which is a natural extension of a system for substructural implication developed by the first two authors in (...) a previous paper. (shrink)

We present a semantic study of a family of modal intuitionistic linear systems, providing various logics with both an algebraic semantics and a relational semantics, to obtain completeness results. We call modality a unary operator on formulas which satisfies only one rale (regularity), and we consider any subsetW of a list of axioms which defines the exponential of course of linear logic. We define an algebraic semantics by interpreting the modality as a unary operation on an IL-algebra. Then we introduce (...) a relational semantics based on pretopologies with an additional binary relationr between information states. The interpretation of is defined in a suitable way, which differs from the traditional one in classical modal logic. We prove that such models provide a complete semantics for our minimal modal system, as well as, by requiring the suitable conditions onr (in the spirit of correspondence theory), for any of its extensions axiomatized by any subsetW as above. We also prove an embedding theorem for modal IL-algebras into complete ones and, after introducing the notion of general frame, we apply it to obtain a duality between general frames and modal IL-algebras. (shrink)