Abstract
The purpose of this chapter is to extend the goal-directed proof methods to strict implication modal logics. We consider this as a first step in order to extend the goal-directed paradigm to the realm of modal logics. Strict implication, denoted by A ⇒ B is read as ‘necessarily A implies B’. The notion of necessity (and the dual notion of possibility) are the subject of modal logics. Strict implication can be regarded as a derived notion: A ⇒ B = □(A → B),where → denotes material implication and □ denotes modal necessity. However, strict implication can also be considered as a primitive notion, and has already been considered as such at the beginning of the century in many discussions about the paradoxes of material implication [Lewis, 1912; Lewis and Langford, 1932].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Reference
We use the acronym KT rather than the more common T, as the latter is also the name of a subrelevance logic we will meet in Chapter 5.
We do not consider here systems containing D: •A —+ OA, which correspond to the seriality of the accessibility relation, i.e. Vx3y xRy in Kripke frames. The reason is that seriality cannot be expressed in the language of strict implication alone; moreover, it cannot be expressed in any modal language, unless or 0 is allowed. We will come back to the treatment of seriality in Section 7.3.
We will drop this condition in Section 7, when we add conjunction.
In these two systems the validity of DC does not imply the validity of C, as it holds for all the other systems considered in this chapter.
Our modified implication rule corresponds closely to the rule for necessity in G in the tableau formulation: if •A is in a branch then create a new world with -’A and •A [Fitting, 19831.
We can introduce a further distinction between an extensional part of AR corresponding to the old a and an intensional part containing the Horn formulas; the former varies for each database, whereas the latter is fixed for each modal logic.
This distinction is emphasized, for instance, in [Gore, 1999].
The following calculus makes another simplification w.r.t. the original formulation, the only formula in the consequent is always at the same level as maximum level of the 2-sequence in the antecedent, thus we can omit Ek in the consequent.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Gabbay, D.M., Olivetti, N. (2000). Modal Logics of Strict Implication. In: Goal-Directed Proof Theory. Applied Logic Series, vol 21. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-1713-7_4
Download citation
DOI: https://doi.org/10.1007/978-94-017-1713-7_4
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5526-2
Online ISBN: 978-94-017-1713-7
eBook Packages: Springer Book Archive