# Algorithmic proof methods and cut elimination for implicational logics part I: Modal implication

Studia Logica 61 (2):237-280 (1998)

# Abstract

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].

## PhilArchive

Upload a copy of this work     Papers currently archived: 91,088

Setup an account with your affiliations in order to access resources via your University's proxy server

# Similar books and articles

Goal-directed proof theory.Dov M. Gabbay - 2000 - Boston: Kluwer Academic. Edited by Nicola Olivetti.
Deduction theorems for weak implicational logics.M. W. Bunder - 1982 - Studia Logica 41 (2-3):95 - 108.
Labelled non-classical logics.Luca Viganò - 2000 - Boston: Kluwer Academic Publishers.
Proof theory of modal logic.Heinrich Wansing (ed.) - 1996 - Boston: Kluwer Academic Publishers.
Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.
Implicational f-structures and implicational relevance logics.A. Avron - 2000 - Journal of Symbolic Logic 65 (2):788-802.

2009-01-28

44 (#327,510)

6 months
6 (#252,172)

# Author's Profile

Dov Gabbay
Hebrew University of Jerusalem

# Citations of this work

Dual-Context Sequent Calculus and Strict Implication.Kentaro Kikuchi - 2002 - Mathematical Logic Quarterly 48 (1):87-92.

# References found in this work

Proof Methods for Modal and Intuitionistic Logics.Melvin Fitting - 1985 - Journal of Symbolic Logic 50 (3):855-856.
Intuitionistic tense and modal logic.W. B. Ewald - 1986 - Journal of Symbolic Logic 51 (1):166-179.