Logical consequence in modal logic. II. Some semantic systems for ${\rm S}4$.
John Corcoran, George E. Weaver · Notre Dame Journal of Formal Logic · 1974
This paper is a continuation of the investigations reported in Corcoran and Weaver [1] where two logics j£Π and -CDD, having natural deduction systems based on Lewis's S5, are shown to have the usually desired properties (strong soundness, strong completeness, compactness).As in [1], we desire to treat modal logic as a "clean" natural deduction system with a conceptually meaningful semantics.Here, our investigations are carried out for several S4 based logics.These logics, when regarded as logistic systems (cf.Corcoran [2], p. 154), are seen to be equivalent; but, when regarded as consequence systems (ibid., p. 157), one diverges from the others in a fashion which suggests that two standard measures of semantic complexity may not be linked.Some of the results of [l] are presupposed here and the more obvious definitions will not be repeated in detail.We consider the logics -Cl, -C2, and -£3.These logics share the same language (^DD) and deductive system (Δ'DD) but each has its own semantics system (Σl, Σ2, Σ3).Σl is an extension of the Kripke [3] semantics for S5 as modified in [l], Σ2 is largely due to Makinson [5], and Σ3 is due to Kripke [4].-C DD is the usual modal sentential language with D, ~ and 3 as logical constants (see 2 below).Δ'DD (see 3 below), a modification of the natural deduction system given in [l], permits proofs from arbitrary sets of premises.For S a set of sentences and A & sentence, Sv-A means that A is provable from S, i.e., there is a proof (in Δ'DD) of A whose premises are among the members of S. ([-A means S\-A where S is empty.)If S\-A, we sometimes say that the argument (S, A) is demonstrable and when, in addition, S is empty we say that A is provable.Each semantic system includes a set of interpretations for ^DD together with truth-valuations for each interpretation.As usual, if M is an interpretation (in Σi) and A is a sentence, M is a model of A iff A is true on M; if S is a set of sentences, M is a model of S iff Mis a model of every member of S. St=A (in Σi) indicates that A is a logical consequence of S